PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Tadd Mao, Tianjun Zhong, Dhruva Arekar, Yuming Feng, One An, Jiani Huang, Xujie Si, Ziyang Li

arXiv:2608.15432v1cs.AI

TL;DR

Faithful formalization lacks a precise, checkable account of whether formal proofs reflect natural-language reasoning. Pistis addresses this with oracle-guided, structure-preserving proof search, producing stronger Euclid formalizations that can also surface errors and gaps.

  • Problem

    Faithful formalization lacks a precise, checkable notion of whether formal proofs preserve natural-language reasoning, limiting argument-level proof checking.

  • Method

    Pistis segments natural-language proofs and uses OrderDecompose to fill ordered subgoals while preserving structure and citation dependencies, with refutation search for unclosed or erroneous steps.

  • Results

    45/45 runs succeed across 15 propositions, while the baseline solves 6 and times out on 29/45 runs within 12 hours.

  • Takeaways & Limitations

    Pistis produces more faithful, faster-compiling Euclid proofs and can accept or refute human- and AI-written arguments while surfacing genuine errors.

  • Takeaways & Limitations

    The study is limited to Euclidean geometry in System E, relies on a human or LLM oracle, and uses conditions that are necessary but not sufficient to capture full authorial intent.

Abstract

from arXiv · show

In formal verification, both the autoformalization of statements and automated proof search have been studied extensively. While automated proof search can produce a formal proof that compiles, the generated proof does not necessarily reflect how the natural-language argument arrives at its conclusion--a property we refer to as faithfulness. With faithfully formalized proofs, one can check the reasoning behind a human- or AI-written argument, and assist mathematicians in formalizing their proof sketches. However, it is particularly challenging due to misalignment of formal proof tactics and natural language reasoning. In this work, we rigorously describe a set of five necessary conditions a faithful formal proof must satisfy, and introduce Pistis, an agentic, oracle-guided proof search that produces formal Lean proofs that satisfy them. At its core is a novel faithfulness-preserving divide-and-conquer search, which we name OrderDecompose, that tracks citation dependencies and blocks unfaithful shortcuts, paired with a refutation search, that surfaces gaps and errors in the natural language proof source. OrderDecompose completes proofs that baselines cannot close even within a 12-hour budget, and its artifacts compile over 33$\times$ as fast as prior work's. We apply Pistis on the first three books of Euclid's Elements, producing high-quality artifacts containing faithful formal proofs. Under a blinded human study and an LLM-as-a-judge protocol on rigorous rubrics, Pistis-generated proofs are favored over prior works--2.89$\times$ and 5.2$\times$ as often by human reviewers and the LLM judge, respectively. It further uncovers gaps in Euclid's proofs and their translation, and can accept or refute natural language proofs written by humans or AI, demonstrating that faithful formalization is useful as a proof-checking tool.

1 Introduction

The introduction frames faithful formalization as argument-level checking rather than mere proof compilation, and presents Pistis as an oracle-guided, structure-preserving approach demonstrated on Euclid’s Elements. It highlights faithfulness challenges, efficient proof search, and empirical evidence that Pistis produces higher-quality artifacts while exposing gaps and citation errors.

  • Motivation: Faithful formalization checks whether the formal proof reflects the natural-language argument, localizing holes instead of silently hiding them through automation.It enables validation or refutation of natural-language proofs and supports turning informal sketches into formal artifacts.
  • Challenges: Faithfulness is difficult because tactics and mathematical sentences are misaligned, omitted informal steps must be filled, and no precise checkable notion previously existed.The introduction identifies three obstacles: source-target misalignment, omitted steps, and the lack of a precise definition.
  • Method: Pistis maps natural-language proofs into faithful structures, then uses OrderDecompose to close stratified sub-goals individually while preserving the top-level proof structure.The Map Stage uses an oracle, while the Fill Stage provides hierarchical decomposition, efficient compilation, and feedback.
  • Evaluation: 33× faster compilation and 2.89× more frequent human preference over LeanEuclid are reported for Pistis artifacts evaluated on Books I–III of Euclid’s Elements.The evaluation covers 92 propositions and 127 blinded reviews across four criteria.
  • Findings: Pistis surfaces gaps and refutes erroneous natural-language proofs, including 2 genuine citation mistakes in the translated Elements text.The stated contributions also include at least 52 identified gaps in the source material or its translation.

