













Authors:Mihai Prunescu (Research Center for Logic, Optimization and Security (LOS), Faculty of Mathematics and Computer Science, University of Bucharest, Simion Stoilow Institute of Mathematics of the Romanian Academy)
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.
From: Mihai Prunescu [view email] [via EPTCS proxy]
[v1]
Thu, 26 Jun 2025 09:20:21 UTC (13 KB)
[v2]
Mon, 30 Jun 2025 14:13:27 UTC (13 KB)
[v3]
Wed, 27 Aug 2025 15:25:51 UTC (14 KB)
[v4]
Tue, 16 Sep 2025 12:50:44 UTC (31 KB)
[v5]
Fri, 4 Sep 2026 17:08:09 UTC (16 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。