Summary of "Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs"

Summary (Overview)

• Faithful formalization framework: The paper introduces Pistis, an oracle-guided proof search system that formalizes natural-language (NL) proofs into Lean proofs that faithfully mirror the original argument structure, rather than merely producing any valid proof.

• Five necessary conditions of faithfulness: The authors rigorously define COVERAGE, ATOMICITY, ATOMIC FAITHFULNESS, ORDER, and CITATION as necessary (though not sufficient) conditions that a faithful formal proof must satisfy.

• Novel search algorithm: The OrderDecompose algorithm performs ordered, hierarchical, divide-and-conquer proof search that tracks citation dependencies, blocks unfaithful shortcuts, and closes stratified sub-goals individually rather than the theorem as a whole.

• Superior empirical results: Pistis-generated proofs are favored 2.89× more often by human reviewers and 5.2× more often by an LLM judge over prior work (LeanEuclid), compile 33× faster, and complete all 15 benchmark propositions within budget where a bare-LLM baseline fails 60% of the time.

• Proof checking capability: Pistis uncovers 52 gaps in Euclid's Elements including 2 genuine citation mistakes in the Fitzpatrick translation, and can formally refute erroneous NL proofs written by humans or AI.

---

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses a critical gap in autoformalization research: while formalizing statements has been extensively studied, formalizing proofs is often left to automated proof search that produces any closing tactic sequence—regardless of whether it reflects the natural-language argument's reasoning structure. The authors define faithfulness as the property that a formal proof mirrors the NL proof step-by-step, with each formal step corresponding to a specific NL sentence in the same order.

The motivation is practical, not just aesthetic:

• A faithful formalization lets us check correctness at the level of the argument, certifying that the reasoning as written is valid.
• When an argument has a hole, a faithful attempt localizes the gap rather than silently papering over it with proof automation.
• Faithful proofs help mathematicians transform informal sketches into formal artifacts that remain legible for study and teaching.

Why Faithfulness Is Hard

Three fundamental challenges are identified:

1. Intrinsic misalignment: Lean/Rocq advances via tactics (transforming proof states), whereas NL proofs advance via sentences of mathematical reasoning.
2. Implicit steps: NL proofs omit steps humans find obvious but formal systems explicitly demand; faithful proofs must fill these gaps without altering the mathematical proof structure.
3. Lack of precise notion: The field lacks a checkable definition of proof faithfulness—prior evaluations rely on coarse proxies like LLM-as-judge semantic matching.

System E and Euclidean Geometry

The work builds on System E (Avigad, Dean, and Mumma 2009), a formal system faithfully modeling Euclid's proofs, and LeanEuclid (Murphy et al. 2024), which implements System E in Lean with SMT for diagrammatic reasoning. The axioms of System E are denoted $\Delta$.

---

Methodology

Problem Definition

Input: $\langle P_{\mathrm{NL}}, \mathrm{formal}(P_{\mathrm{NL}}), F_{\mathrm{NL}}, \Delta \rangle$ where:

• $P_{\mathrm{NL}}$ is an NL proposition
• $\mathrm{formal}(P_{\mathrm{NL}})$ is its Lean formalization, of form $\alpha \Rightarrow \beta$ (hypotheses $\alpha = \alpha_1 \wedge \ldots \wedge \alpha_m$, free variables $v_1, \ldots, v_k$)
• $F_{\mathrm{NL}}$ is the NL proof
• $\Delta$ is the set of System E axioms

Output: A tuple $\langle \bar{\phi}, \bar{s}, \mathrm{assumps}(\cdot), \mathrm{assert}(\cdot), \mathrm{formal}(\cdot) \rangle$ containing the formal proof steps, NL segmentation, and mapping between them.

The Five Necessary Conditions of Faithfulness

Pistis Architecture: Two Stages