2 Motivating Example

Euclid’s simple Proposition I-6 proof shows that faithful formalization must mirror the natural-language argument, including its contradiction structure, cited propositions, and implicit deductions. The example contrasts valid but unfaithful shortcuts with a line-by-line formalization that makes Euclid’s hidden reasoning explicit.

  • Motivating example: Formalizing Proposition I-6 faithfully requires discharging an implicit without-loss-of-generality step and several unstated deductions despite its short, simple natural-language argument.The proposition states that a triangle’s equal angles subtend equal sides.
  • Faithfulness: A faithful proof mirrors each natural-language sentence step by step, in the same order and under the assumptions that sentence invokes.Lean may treat distinct proofs of the same proposition as interchangeable, even when their reasoning differs.
  • Faithfulness requirements: For I-6, faithfulness requires following Euclid’s contradiction path, constructing D, applying cited propositions at their stated points, and making the WLOG step explicit.The proof must use Proposition I-3 for the construction and Proposition I-4 for triangle congruence.
  • Unfaithful and partly faithful proofs: A symmetry-based proof is valid but unfaithful, while prior work’s partly faithful proof proves both WLOG cases directly and leaves many sentences unmapped.The shortcut reflects triangle ABC across the axis through A and reconstructs none of Euclid’s steps.
  • A faithful proof: Pistis’s faithful proof recognizes contradiction, uses `wlog` to discharge Euclid’s implicit symmetry gap, names intermediate subgoals, and closes the argument with `exact`.Its formal steps map to Euclid’s sentences, including the explicit WLOG reasoning and the final contradiction discharge.

3 Methodology

Pistis formalizes natural-language proofs as structured, faithfulness-constrained Lean artifacts rather than arbitrary compilable proofs. Its map-and-fill workflow uses oracle checks, recursive OrderDecompose search, and refutation or gap detection to preserve proof structure and diagnose failures.

  • Problem definition: Pistis takes a Lean-formalized proposition, its natural-language proposition and proof, and axioms as input, then outputs a structured formal proof aligned with segmented natural-language reasoning.The output records formal proof steps, natural-language segments, assumption and assertion mappings, and formalized content.
  • Problem definition: Faithfulness imposes necessary structural conditions beyond Lean soundness, while remaining insufficient to capture all implicit authorial intent.The conditions constrain proof structure, and exact mirroring is unattainable because formalization must fill omitted gaps.
  • Pistis workflow: Pistis separates formalization into a map stage that builds an oracle-checked template with sorry placeholders and a fill stage that closes its formal subgoals.The map stage uses LLM agents to establish the faithfulness conditions other than soundness and citation; oracle feedback prompts revisions when checks fail.
  • Pistis workflow: OrderDecompose proves subgoals in order using recursive divide-and-conquer decomposition, retaining proposed helper lemmas only when they are sufficient and suppliable.Its recursive Decomp function first attempts direct closure under a 30-second SMT budget, then searches for and recursively proves intermediate lemmas.
  • Proof diagnosis: Pistis distinguishes acceptance, refutation, and gaps: acceptance certifies no contradiction, whereas refutation formally exhibits a false assertion or an assertion that does not follow from the premises.Gaps are missing non-contradictory steps, detected through fill-stage failures or unclosed formal assumptions.

4 Evaluation

Evaluation across Euclid’s first three books finds that Pistis produces more faithful formalizations, completes more proofs at lower cost, compiles substantially faster, and exposes gaps in source proofs and translations. These results come from blinded human review, LLM judging, ablation studies, cold-compilation experiments, and corpus-wide gap analysis.

  • Faithfulness: Human reviewers favored Pistis across all evaluated dimensions, with higher mean step fidelity than LeanEuclid (4.52 vs. 3.68).The study randomly sampled 30 of 48 Book I propositions and presented anonymized formalizations for interactive inspection.
  • Faithfulness: Pistis was preferred in 63.0% of mathematical-transparency comparisons, 73.2% of textbook-representation comparisons, and 62.2% of overall-preference comparisons.Proposition-level results show these gains were broadly distributed rather than concentrated in a few propositions.
  • Faithfulness: LLM-as-judge evaluation consistently favored Pistis over the baselines across five faithfulness subcategories and all three books.The rubric measured object correspondence, proof step coverage, proof structure fidelity, cited dependency fidelity, and assumptions and side conditions on a 5-point scale.
  • OrderDecompose ablation: 45/45 Pistis runs solved all 15 ablation propositions, while the bare-LLM baseline solved 6 and timed out on 29/45 runs; successful proofs cost $15.6 versus $28.8.The baseline used the same model and agentic framework but removed Pistis’s skills, scripts, hooks, and persistent memory, with a 12-hour budget.
  • Compilation speed: Pistis compiled all 48 Book I propositions in 13.3 minutes, over 33× faster than LeanEuclid’s 7.3+ hours, which compiled 41 propositions.Cold compilation was repeated over three runs with a one-hour per-proposition timeout.
  • Refutation and gap finding: Across Books I–III, Pistis marked 33 assumption gaps, 2 confirmed citation mistakes, and 17 other generic gaps, including a translation’s citation of I-9 instead of I-10.The cited error concerns bisecting a straight line, whereas Proposition I-9 concerns bisecting an angle.

