arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2506.21114

Proof verification by polynomial Fingerprinting

Mihai Prunescu
View original source ↗Read source document ↗Export metadata ↓

Abstract

To cater to the needs of fast verification for mathematical proofs, we describe a method to encode formal sentences in $2 \times 2$ - matrices over multivariate polynomials with integer coefficients. This correspondence is homomorphic: usual proof-steps like modus-ponens or variable substitution in terms and formulae become operations with matrices. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to axioms and tautologies have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. The polynomial matrix corresponding to the conclusion of the proof is also evaluated in the chosen random values. If the last term of the numeric sequence equals the evaluation of the conclusion, by the Schwartz-Zippel Lemma, the proof is with high probability correct.

Explore related subjects

math.LOcs.CR

Keep this discovery

BibTeXRIS

Mihai Prunescu. 2026-09-04. Proof verification by polynomial Fingerprinting. https://doi.org/10.4204/eptcs.427.3

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.CR subjectmath.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2025

Security Science (SecSci), Basic Concepts and Mathematical Foundations

This textbook compiles the lecture notes from security courses taught at Oxford in the 2000s, at Royal Holloway in the 2010s, and currently in Hawaii. The early chapters are suitable for a first course in security. The middle chapters have been used in advanced courses. Towards the end there are also some research problems.

cs.CR↗
arXiv2026

Bootstrapping Mutual Attestation with Kleene's Second Recursion Theorem

Mutual attestation among nodes with no central trusted operator requires each node to hold reference values (expected code measurements) for its peers. The naïve approach of mutually embedding these reference values in the nodes' code leads to an infinite regress. We call the problem of resolving this infinite regress the reference-value bootstrapping problem for mutual attestation. Existing solutions avoid this regress by relying on a trusted third party (TTP), externally supplied reference values, or architecture-specific measurement mechanisms. We instead express the bootstrapping problem as a system of mutual fixed-point equations and solve it by Kleene's second recursion theorem. The construction produces nodes that mutually reference one another's code and reconstruct every peer's exact source from built-in data alone. When a deployed source file is measured directly, as with a Python script, a node obtains the peer's reference value by applying the measurement function directly to the reconstructed source. When a built image is measured, as with AWS Nitro Enclaves, a node instead reproducibly rebuilds the peer's image from the reconstructed source and derives its reference measurement. For the first case, we develop PyReflect, a Python transpiler, and use it to implement a TPM mutual-attestation PoC. For the second, we develop NixReflect, a Nix transpiler, and use it in a PoC in which two Nitro Enclaves reproduce each other's reference PCRs from built-in data alone. Our solution is architecture-independent, requires neither a TTP nor externally supplied reference values, and works with existing attestation stacks unchanged.

cs.CR↗
arXiv2026

A Non-Formulable Theorem: A Fundamental Limit of Finite Syntactic Systems and Its Consequences for Security and AI

For every coherent and sufficiently expressive finite syntactic system S, we prove the existence of at least one theorem that S cannot produce autonomously. The result is a metatheorem: it proves the existence of a theorem, and applies to every finite syntactic system - security mechanisms, AI systems, formal verifiers, legal systems, economic models, and the formal system in which it is itself proved.

cs.CR↗