Map Stage: LLM agents create a faithful formal template $\bar{\phi'}$ with sorry placeholders, segmenting the NL proof into steps and establishing the mapping. An oracle checks ATOMICITY and ATOMIC FAITHFULNESS, with iterative feedback until satisfied.

Fill Stage: Uses OrderDecompose to prove each $\phi'_i$. The algorithm:

Algorithm 1: ORDERDECOMPOSE
Require: Hypothesis τ, Subgoals ψ₁,…,ψₙ, conclusion γ, LLM M
1: for i = 1, …, m do  ▷ prove each subgoal ψᵢ in order
2:   repeat  ▷ re-attempt ψᵢ until it passes every check
3:     if GIVEUP(τ, ψᵢ, M) then return False
4:     (η₁, …, ηₘ) ← CREATEHYPOTHESIS(τ, ψᵢ, M)
5:     SP ← ⋀ⱼ INCONTEXT(ηⱼ)
6:     P ← DECOMP((η₁, …, ηₘ), ψᵢ, M)
7:   until SP ∧ P ∧ CITATION(ψᵢ) ∧ UNCHANGED(M {φ̄'})
8: end for
9: return True

The recursive DECOMP function:

• Attempts direct SMT solving within a 30-second budget ($\Delta \cup \{\cup_j \eta_j\} \vdash_{\mathrm{SMT-30s}} \nu$)
• If that fails, asks the LLM to propose intermediate lemmas $h^{(j)} \to \omega^{(j)}$
• Keeps lemmas only if sufficient (SF: close the goal) and suppliable (SP: derivable from context)
• Recurses on each helper lemma

Acceptance, Refutation, and Gap Identification

• Refute: Derive a logical contradiction from the proof. Either (1) an asserted step is false under premises ($\Delta \cup \{\alpha\} \vdash \neg \mathrm{formal}(\mathrm{assert}(s_i))$), or (2) an asserted step doesn't follow from premises (there exists a configuration satisfying hypotheses but violating the assertion).
• Gap: A missing step that doesn't create a contradiction. Detected via (1) LLM flagging during fill stage, or (2) automatic assumption-gap detection where unclosed have statements are marked.

---

Empirical Validation / Results

RQ1: Faithfulness of Generated Proofs

Double-blind Human Evaluation (14 formal-methods researchers, 127 completed assignments, 254 step-fidelity ratings, 381 pairwise preferences):

LLM-as-judge (5-point rubric across 5 subcategories: object correspondence, proof step coverage, proof structure fidelity, cited dependency fidelity, assumption & side conditions):

• Book I: Pistis favored 5.2× as often as LeanEuclid (26 wins, 17 ties, 5 losses)

RQ2: Fill Stage Ablation (N=15, k=3 runs each, 12-hour budget)

Pistis finishes all runs within ~3.5 hours; the baseline times out (fails) on 29/45 runs.

RQ3: Lean Compile Performance

• Pistis compiles all 48 Book I propositions; LeanEuclid compiles only 41.
• Pistis compiles all of Book I in 13.3 minutes vs. LeanEuclid's 7.3+ hours (≥33× faster).

RQ4: Refutations and Gaps Found

• 33 assumption gaps, 2 confirmed citation mistakes, 17 other generic gaps across Books I–III.
• Example citation gap: In Prop. III-1, Fitzpatrick brackets "cut AB in half" as Proposition I-9, but I-9 bisects an angle; bisecting a straight line is Proposition I-10.
• Example refutation: An LLM-generated proof of Book I Prop. 5 claiming angle CBD is a right angle was formally refuted by proving $\neg \mathrm{formal}(\mathrm{assert}(s_3))$.

---

Theoretical and Practical Implications

For Formal Verification

The paper provides the first precise, checkable taxonomy of proof faithfulness—five necessary conditions that can be partially automated (script-checked) and partially oracle-checked. This moves beyond coarse proxies like LLM-as-judge semantic matching or edit-distance heuristics.

For Mathematics

• Proof checking: Pistis demonstrates that faithful formalization is useful as a proof-checking tool, not just a verification oracle. It can accept valid proofs, refute erroneous ones, and localize gaps in human or AI-written arguments.
• Translation quality: The discovery of genuine citation mistakes in the Fitzpatrick translation of Euclid shows the value of formal verification for historical mathematical texts.
• Pedagogical value: Faithful proofs preserve the legibility of the original argument, making formal artifacts useful for teaching and mathematical communication.

For AI-Assisted Proof

The ablation study shows that structure matters: a bare LLM with the same model and agentic framework fails 60% of the time within budget, while OrderDecompose's ordered hierarchical decomposition succeeds 100% of the time at lower cost. This suggests that proof search benefits from respecting the argument structure rather than treating the theorem as a monolithic goal.

---

Conclusion

Main Takeaways

Pistis demonstrates that faithful formalization is achievable and practical for Euclidean geometry. The key insight is that faithfulness becomes tractable through segmentation: splitting the NL proof into structural sub-goals, then using ordered, hierarchical proof search (OrderDecompose) that enforces citation dependencies and blocks unfaithful shortcuts.

Future Directions

1. Extending beyond Euclidean geometry to other mathematical domains
2. Reducing reliance on supervision (human or LLM oracles for faithfulness certification)
3. Addressing the sufficiency gap: the five conditions are necessary but not sufficient—complete faithfulness (capturing author's implicit intent) remains unattainable since formal proofs must fill gaps the NL proof omits

Limitations

• Limited to Euclidean geometry expressible in System E (some Book III propositions excluded)
• Relies on human or LLM oracle for certifying faithfulness
• The five conditions, while necessary, cannot capture an author's full intent