5 Related Work

Prior work spans Lean autoformalization, neurosymbolic and agentic proof systems, and faithfulness evaluation. The paper distinguishes statement-level equivalence and proof acceptance from faithfulness to the source argument.

  • Autoformalization and Euclidean Geometry: Lean autoformalization has grown from landmark formalizations and libraries into language-model-driven systems targeting increasingly large collections of mathematical statements.This work includes competition and textbook statements, repositories, and long-context settings.
  • Neurosymbolic and Agentic Approaches: Neurosymbolic programming combines neural facts with symbolic reasoning, while agentic coding frameworks establish tool-equipped agents and hierarchical searches decompose goals into tractable subgoals.Unlike faithfulness-preserving search, hierarchical decomposition accepts any independently closed subgoals that close the theorem.
  • Faithfulness: Statement-level faithfulness evaluates semantic equivalence with the source, but this does not constrain which well-typed proof term inhabits the formal goal.Proof-level evaluation such as LeanEuclid measures Lean acceptance and edit distance to a hand repair.

6 Conclusion and Future Works

Pistis formalizes natural-language proofs into faithful Lean proofs, compiles them efficiently, and can accept or refute human- and AI-written arguments. The study is limited to Euclidean geometry and oracle supervision, motivating extensions beyond geometry and reduced reliance on supervision.

  • Conclusion: Pistis formalizes natural-language proofs into Lean proofs satisfying five necessary faithfulness conditions.The system was applied across three books of Euclid’s Elements.
  • Conclusion: Pistis produces more faithful proofs than prior work, compiles faster, and surfaces genuine errors in human- and AI-written arguments.It can accept or refute those arguments as part of its proof-checking capability.
  • Future Work: Future work will extend faithful formalization beyond Euclidean geometry and reduce reliance on supervision.The current faithfulness conditions are necessary but insufficient to capture an author’s full intent.
  • Limitations: The study is limited to Euclidean geometry in System E, which cannot express some Elements propositions.Pistis also relies on a human or LLM oracle to certify faithfulness.

A Pistis Implementation Details … B.1 Why Refutation Creates a Logical Contradiction

The implementation connects Pistis’s abstract methodology to executable Lean artifacts through structured map and fill stages that enforce faithfulness and ordered proof search. Its refutation procedure turns rejected proof claims into contradictions under explicit logical assumptions.

  • A Pistis Implementation Details: Pistis’s implementation explains how abstract methodology components, including formal(·) and OrderDecompose enforcement, are realized in code.The section is explicitly intended to connect the main paper’s abstract methodology to its implementation.
  • A.1 How Objects are Implemented: The map artifact represents ordered natural-language steps, assertions, assumptions, formal types, and helper subgoals in a single Lean file.The ordered string literals enforce Order by construction, while helper have steps bridge sentence-level subgoals.
  • A.2 Map Stage Details: The map stage splits the proposition into an ordered, atomic, coverage-preserving list, then checks coverage, order, and oracle-validated faithfulness before filling proofs.The split is checked byte-for-byte against the source, and saved objects are protected from silent alteration.
  • A.3 Fill Stage (OrderDecompose) Details: The fill stage operationalizes OrderDecompose through skills, restricted build tools, and hooks that prevent skipping uncertified earlier steps.The agent cannot write later step files before the latest checked step, and every build is routed through checkable tools.
  • A.3 Fill Stage (OrderDecompose) Details: The resume mechanism preserves already-proven steps because ordered dependencies exclude later steps, requiring reproof only from a corrected map step onward.check_step.py records completed steps, enabling continuation without restarting the proof.
  • B Accept, Refute, and Gaps: The paper validates formal refutation methods as a way to accept, refute, and investigate gaps in natural-language proofs.The surrounding section introduces validation of formal refutation methods before discussing gaps in greater detail.
  • B.1 Why Refutation Creates a Logical Contradiction: Refutation yields False when a rejected assertion contradicts the proof’s derived assertion or when an existential counterexample contradicts the universally derived implication.In case A, the proof derives ϕk while refutation derives ¬ϕk; in case B, the proof establishes ∀v1, ..., vk, (α →ϕk), contradicting an existential negation.

