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

> Pistis achieves faithful formalization of Euclid's proofs by enforcing five checkable conditions, beating prior work 2.89x in human preference and finding genuine citation errors.

- **Source:** [arXiv](https://arxiv.org/abs/2608.15432)
- **Published:** 2026-08-22
- **Permalink:** https://picx.dev/p/0F9mM1
- **Whiteboard:** https://picx.dev/p/0F9mM1/image

## Summary

# 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

| Name | Condition | Checked by |
|------|-----------|------------|
| **COVERAGE** | $s_1, \ldots, s_n$ concatenate, in order, to the NL proof $P_{\mathrm{NL}}$ | Script |
| **ATOMICITY** | $s_i$ has a single assertion $\mathrm{assert}(s_i)$, with assumptions $\mathrm{assumps}(s_i)$ | Oracle |
| **ATOMIC FAITHFULNESS** | $\forall a \in \mathrm{assumps}(s_i), \mathrm{formal}(a)$ is faithful, and $\mathrm{formal}(\mathrm{assert}(s_i))$ is faithful | Oracle |
| **ORDER** | $(\mathrm{formal}(\mathrm{assert}(s_1)), \ldots, \mathrm{formal}(\mathrm{assert}(s_n)))$ is a subsequence of $(\phi_1, \ldots, \phi_N)$ | Script |
| **CITATION** | Given $\mathrm{formal}(\mathrm{assert}(s_i)) = \phi_k$, every NL proposition $p$ cited in $s_i$ has $\mathrm{formal}(p) \in \{\phi_j : j < k\}$ | Script |
| **SOUNDNESS** (separate) | $\mathrm{formal}(P_{\mathrm{NL}})$ compiles in Lean with no `sorry` | Lean |

### 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):

| Metric | Pistis | LeanEuclid |
|--------|--------|------------|
| Mean step-fidelity (scale 3–5) | **4.52** | 3.68 |
| Mathematical transparency preference | **63.0%** | — |
| Textbook representation preference | **73.2%** | — |
| Overall preference | **62.2%** | — |

**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)

| Metric | OrderDecompose | LLM-only | Factor |
|--------|---------------|----------|--------|
| Coverage (pass@k) ↑ | 15/15 (100%) | 6/15 (40%) | **2.5×** |
| Total cost / success ($) ↓ | **$15.6** | $28.8 | 1.8× |

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

---

_Markdown view of https://picx.dev/p/0F9mM1, served by PicX — AI-generated visual whiteboard summaries of research papers._