B.2 Assumption Gap Implementation Details · B.3 Citation Gap

The implementation details define how Pistis detects and records assumption gaps, while citation gaps are explicitly suppressed when citations are erroneous or out of scope. Across 92 proofs, 311 assumptions were materialized, 33 marked as gaps, and seven citation-gap tags used in Book III.

  • B.2 Assumption Gap Implementation Details: The assumption-gap stage tries rfl, assumption, simp, linarith, nlinarith, and euclid_finish sequentially, marking an unresolved assumption with @assumption_gap and leaving sorry.euclid_finish is essentially an SMT solver.
  • B.2 Assumption Gap Implementation Details: The gap measure treats assumptions as claims that should already be proven, and regards the automated tactics as sufficiently powerful for unresolved gaps to be trustworthy.The rationale is that assumptions are not new steps to prove.
  • B.2 Assumption Gap Implementation Details: 311 assumptions were materialized across 92 proofs, with 33 marked as gaps and passed to the fill stage: 11 in Book I, 5 in Book II, and 17 in Book III.The gap counts are reported by book.
  • B.3 Citation Gap: A citation gap is a cited proposition that the Citation check cannot satisfy, and it is marked with -- @suppress_deps_check "reason" so check_faithful.py skips that citation.This mechanism records an explicit exception rather than silently treating the citation as satisfied.
  • B.3 Citation Gap: Citation-gap suppression is used when the source edition contains an actual citation mistake or when the citation points to a proposition omitted from scope, with 7 tags used across Book III.The omitted propositions are among the Book III propositions left out of scope.
  • B.3 Citation Gap: For sentence 1.6.9 of Proposition 6, the map stage leaves step9 as sorry for missing steps κ1, . . . ,κt, while the fill stage replaces it with a backing-lemma call.The filled proof body uses euclid_apply (helper_1_6_step9 ...).
  • B.3 Citation Gap: The agent workflow runs faithful-split and faithful-map in the map stage, followed by faithful-prove in the fill stage.These skills are listed as prompt files under .claude/skills/.

B.4 Generic Gap Implementation Details

Pistis identifies generic gaps in Euclid’s reasoning when OrderDecompose cannot close a step and an oracle confirms the failure is neither an assumption nor mapping issue. These gaps are marked in Lean comments, including a missing case in Book III Proposition 35, although judgments about what constitutes a gap remain subjective.

  • Generic gap identification: Generic gaps are marked with -- @euclid_gap: <why> when OrderDecompose returns False and the oracle confirms a genuine reasoning gap rather than an M or mapping failure.Ordinary System-E plumbing is not treated as a gap.
  • Example: Book III Proposition 35: In Book III Proposition 35, Euclid omits the case where one intersecting line passes through the circle’s centre and the other does not, so the formalization adds and tags it as a gap.The original proof covers only the cases where both lines, or neither line, pass through the centre.
  • Judgment criteria: What qualifies as a generic gap is subjective and reflects the authors’ judgments.The paper distinguishes these judgments from ordinary System-E plumbing, which is not considered a gap.

C Human Evaluation Protocol … D LLM as a Judge

The evaluation combines a blinded human review of anonymized formalization pairs with an LLM-as-judge protocol. Humans assess step fidelity and pairwise preferences, while two LLM judges score faithfulness across five rubric-defined dimensions.

  • C Human Evaluation Protocol: Reviewers used a custom web interface supporting an interactive tutorial, independent step-fidelity scoring, and final pairwise preferences for anonymized formalization pairs.Only the formal Lean proofs were compared to ensure fairness.
  • C.1 Step Fidelity: Step fidelity was rated on a 0–5 scale according to how well each Lean proof preserves the textbook proof’s mathematical route.The full scoring rubric appears in Table 5.
  • C.2 Pairwise Preferences: For each proposition, reviewers answered three seven-tier pairwise questions, with the center indicating no preference and distance indicating preference strength.The criteria are summarized in Table 6.
  • C.3 Evaluation Interface: The interface displayed the textbook theorem and proof beside one formalization at a time before reviewers assigned a detailed 0–5 step-fidelity score.Reviewers first completed a tutorial covering the task, anonymized presentation, and interface controls.
  • C.3 Evaluation Interface: Reviewers then reported pairwise preferences for mathematical transparency, textbook representation, and overall preference.These judgments followed examination of each formalization.
  • D LLM as a Judge: Two LLM judges, Claude Opus 4.6 and GLM-5, independently scored each formalization on five faithfulness dimensions using strict 0–5 rubrics.The dimensions are object correspondence, proof-step coverage, proof-structure fidelity, cited-dependency fidelity, and assumption/side-condition fidelity.
  • D LLM as a Judge: The LLM judges evaluated mathematical faithfulness to the textbook rather than general elegance, maintainability, brevity, annotation quality, or code style.Formal encoding overhead and other routine formalization necessities were not to be penalized.
  • D LLM as a Judge: Each judge provided brief justifications citing the Lean code and textbook proof, then output five integer scores in a fixed angle-bracket order.The required order was object correspondence, proof-step coverage, proof-structure fidelity, cited-dependency fidelity, and assumption/side-condition fidelity.

E Ablation Study Details · F Compile Performance Details · G Further Refutation Examples

The ablation isolates OrderDecompose from a standard proof-search arm under controlled, anti-cheating conditions, while compile benchmarks compare faithful decomposed proofs with prior proofs. Released examples also demonstrate refutation of flawed proofs and acceptance of valid alternatives to Euclid’s proofs.

  • E Ablation Study Details: The ablation compares the full OrderDecompose arm with an ablated arm using the same Opus 4.8 model.Each arm runs separately in its own worktree and branch, with memory wiped before every run.
  • E Ablation Study Details: The evaluation forbids repository-external reading and git use, with violations automatically failing the attempt.These restrictions are stated to agents and suspicious behavior is checked afterward because proven answers exist in git history.
  • E Ablation Study Details: The ablated arm receives explicit output requirements and cannot modify the original formal claim, preserving a fair comparison.Prompts require filling every sorry, retaining theorem and claim types, and citing anything Euclid cites.
  • E Ablation Study Details: The ablated arm typically attempts the entire proof at once, whereas OrderDecompose builds small step lemmas in fast scoped batches.The transcripts show the ablated strategy repeatedly triggering massive builds, while the full method makes steady in-order progress.
  • F Compile Performance Details: Compile benchmarks measure per-proposition wall-clock time for faithful decomposed proofs versus Murphy et al. (2024), with both proving the same proposition_N.Each proposition is compiled cold after wiping .lake/build, while cached Mathlib packages remain untouched.
  • F Compile Performance Details: The ablation compile-time companion evaluates artifacts from the ablated arm and OrderDecompose using the same procedure on an AMD EPYC 9754 128-core node.Drivers, hardware metadata, and result CSVs are provided in the reproducible-experiments archive.
  • G Further Refutation Examples: Released refutation examples include a type B case, alongside accepted proofs that differ from Euclid’s proof while establishing the same statement.These examples illustrate that the methodology can formally determine which alternative proofs to accept or refute.

H Limitation Details

The formalization covers 30 of Book III’s 37 propositions, while seven require new System E primitives outside the project’s scope. Pistis also depends on oracle validation, with proof quality potentially degrading when an LLM replaces a human oracle.

  • Skipped propositions: 30 of Book III’s 37 propositions are completed; the remaining seven require new System E primitives and are out of scope.Props. 24 and 26–31 require circle superposition, arc-length, or horn-angle primitives.
  • Reliance on the oracle: Pistis requires a human or automated oracle to validate Atomicity and Atomic Faithfulness during the map stage.The system is oracle-guided rather than fully autonomous.
  • Reliance on the oracle: LLM-oracle use may degrade proof quality compared with a human oracle, making reduced oracle dependence a natural future direction.The methodology minimizes human-oracle effort but does not eliminate oracle involvement.
Loading 2608.15432v1…