Paper deep dive
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
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 8/22/2026, 2:16:26 AM
Summary
This paper introduces Pistis, an agentic, oracle-guided framework for the faithful formalization of natural language mathematical proofs into Lean. It addresses the misalignment between natural language reasoning and formal proof tactics by enforcing five necessary conditions for faithfulness, including atomicity, order preservation, and citation integrity. The core algorithm, OrderDecompose, uses a divide-and-conquer strategy to generate formal proofs that mirror the structure of the source argument. Evaluated on Euclid's Elements (Books I-III), Pistis produces high-quality, fast-compiling artifacts that are preferred by human reviewers and LLM judges over prior methods, while also identifying gaps and errors in the original texts.
Entities (7)
Relation Signals (6)
Pistis → appliedto → Euclid's Elements
confidence 98% · We apply Pistis on the first three books of Euclid's Elements
Pistis → uses → OrderDecompose
confidence 98% · At its core is a novel faithfulness-preserving divide-and-conquer search, which we name OrderDecompose
Pistis → targets → Lean
confidence 97% · introduce Pistis... that produces formal Lean proofs
Pistis → outperforms → LeanEuclid
confidence 95% · Pistis-generated proofs are favored over prior works... 2.89x and 5.2x as often by human reviewers and the LLM judge
OrderDecompose → enforces → Faithfulness
confidence 94% · novel faithfulness-preserving divide-and-conquer search... tracks citation dependencies and blocks unfaithful shortcuts
Pistis → detects → gaps in Euclid's proofs
confidence 93% · It further uncovers gaps in Euclid's proofs and their translation
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2608.15432v1
- Canonical: https://arxiv.org/abs/2608.15432v1
Trouble viewing inline? Open PDF directly →
Full Text
81,799 characters extracted from source content.
Expand or collapse full text
Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs Tadd Mao 1 , Tianjun Zhong 2 , Dhruva Arekar 2 , Yuming Feng 2 , One An 3 , Jiani Huang 3 , Xujie Si 1∗ , Ziyang Li 2∗† 1 University of Toronto 2 Johns Hopkins University 3 University of Pennsylvania ziyang@cs.jhu.edu Abstract In formal verification, both the autoformalization of state- ments and automated proof search have been studied exten- sively. While automated proof search can produce a formal proof that compiles, the generated proof does not necessar- ily reflect how the natural-language argument arrives at its conclusion—a property we refer to as faithfulness. With faith- fully 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 de- scribe 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 er- rors 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× 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× and 5.2× 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 We are not trying to meet some abstract production quota of definitions, theorems and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about mathematics. On Proof and Progress in Mathematics (Thurston 1994) Autoformalization translates natural-language (NL) mathe- matics into the formal language of a proof assistant such as Lean or Rocq, where it can be checked mechanically (Wu ∗ These authors contributed equally. † Corresponding author. et al. 2022; de Moura and Ullrich 2021). Most work targets the formalization of statements (Li et al. 2024; Azerbayev et al. 2023), yet the formalization of proofs is often left to automated proof search, which hunts for a sequence of proof tactics that closes the goal. As a result, proof faithful- ness, whether the formal proof reflects how the NL argument reaches its conclusion (Avigad, Dean, and Mumma 2009; Cabral et al. 2025), is largely overlooked. Faithfulness is not a stylistic nicety; it is what makes a formal proof useful beyond a yes or no verdict. A faithful formalization lets us check correctness at the level of the ar- gument, certifying that the reasoning as written in NL is valid. When the argument has a hole, a faithful attempt localizes it rather than silently papering over it with proof automa- tion, letting us validate or refute a given NL proof. It helps mathematicians turn informal sketches into formal artifacts that still resemble what they wrote, and it keeps those arti- facts legible for study and teaching, since each NL reasoning step maps directly to a formal step. For a proof to contribute to the broader field, legibility is only the starting point; the community must also recognize, digest, and build upon its argument. A human author can convey the insights behind a proof, while current AI tools remain black boxes (Tao 2026). Achieving faithfulness is hard for three reasons. First, the target is intrinsically misaligned with the source: a proof assistant like Lean or Rocq advances by tactics, which trans- form proof states, whereas an NL proof advances by sen- tences of mathematical reasoning. Second, NL proofs may omit steps a human finds obvious but the formal system explicitly demands, so a faithful proof must fill these gaps without altering mathematical proof structures. Third, the field lacks a precise, checkable notion of what proof faith- fulness is (Murphy et al. 2024; Cabral et al. 2025): prior evaluations lean on coarse proxies such as LLM-as-a-judge semantic matching (Lu et al. 2024; Poiroux et al. 2025; Yu et al. 2025), which cannot serve as a certification. In this work we introduce Pistis 1 , a framework that for- malizes an NL proof into a faithful Lean proof, which we demonstrate in Euclidean geometry. Our key insight is that faithfulness becomes tractable once the proof is segmented: rather than searching for a single proof term that closes the whole theorem, we split the NL proof into structural formal 1 From the Greek pistis (π ́ιστις), meaning “faith” or “trust.” arXiv:2608.15432v1 [cs.AI] 15 Aug 2026 Euclid, Elements I-6 Statement. If a triangle has two angles equal to one another then the sides subtend- ing the equal angles will also be equal to one another. LetABC be a triangle having the angleABC equal to the angleACB. I say that sideAB is also equal to sideAC. Proof. For ifAB is unequal toAC then one of them is greater. 1LetAB be greater.2And letDB, equal to the lesser AC, have been cut off from the greaterAB Proposition I-3.3Therefore, . . . , and the angleDBC is equal to the angleACB.6 Thus, the baseDC is equal to the base AB,7and the triangleDBC will be equal to the triangleACBProposition I-4, the lesser to the greater.8The very no- tion (is) absurd Common Notion 5 . 9 Thus, AB is not unequal toAC.10Thus, (it is) equal.11Thus, if a triangle has. . .12□ Formal statement in Lean (given) theorem proposition_6 : ∀ (a b c : Point) (AB BC AC : Line), formTriangle a b c AB BC AC ∧ (∠ a:b:c =∠ a:c:b) → |(a–b)| = |(a–c)| Unfaithful by euclid_intros euclid_apply (superposition a b c a c b AB BC AC AC) as (b’,c’,BC’,AC’) euclid_finish Partly faithful by euclid_intros by_contra by_cases |(a–b)| > |(a–c)| · -- the first case euclid_apply (prop_3... ) as d euclid_apply (line d c) as DC euclid_apply prop_4... euclid_finish · -- the second case euclid_apply (prop_3... ) as d ... euclid_finish Faithful (ours) by euclid_intros have habsurd: ¬(|(a–b)|̸=|(a–c)|) :=... wlog gt: |(a–b)| > |(a–c)| generalizing b c AB BC AC with Hsym ·... -- prove symmetry gap · have s3: between b d a ∧ |(b–d)|=|(a–c)| :=... ... -- steps 4-5 have s6:∠d:b:c =∠a:c:b ... -- steps 7-9 have s10: ¬(|(a–b)|̸=|(a–c)|) := by exact habsurd have s11: |(a–b)| = |(a–c)| := by_contra... exact s11 A BC D 12 3 12 3 6 10–11 Figure 1: Motivating example (Book I, Prop. 6). Left: Euclid’s statement and natural-language proof, its sentences marked1–12 at the points where our method splits them; citations appear as pills (e.g.Proposition I-3); the accompanied diagram illustrates the corresponding geometric constructions. Top right: the formal statement we are given in Lean. Bottom right: three ways to fill the proof, from unfaithful to faithful. Left: a single superposition that discards Euclid’s argument; middle: prior work (Murphy et al. 2024), where one euclid_finish collapses many of Euclid’s sentences; and right: our faithful proof, where each NL sentence maps to exactly one formal step matchingkon the left. sub-goals. This process is accomplished by the Map Stage of Pistis, where an agent works with an oracle to ensure the faithfulness of the mathematical proof structure. After mapping a faithful proof structure, Pistis invokes a Fill Stage algorithm, OrderDecompose, which is a novel proof search backed by LLM agents. Its key component is an ordered, hierarchical decomposition that closes stratified sub-goals individually rather than the theorem as a whole, giving both efficient compilation and a tight feedback loop. This is further accompanied by 1) a proof-structure preser- vation mechanism that guards against the rewriting of the top-level faithful structure, 2) agentic tools that enforce faith- ful citation dependencies so each supporting proposition is applied exactly where the argument invokes it, and 3) when a sub-goal will not close, refutation techniques such as proving the negated sub-goal or searching for a counterexample. We evaluate Pistis on the first three books of Euclid’s Elements (92 propositions), producing new Lean artifacts. Beyond extending the previously formalized single book of LeanEuclid (Murphy et al. 2024), we argue our artifact is of higher quality. They compile at least 33× as fast, and on four criteria across 127 blinded reviews, human evaluators favor Pistis-generated proofs 2.89× as often as the already faithfulness-claiming LeanEuclid. An LLM-as-a-judge pro- tocol scoring a rigorous five-dimension rubric agrees, fa- voring Pistis over LeanEuclid by a 26:5 win–loss ratio on Book I. An ablation shows that OrderDecompose finishes within a fixed budget, produces 2.5× as many completed proofs as a state-of-the-art LLM-agent baseline while being 80% more cost-effective. Finally, Pistis faithfully surfaces gaps and refutes erroneous NL proofs, including 2 genuine citation mistakes in the Elements translated text. Contributions. In summary, we contribute: • new Lean artifacts of faithfully formalized proofs for Books I–I of Euclid’s Elements; • a taxonomy of five necessary conditions of faithfulness a formal proof must satisfy; • Pistis, an oracle-guided methodology for faithful proof formalization, built on the OrderDecompose search; • a thorough evaluation on faithfulness, cost efficiency, and compilation time, including a double-blind human expert review, showing improvements over prior methods; and • the identification of at least 52 gaps in Elements proofs including 2 genuine mistakes in the translation. 2 Motivating Example Consider Proposition 6 of Book I (I-6): if a triangle has two equal angles, the sides subtending them are equal (Fig. 1). Problem-wise, we are given its natural-language (NL) proof as a string and its statement already formalized in Lean; our task is to fill in the formal proof. It appears early in Euclid’s Elements and reads as a short, simple argument. However, formalizing it faithfully already forces us to discharge an implicit without-loss-of-generality step and several unstated deductions, difficulties that compound in later propositions. Faithfulness. Lean’s kernel enforces proof irrelevance: any two proofs of the same proposition are definitionally equal (Carneiro 2019), so Lean accepts any term whose type Table 1: Conditions Pistis guarantees; all notation is defined in the Problem Definition. Faithfulness comprises the five necessary conditions of faithfulness; Soundness is separate. A free variable s i ranges over all sentences s 1 ,...,s n . script checks are automated (noM), oracle checks are by human experts, and Soundness is checked by Lean. NameConditionChecked by Coverages 1 ,...,s n concatenate, in order, to the NL proof P NL Script Atomicitys i has a single assertion assert(s i ), with assumptions assumps(s i )Oracle Atomic Faithfulness ∀a∈ assumps(s i ), formal(a) is faithful, and formal(assert(s i )) is faithfulOracle Order(formal(assert(s 1 )),..., formal(assert(s n ))) is a subsequence of (φ 1 ,...,φ N )Script CitationGiven formal(assert(s i )) = φ k , every (NL) prop. p cited in s i has formal(p)∈φ j : j < kScript Soundnessformal(P NL ) compiles in Lean with no sorryLean is the stated proposition. Therefore, all three proofs in Fig. 1 are treated as interchangeable. Yet they differ sharply in how, and whether, they follow Euclid. We call a formal proof faith- ful when it mirrors the NL proof step by step, each formal step corresponding to a specific NL sentence, in the same order, under the assumptions that sentence actually invokes. What a faithful proof for I-6 must capture. Euclid ar- gues by contradiction. A faithful formalization must therefore (a) follow this contradiction path, including the construction of D; (b) apply each cited proposition exactly where Euclid applies it, e.g. Proposition I-3 for the construction and I-4 for the triangle congruence; (c) discharge the gaps Euclid leaves implicit, in particular the without-loss-of-generality (WLOG) step his “one of them is greater. 1Let AB be greater.2” leaves unstated; and (d) justify each step from precisely the claims that step is entitled to use. Unfaithful and partly faithful proofs. The leftmost proof (unfaithful) reflects triangle ABC across the axis through A, producing a copy that is congruent, whence AB = AC. This is a valid proof, but it proves by symmetry and reconstructs none of his steps. The middle proof (partly faithful), pre- sented in prior work (Murphy et al. 2024), recovers the high- level shape, but three problems remain. First, where Euclid reasons WLOG, it instead proves both cases directly. Second, many sentences have no formal counterpart: sentence 6, for instance, is absent, and one can only guess the correspon- dence by inspecting the referenced symbols. Third, it may hide NL reasoning steps in a black-box euclid_finish tactic, which might take a different route than Euclid’s inten- tion and is non-deterministic. A faithful proof. Our proof (faithful, right) follows the NL reasoning line by line. Reading Euclid’s “the very notion is absurd” 9, we recognize an argument by contradiction and name the negated goal habsurd. Euclid never states WLOG; we infer it from “one of them is greater.1 LetAB be greater. 2 ” and make it explicit with thewlog tactic, proving the required symmetry rather than expanding both cases 2 . This discharges the symmetry gap Euclid leaves implicit; had that symmetry been false, the attempt would instead expose the gap or refute the proof outright (Sec. 4.5). We then proceed sentence by sentence, introducing each assertion 2 Without-loss-of-generality (WLOG) is a well-known source of subtle errors, since the appealed-to symmetry is not always genuine. as a named subgoal with have (stepK, shown sK in the figure), so sentences 3and6map exactly. Finally, mirroring Euclid’s conclusion in sentences10and 11 , we discharge habsurd and close the proof with exact. As we show later, the same faithful formalization, applied across the corpus, further lets us identify gaps in the Ele- ments and its translations (such as a reference to the wrong proposition), produce proofs that human readers prefer, and produce proofs that compile faster than automation-heavy alternatives. 3 Methodology In this section, we describe the problem definition of faith- ful formalization of NL proofs, including one taxonomy of necessary faithful conditions (Sec. 3.1). We then present the overview of Pistis, including its map stage, fill stage, and the main OrderDecomposition algorithm (Sec. 3.2). 3.1 Problem Definition We begin by explaining what Pistis takes as input, what it produces as output, and what conditions these satisfy. Input. Pistis takes as input ⟨P NL , formal(P NL ),F NL , ∆⟩, where P NL is an NL proposition, formal(P NL ) is its formal- ization in Lean, and F NL is an NL proof of P NL . Specifically, formal(P NL ) is of the form α → β, which reads “given the hypotheses α, the theorem concludes β.” We may also write α = α 1 ∧...∧α m to separate the larger formula of hypothe- ses into the individual hypothesis formulas α 1 ,...,α m , and free variables in α are referred to as v 1 ,...,v k ; the Appendix explains why these occur, and concrete examples in Lean. Additionally, the set of System E (Avigad, Dean, and Mumma 2009) axioms is denoted ∆ and is also part of the input. Output. While general proof search algorithms only output an arbitrary sound formal proof formal(F NL ), we argue that to ensure faithfulness, the output requires more than just the formal proof itself. In this work, we enforce a faithful proof to capture: (i) knowing each step of the formal proof φ 1 ,...,φ N (rather than the whole proof as one objectφ) so we can match these formal steps to the NL steps, (i) what we even mean by an NL step and how the NL proof is segmented into steps, (i) what is the structure within an NL step, and finally (iv) which NL step maps to which formal step. Therefore, to address the above requirements, the output of Pistis is a tuple ⟨ ̄ φ, ̄s, assumps(·), assert(·), formal(·)⟩ where: (1) ̄ φ = φ i N 1 = formal(F NL ) which is a sequence of formal steps, with each φ i derivable from the System E axioms ∆, hypotheses α and φ 1 ,...,φ i−1 . Formally ̄ φ is a proof that ∆∪α⊢ β; (2) an NL partition of F NL into steps ̄s = s 1 ,...,s n , where each NL step s i is referred to as a segment; (3) two mappings assumps(·) and assert(·), send- ing each segments i to a set of substrings ofs i in assumps(s i ) and a single substring ofs i in assert(s i ), respectively. For ex- ample, consider s i = “since P and Q, therefore R” we have assumps(s i ) = P,Q and assert(s i ) = R; (4) a mapping formal(·) that sends each assertion assert(s i ) to some φ j and each assumption in assumps(s i ) to some φ k . Conditions. Whereas a typical proof search need only soundness, i.e., Lean compilation, faithfulness demands more, and we present these additional conditions in Tab. 1. They are necessary but not sufficient: they constrain the proof’s structure while leaving aspects such as author’s im- plicit intent uncaptured. Complete faithfulness is, we argue, unattainable: since a formal proof must fill gaps the NL proof omits, a formalization mirroring the NL proof exactly would leave those gaps and hence be unsound. We therefore aim to be more faithful than prior work rather than perfectly faithful, and leave this gap to future work. 3.2 Approach Overview In order to produce a faithful formal proof satisfying the aforementioned conditions, Pistis uses a two-stage approach: a map stage, which creates a faithful and formal template with sorry placeholders, and a fill stage, which uses OrderDe- compose to close the formal goal. Map Stage. M :=⟨ ̄ φ ′ , ̄s, assumps(·), assert(·), formal(·)⟩ are produced by the map stage, where ̄ φ ′ is intended to be a subsequence of the (eventual) formal proof ̄ φ. These outputs are created by LLM agents to ensure every condition in Tab. 1 except for Soundness, and Citation, and are checked by an oracle or a script. Details of the LLM-agent and its prompting strategies are described in the Appendix. If the conditions the oracle is assigned to check are not satisfied, the oracle prompts the LLM to fix the output, and this process repeats until the oracle is satisfied. Fill stage. The fill stage proves each φ ′ i since they were left unproven (sorry) in the map stage. By “proves“ we mean for each φ ′ i , create a sequence of steps κ 1 ,...,κ t s.t. Lean com- piler is able to check that ∆∪α,φ ′ 1 ,...,φ ′ i−1 ,κ 1 ,...,κ t ⊢ φ ′ i . When the check succeeds, κ 1 ,...,κ t are added to the proof: (φ ′ 1 ,...,φ ′ N ′ ) ← (φ ′ 1 ,...,φ ′ i−1 ,κ 1 ,...,κ t ,φ ′ i ,...φ ′ N ′ ). This process is done using OrderDecompose (Alg. 1). OrderDecompose takes in hypothesesα, subgoals ̄ φ ′ , and conclusion β, along with an LLMM. It returns either True if it successfully proves all subgoals φ ′ i , or False if M decides to GiveUp. The main structure of OrderDecompose is to prove φ ′ 1 , then φ ′ 2 , until φ ′ N ′ in order (Alg. 1, line 1–9), and for each φ ′ i , does a recursive, divide-and-conquer search by decomposing it into further sub-lemmas (line 14–19) until each sub-lemma, is proven, resulting inφ ′ i to be proven. LLM executes and follows OrderDecompose in practice through skill files for general instructions, agentic hooks to prevent Algorithm 1: OrderDecompose Require: Hypothesis τ, Subgoals ψ 1 ,...,ψ n and conclusion γ s.t. ∆∪τ,ψ 1 ,...,ψ n ⊢ γ; LLMM Returns: Bool — whether the proof search succeeded 1: for i = 1,...,m do▷ prove each subgoal ψ i in order 2: repeat▷ re-attempt ψ i until it passes every check 3:if GiveUp(τ,ψ i ,M) then return False 4:(η 1 ,...,η m )← CreateHypothesis(τ,ψ i ,M) 5:SP← V j InContext(η j )▷ suppliable 6:P← Decomp((η 1 ,...,η m ),ψ i ,M) ▷ soundness 7: until SP∧ P∧Citation(ψ i )∧ UnChanged(M \ ̄ φ ′ ) 8: end for 9: return True▷ all subgoals proven, so γ follows 10: function Decomp((η 1 ,...,η n ),ν,M) : Bool 11: repeat▷ close ν directly, else decompose it 12:if ∆∪ j η j ⊢ SMT-30s ν then return True 13:if GiveUp( ̄η,ν,M) then return False 14:repeat ▷ search lemmas until sufficient & suppliable 15:(h (j) → ω (j) )← CreateLemmas( ̄η,ν,M) 16:SF← (∆∪ k η k ∪ j ω (j) ⊢ SMT-30s ν)▷ sufficient 17:∀j, (h (j) 1 ,...,h (j) l j )← h (j) 18:SP← V j,i InContext(h (j) i )▷ suppliable 19:until SF∧ SP 20:allHelpersClosed ← V j Decomp((h (j) ),ω (j) ,M) 21: until allHelpersClosed 22: return True ▷ all helper lemmas proved, so ν holds 23: end function “cheating”, and agentic tools to aid in the proof search (details in the Appendix). The core of OrderDecompose is the recursive Decomp function (Alg. 1, line 10), which proves a subgoal ν from hy- potheses η 1 ,...,η n under a 30-second SMT budget, denoted ∆∪ j η j ⊢ SMT-30s ν; the tight budget keeps the feedback loop fast. When a direct SMT search fails, Decomp asks the LLM to propose intermediate lemmas h (j) → ω (j) , keeps them only if they are sufficient (SF) to close ν and suppli- able (SP) from the current context, and recurses on each. In both CreateLemmas and CreateHypothesis, the lemma search is aided by agentic tools. Finally, because the map stage leaves Soundness (P) and Citation unverified, Or- derDecompose checks both, and also that map stage objects were unchanged (line 7). If OrderDecompose returns False, either: (1) LLM is incapable (2) The oracle made a map stage mistake (3) Sys- tem E implementation limitations (4) Euclid made a mistake or (5) The translated text made a mistake. First, OrderDe- compose’s purpose is to mitigate LLM limitations. Second, if the oracle makes a mistake, they fix it and resume Or- derDecompose (details in the Appendix), and finally, (4) and (5) are formally addressed in the next section. Acceptance, Refute, and Gaps. To address issues (4) and (5), Pistis can refute a proof or identify its gaps; we define these notions precisely. To refute a proof is to derive a logical contradiction from it. A gap is a missing step that does not itself create a contradiction, and whether an omission is large enough to count as a gap is inherently subjective. To accept LeanEuclidOurs 0 1 2 3 4 5 3.68 4.52 Step Fidelity (0–5) 020406080100 Mathematical transparency Textbook representation Overall preference 63% 73% 62% 31% 17% 29% Preferred Responses (%) LeanEuclidTieOurs Figure 2: Human expert review results. Left: mean step- fidelity ratings with standard error over all rated items. Right: preference judgments by reviewers on three dimensions. a proof is to certify that it contains no contradiction, and is therefore valid, though it may still contain gaps. Pistis identifies gaps in two ways. First, during the fill stage the LLM may flag a suspected gap by returning False; if the oracle agrees, we mark it (details on how we mark in the Appendix). Second, Pistis detects assumption gaps automatically, in an optional stage between mapping and filling. A script materializes each formal assumption as a have statement and tries to close it with automated tactics, including SMT search; any unclosed assumption becomes a gap, marked with asorry and added to the sequence (φ ′ i ) i to be discharged. We treat an unclosed assumption as a reliable gap because assumptions should already be provable, so these tactics should close them. Pistis refutes a proof by formally exhibiting one of two failures at a step. The first is that an asserted step is false under premises,∃i, ∆∪α ⊢ ¬ formal(assert(s i )): the axioms and hypotheses together disprove what the proof claims ats i . The second is that an asserted step does not follow from the premises,∃i, ∆ ⊢ ∃v 1 ,...,v k ¬(α → formal(assert(s i ))): there is a concrete configuration of the geometric objects v 1 ,...,v k (the free variables ofα) that satisfies the hypotheses yet violates assert(s i ). Either failure yields a contradiction that certifies the proof is wrong; we further detail how this is derived in the Appendix, and give examples in Sec. 4.5. 4 Evaluation We conduct systematic evaluations of our method to answer the following four research questions: RQ1. How faithful are the Pistis-generated formal proofs compared to LeanEuclid (Murphy et al. 2024)? RQ2. Is OrderDecompose necessary, or can a bare LLM complete the fill stage on its own? RQ3. How does the compilation speed of Pistis-generated proofs compare to LeanEuclid? RQ4. Qualitatively, how does Pistis refute proofs and iden- tify gaps, including those in the textbook translations? 4.1 Evaluation Setups Targets. We target Euclid’s Elements, Books I–I, com- prising 92 propositions in total (48 in Book I, 14 in Book I, 30 in Book I). We take the natural-language proof text (including its bracketed proposition references) from open StepTranspReprPref Prop I-1 Prop I-2 Prop I-6 Prop I-7 Prop I-8 Prop I-9 Prop I-11 Prop I-12 Prop I-13 Prop I-14 Prop I-15 Prop I-16 Prop I-17 Prop I-20 Prop I-23 StepTranspReprPref Prop I-25 Prop I-27 Prop I-28 Prop I-30 Prop I-32 Prop I-33 Prop I-35 Prop I-36 Prop I-37 Prop I-38 Prop I-39 Prop I-40 Prop I-42 Prop I-43 Prop I-46 LeanEuclidTieOurs Figure 3: Per-proposition human evaluation on Book I, each cell scored on the [−3, 3] scale: blue favors LeanEuclid, white a tie, and gold favors ours. source Fitzpatrick (2007), and treat it as the source we for- malize faithfully. A small number of Book I propositions are omitted as they lie beyond the scope of the current System E implementation. Model and Agent. All proofs are generated with Claude Code (version 2.1.168), driving Claude Opus 4.8. Machine configuration. Proofs are checked with Lean 4 (v4.8.0-rc2), using SMT solvers Z3 4.15.4 and cvc5 1.3.4. In the Lean compile-time experiments, the SMT solvers run uncapped, so the only cutoff is a wall-clock limit. Experiments were generally run on a Linux SLURM cluster whose compute nodes are Intel Xeon Platinum 8480+ (Sap- phire Rapids), with each job allocated 32 cores and 128 GB. Baselines and Metrics. We compare against LeanEu- clid (Murphy et al. 2024) (Book I only), which claims to already provide faithful formalizations, and vanilla LLM- agent based baselines. We report faithfulness (detailed in RQ1), wall-clock time, monetary cost, and other relevant metrics detailed in the following sections. 4.2 RQ1: Faithfulness of Generated Proofs Double-blind Human Evaluation. We randomly sampled 30 of the 48 Book I propositions for human review. Each reviewer was assigned 10 random propositions and saw the textbook theorem and proof, two anonymized formalizations, and an interactive Lean server for inspecting the proof state at each line. The formalizations were shown in randomized or- der, and method-identifying nonmathematical artifacts were removed. Reviewers were 14 formal-methods researchers and students familiar with Lean and geometry, who were indepen- dent of the author team. The study produced 127 completed assignments, with 4.2 final annotations per proposition on average, covering 254 step-fidelity ratings and 381 pairwise preference judgments. The review rubric and interface are detailed and summarized in the Appendix. Figure 2 summarizes the aggregate human scores and pref- erences, while Figure 3 shows the proposition-level pattern. The human ratings favor our method across all evaluated di- mensions. Figure 2 shows a higher mean step-fidelity score for our formalizations than for LeanEuclid (4.52 vs. 3.68). Reviewers also preferred proofs generated by our method in Pistis (Ours)Baseline (LeanEuclid)Baseline (Claude Code) OC PSC PSFCDF ASC n = 48, scale 3–5 (a) Book I OC PSC PSFCDF ASC n = 14, scale 0–5 (b) Book I OC PSC PSFCDF ASC n = 30, scale 0–5 (c) Book I Figure 4: LLM-as-judge faithfulness by book over five sub- categories, OC (object correspondence), PSC (proof step coverage), PSF (proof structure fidelity), CDF (cited depen- dency fidelity), ASC (assumption & side condition). Book I compares Pistis against the LeanEuclid baseline, while Book I compares against LLM-agent-generated proofs. MetricOrderDecompose LLM-only Factor coverage (pass@k)↑15/15 (100%) 6/15 (40%) 2.5× total cost / success ($)↓15.628.81.8× Table 2: Fill Stage ablation (N =15, k=3 runs each). 63.0% of mathematical-transparency comparisons, 73.2% of textbook-representation comparisons, and 62.2% of overall- preference comparisons. The proposition-level heatmaps in Figure 3 show that these gains are broadly distributed rather than driven by a small number of propositions. LLM-as-Judge Evaluation. We also assess faithfulness with an LLM-as-judge protocol. As shown in Fig. 4, our method consistently outperforms the baselines while staying consistent throughout the three books. Specifically, faithful- ness evaluation was done with a 5 point scale rubric across 5 different subcategories: object correspondence, proof step coverage, proof structure fidelity, cited dependency fidelity, and assumption and side conditions. We prompted open and closed LLMs (Opus 4.6 shown, GLM-5 in Appendix) to perform assessment with a strict rubric, detailed in the Ap- pendix. On Book I, Pistis is favored 5.2× as often as Lea- nEuclid (26 wins, 17 ties, 5 losses). 4.3 RQ2: Filling Stage Ablation Study We compare Pistis (full pipeline) against an ablated bare- LLM baseline that receives the same agentic framework and model but with our skills, scripts, hooks, and persistent mem- ory removed. Both arms start in the same state, where the map stage has just been completed. Further, they are given the same citation instructions, are graded once at the end by an identical script checking Soundness, Citation (Tab. 1), and that none of the objects created in the map stage were altered. They run under a 12-hour wall-clock budget per at- tempt, and we evaluate 15 propositions across Books I–I with 3 repeated runs each (90 total runs). BaselinePistis (Ours)Baseline failed 10 −1 10 0 10 1 Prop I-3 Prop I-6 Prop I-12 Prop I-18 Prop I-20 Prop I-27 Prop I-30 Prop I-36 Prop I-45 Prop I-3 Prop I-12 Prop I-6 Prop I-11 Prop I-25 Prop I-36 Timeout (12h) (a) Synthesis wall-clock (hr) 10 1 10 1.5 (b) Compile time (s) Figure 5: Fill Stage ablation over Books I–I (all 3 runs shown as separate bars). (a) Synthesis wall-clock per propo- sition; baseline runs that reach the 12h cap fail, while every run of Pistis finishes within∼3.5h. (b) Compile time of the proof each arm produced, timed by recompiling only that proof’s own files from a warm cited-dependency cache. 010203040 10 1 10 2 10 3 ? Timeout (1 Hour) Number of Propositions Compiled Compile Time (s) Pistis (Ours) – Run 1 Pistis (Ours) – Run 2 Pistis (Ours) – Run 3 Baseline (LeanEuclid) – Run 1 Baseline (LeanEuclid) – Run 2 Baseline (LeanEuclid) – Run 3 Figure 6: Cactus plot of cold-compile time on a log scale, all 3 runs drawn per world. Our decomposed proofs compile all 48 propositions, while the original baseline compiles 41. Findings. As shown in Table 2, and a more detailed view in Fig. 5, Pistis solves all 15 propositions (45/45 runs succeed), whereas the baseline solves 6 and fails to finish the remaining 9 within the 12-hour budget (29/45 runs time out). Pistis is also cheaper per successful proof ($15.6 vs. $28.8), since the baseline pays for many long runs that never complete. 4.4 RQ3: Lean Compile Performance Some LeanEuclid proofs compile very slowly (over an hour) or not at all, due to heavy SMT reliance. A key design decision of OrderDecompose is to ensure proofs compile quickly, so here we compare Pistis generated proofs against Prop I-9. To cut a given rectilinearangle in half. LetBAC be the given recti. . . Prop I-10. To cut a given finitestraight-line in half. LetAB be the given finite. . . NL Source Prop I-1. To find the center of a given circle. LetABC be the given circle. . . Proof. Let some straight-lineAB be drawn through (ABC), at random 1 , and let (AB) be cut in half at pointD Proposition I-92 . . . . Faithful formalization theorem p1: ∀(ABC: Circle), ∃f: Point, f.isCentre ABC := by... euclid_apply prop_10... -- @suppress_deps_check have s2: between a d b ∧ |(a–d)|=|(d–b)|:= by... 2 Figure 7: A citation gap unveiled in the proof of Prop. I-1. Fitzpatrick brackets “cut AB in half” asProposition I-9, but I-9 is about angles, not straight lines, and it should be Prop I-10. NL Source Prop I-5. For isosceles triangles, the angles at the base are equal to one an- other. and if the equal sides are. . . Proof. Since the sideAB is equal to the sideAC, the base angles are equal to one another. . . Now the angleCBD is itself a right-angle 3,. . . Which is the very thing required to show. Formal refutation theorem p5: ∀(a b c... )... → (∠c:b:d=∠b:c:e) := by have s3 : ∠ c:b:d = ⌞ := by sorry have refute_s3 : ¬(∠ c:b:d = ⌞) := by ... ; euclid_finish have contra : False := refute_s3 s3 3 Figure 8: Formal refutation of an LLM-generated proof. Left: excerpt from an LLM-generated proof with false claim s 3 . Right: we prove¬ formal(assert(s 3 )). the original LeanEuclid proofs (Murphy et al. 2024) in terms of compilation speed on Book I. We wipe all built artifacts and compile 3 every proposition from cold, one at a time, with a one-hour per-proposition wall timeout, and repeat this over three runs. As Fig. 6 shows, Pistis compiles all 48 proposi- tions, whereas LeanEuclid compiles only 41. Further, Pistis compiles all of Book I in 13.3 minutes of wall-clock, more than 33× as fast as LeanEuclid (7.3+ hours). 4.5 RQ4: Qual. Analysis of Refutations and Gaps We now illustrate how Pistis identifies gaps in Euclid’s El- ements and its translations, or refutes NL proofs such as those generated by AI. Across the corpus of Books I–I, we mark 33 assumption gaps, 2 confirmed citation mistakes, and 17 other generic gaps. We hereby illustrate a citation gap found by Pistis arising from the edition rather than Euclid: Fig. 7 shows a source that brackets “let AB be cut in half” as [Prop. I-9], though I-9 bisects an angle whereas bisect- ing a straight-line is I-10. Another example, an AI-generated proof refuted by our method, is presented in Fig. 8, where the sentence s 3 of a proof of Book I, Prop. 5 claims that angle CBD is a right angle, which we formally refute. To- gether, these demonstrate that Pistis is capable of checking NL proofs while surfacing gaps and refuting errors. 3 Compile-time experiments were run on a single exclusive AMD EPYC 9634 (Zen 4, 84 cores) in this specific experiment 5 Related Work Autoformalization and Euclidean Geometry. Autofor- malization in Lean (de Moura and Ullrich 2021) grew from landmark formalizations and libraries (Gonthier 2008; Hales et al. 2017; mathlib Community 2020) into an area driven by language models (Wu et al. 2022; Li et al. 2024). Most work asks what systems can formalize, at growing scales: compe- tition and textbook statements (Zheng, Han, and Polu 2022; Azerbayev et al. 2023), repositories and long contexts (Yang et al. 2023; Hu, Zhu, and Welleck 2025), corpora and theo- ries (Min et al. 2026; Feng et al. 2026), progress measured by compilation. Attention has recently turned to how a proof closes. Euclid has drawn the most: Avigad et al. (Avigad, Dean, and Mumma 2009) give system E as a faithful model of his proofs, Beeson et al. (Beeson, Narboux, and Wiedijk 2018) machine-check Book I, and LeanEuclid (Murphy et al. 2024) implements E in Lean with SMT for diagrams. Else- where informal sketches guide proof search (Jiang et al. 2023; Zheng et al. 2024), but only heuristically. Neurosymbolic and Agentic Approaches. Neurosym- bolic programming (Huang et al. 2021; Li, Huang, and Naik 2023; Manhaeve et al. 2018) supplies neural facts to declarative programs reasoned over symbolically; agentic coding frameworks (Wang et al. 2025) establish the tool- equipped-agent pattern. Closest are hierarchical decompo- sition searches (Lample et al. 2022; Li et al. 2026), which split a goal into independently closed subgoals chosen for tractability: any that closes the theorem will do, none con- strained by the source argument. Faithfulness. Statement-level faithfulness means seman- tic equivalence with the source, via type-checking, back- translation, or logical equivalence (Poiroux et al. 2025; Lu et al. 2024). Such equivalence never constrains the proof: the kernel accepts any well-typed term inhabiting the goal, so a faithful statement admits proofs the source never gave. Proof-level evaluation is weaker: LeanEuclid (Murphy et al. 2024) measures only whether Lean accepts the proof and its edit distance to a hand repair. ProofFlow (Cabral et al. 2025) preserves a dependency graph but validates only well- formedness, not whether each step’s tactics use its declared premises. The informal analogue asks whether a chain of thought reflects its computation (Turpin et al. 2023). 6 Conclusion and Future Works We introduced Pistis, an oracle-guided proof search that for- malizes a natural-language proof into a Lean proof satisfying five necessary conditions of faithfulness. Across three books of Euclid’s Elements, Pistis produces proofs that are more faithful than prior work and compile faster, and it accepts or refutes human- and AI-written arguments, surfacing gen- uine errors. We plan to extend faithful formalization beyond Euclidean geometry and reduce its reliance on supervision. Limitations. Our study is limited to Euclidean geometry in System E, which cannot express a handful of Elements propositions. Moreover, Pistis relies on a human or LLM oracle to certify faithfulness, and our conditions, while nec- essary, are not sufficient to capture an author’s full intent. Acknowledgements We thank the anonymous reviewers who participated in our human evaluation study. Research reported in this publica- tion was supported by an Amazon Research Award, Fall 2025, and by the 2026 Amazon Nova AI Challenge: Trusted Software Agents; Tadd Mao acknowledges support from an NSERC Undergraduate Student Research Award. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies of the supporting sponsors. References Avigad, J.; Dean, E.; and Mumma, J. 2009. A Formal System for Euclid’s Elements. The Review of Symbolic Logic, 2(4): 700–768. Azerbayev, Z.; Piotrowski, B.; Schoelkopf, H.; Ayers, E. W.; Radev, D.; and Avigad, J. 2023. ProofNet: Autoformaliz- ing and Formally Proving Undergraduate-Level Mathemat- ics. arXiv preprint. Beeson, M.; Narboux, J.; and Wiedijk, F. 2018. Proof- checking Euclid. arXiv:1710.00787. Cabral, R.; Do, T. M.; Yu, X.; Tai, W. M.; Feng, Z.; and Shen, X. 2025. ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization. arXiv:2510.15981. Carneiro, M. 2019. The Type Theory of Lean. Master’s thesis, Carnegie Mellon University. https://github.com/digama0/ lean-type-theory. de Moura, L.; and Ullrich, S. 2021. The Lean 4 Theo- rem Prover and Programming Language. In Platzer, A.; and Sutcliffe, G., eds., Automated Deduction (CADE 28), vol- ume 12699 of Lecture Notes in Computer Science, 625–635. Berlin, Heidelberg: Springer. Feng, Y.; Pu, F.; An, O.; Bastani, O.; Zhang, L.; Huang, J.; Si, X.; and Li, Z. 2026. Theory-Scale Auto-Formalization of Logics for Computer Science. arXiv:2606.26525. Fitzpatrick, R. 2007. Euclid’s Elements of Geometry (Greek/English edition). https://github.com/rfitzp/Elements. Greek text after J. L. Heiberg (1883–1885); commit 5a6699e, accessed 2026-07-28. Gonthier, G. 2008. Formal Proof—The Four-Color Theo- rem. Notices of the American Mathematical Society, 55(11): 1382–1393. Hales, T.; Adams, M.; Bauer, G.; Dang, T. D.; Harrison, J.; Hoang, L. T.; Kaliszyk, C.; Magron, V.; McLaughlin, S.; Nguyen, T. T.; et al. 2017. A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5: e2. Hu, J.; Zhu, T.; and Welleck, S. 2025. miniCTX: Neural Theorem Proving with (Long-)Contexts. arXiv:2408.03350. Huang, J.; Li, Z.; Chen, B.; Samel, K.; Naik, M.; Song, L.; and Si, X. 2021. Scallop: From Probabilistic Deductive Databases to Scalable Differentiable Reasoning. In Advances in Neural Information Processing Systems (NeurIPS). Jiang, A. Q.; Welleck, S.; Zhou, J. P.; Li, W.; Liu, J.; Jamnik, M.; Lacroix, T.; Wu, Y.; and Lample, G. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. arXiv:2210.12283. Lample, G.; Lachaux, M.-A.; Lavril, T.; Martinet, X.; Hayat, A.; Ebner, G.; Rodriguez, A.; and Lacroix, T. 2022. Hy- perTree Proof Search for Neural Theorem Proving. arXiv preprint. Li, Z.; Huang, J.; and Naik, M. 2023. Scallop: A Language for Neurosymbolic Programming. Proceedings of the ACM on Programming Languages (PLDI), 7. Li, Z.; Sun, J.; Murphy, L.; Su, Q.; Li, Z.; Zhang, X.; Yang, K.; and Si, X. 2024. A Survey on Deep Learning for Theorem Proving. arXiv preprint. Li, Z.; Yang, Z.; He, D.; Zhao, H.; Zhao, A.; Tang, S.; Yang, K.; Gupta, A.; Su, Z.; and Jin, C. 2026. Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification. arXiv:2603.19329. Lu, J.; Wan, Y.; Huang, Y.; Xiong, J.; Liu, Z.; and Guo, Z. 2024. FormalAlign: Automated Alignment Evaluation for Autoformalization. arXiv preprint. Manhaeve, R.; Dumancic, S.; Kimmig, A.; Demeester, T.; and De Raedt, L. 2018. DeepProbLog: Neural Probabilistic Logic Programming. In Advances in Neural Information Processing Systems (NeurIPS). mathlib Community, T. 2020. The lean mathematical li- brary. In Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, CPP ’20, 367–381. ACM. Min, M. J.; Gao, Y.; Sy, W.; Li, Z.; Si, X.; and Bastani, O. 2026. Divide and Abstract: Autoformalization via Decompo- sition and Abstraction Learning. In International Conference on Learning Representations (ICLR). Murphy, L.; Yang, K.; Sun, J.; Li, Z.; Anandkumar, A.; and Si, X. 2024. Autoformalizing Euclidean Geometry. ArXiv:2405.17216 [cs.LG]. Poiroux, A.; Weiss, G.; Kunčak, V.; and Bosselut, A. 2025. Reliable Evaluation and Benchmarks for Statement Autofor- malization. In Conference on Empirical Methods in Natural Language Processing (EMNLP). Tao, T. 2026. Mathematics in the Age of AI. Public lecture, International Congress of Mathematicians. Thurston, W. P. 1994. On Proof and Progress in Mathematics. Bulletin of the American Mathematical Society, 30(2): 161– 177. Turpin, M.; Michael, J.; Perez, E.; and Bowman, S. R. 2023. Language Models Don’t Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting. arXiv:2305.04388. Wang, X.; Li, B.; Song, Y.; Xu, F. F.; Tang, X.; Zhuge, M.; Pan, J.; Song, Y.; Li, B.; Singh, J.; Tran, H. H.; Li, F.; Ma, R.; Zheng, M.; Qian, B.; Shao, Y.; Muennighoff, N.; Zhang, Y.; Hui, B.; Lin, J.; Brennan, R.; Peng, H.; Ji, H.; and Neubig, G. 2025. OpenHands: An Open Platform for AI Software Developers as Generalist Agents. In International Conference on Learning Representations (ICLR). Wu, Y.; Jiang, A. Q.; Li, W.; Rabe, M. N.; Staats, C.; Jamnik, M.; and Szegedy, C. 2022. Autoformalization with Large Language Models. In Advances in Neural Information Pro- cessing Systems (NeurIPS). Yang, K.; Swope, A. M.; Gu, A.; Chalamala, R.; Song, P.; Yu, S.; Godil, S.; Prenger, R.; and Anandkumar, A. 2023. Le- anDojo: Theorem Proving with Retrieval-Augmented Lan- guage Models. In Advances in Neural Information Process- ing Systems (NeurIPS) Datasets and Benchmarks Track. Yu, X.; Zhong, J.; Feng, Z.; Zhai, P.; Yousefzadeh, R.; Ng, W. C.; Liu, H.; Shou, Z.; Xiong, J.; Zhou, Y.; Ong, C. B.; Sugiarto, A. J.; Zhang, Y.; Tai, W. M.; Cao, H.; Lu, D.; Sun, J.; Xu, Q.; Xin, S.; and Li, Z. 2025. Mathesis: To- wards Formal Theorem Proving from Natural Languages. arXiv:2506.07047. Zheng, C.; Wang, H.; Xie, E.; Liu, Z.; Sun, J.; Xin, H.; Shen, J.; Li, Z.; and Li, Y. 2024. Lyra: Orchestrating Dual Correc- tion in Automated Theorem Proving. arXiv:2309.15806. Zheng, K.; Han, J. M.; and Polu, S. 2022. MiniF2F: a cross- system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations (ICLR). A Pistis Implementation Details This section is intended to clarify the connection between what the main paper describes abstractly in the methodol- ogy to how it is implemented. Examples of such questions we answer include: what does the mapping formal(·) look like in the code? How do we enforce that the agent follows OrderDecompose? A.1 How Objects are Implemented Input Objects. Recall (Sec. 3) that Pistis takes as input the tuple ⟨P NL , formal(P NL ),F NL , ∆⟩. Fig. 9 instantiates every component verbatim from the released artifact on Book I, Prop. 6 (I-6), the running example of Fig. 1, so a reader can locate each object in the codebase directly. The figure shows every input object, as well as further details such as what the free variables are, and how formal(P NL ) is broken down into α→ β. Free Variables. We explain why there are free variables rather than having the variables quantified with∀. Usually, theorems never have any free variables, and they are all quantified with either ∀ or ∃. However the way we write theorems in Lean, when we prove a theorem, we are not proving the one with ∀ quantifiers, and rather the one with free variables. Take for example the theorem statement ∀x∈ C,P (x)→ Q(x). In Lean this theorem statement is theorem prop : (x : C), P(x) → Q(x) := This is a function, where x ∈ C is already given and fixed. The proof, that is the stuff after :=, is really a proof that ∆∪x∈ C⊢ P (x)→ Q(x). Here, x is a free variable not quantified with∀. Another subtlety, is in this case, we would consider P (x) as the hypothesis, and because we use the intro tactic, we are really proving ∆∪x ∈ C,P (x) ⊢ Q(x). Hence in this example, α = α 1 ∧α 2 = x∈ C∧P (x), while β = Q(x), with the proof being that of ∆∪x ∈ C,P (x)⊢ Q(x). As a final note, even though Lean only directly proves ∆∪x ∈ C,P (x) ⊢ Q(x), this directly implies ∆ ⊢ x ∈ C → (P (x) → Q(x)), which further implies ∆ ⊢ ∀x ∈ C, (P (x)→ Q(x)) Map Phase Objects. The map stage produces the tuple M = ⟨ ̄ φ ′ , ̄s, assumps(·), assert(·), formal(·)⟩ (Sec. 3.2) as a single Lean file, and Fig. 10 shows this artifact concretely for Prop. 6 in its pre-fill state, where every step body is still := by sorry. The euclid_sentence tactic is what constructs these objects, and each output-tuple component is pinpointed in the figure. Each tuple object is implemented as: • ̄s =s 1 ,...,s n , the ordered NL string literals, one per euclid_sentence, appearing top-to-bottom so the Order condition holds by construction; • formal(assert(s i )), the type annotation τ of (stepi : τ ) in each sentence. Also, the assertion assert(s i ) is the part of s i that is not an assumption; • For each a∈ assumps(s i ), a and formal(a) are defined by the -- @assumption ("text", type) com- ment tags above the sentence, one per assumption a; • ̄ φ ′ , the sequence of subgoals the fill stage will close, which consists of both the sentence steps formal(assert(s i )) and the additional helper have ...:= by sorry steps the map stage inserts to bridge them (e.g. swapfig in Fig. 10). Alongside euclid_sentence, three sibling tactics han- dle Euclid’s non-assertive sentences. These still record the text (so Coverage can tile the full proof) but emits no have, carries no claim, and leaves the proof term and context un- changed. The three differ only by what role they mark: • euclid_intro_sentence: this is just P NL • euclid_conclude_sentence: the closing restate- ment of P NL , which Euclid always writes • euclid_wts: a mid-proof “I say that X” (last line of Fig. 10) that announces the goal X the following sen- tences will establish, rather than asserting X is already proven. Because a structural sentence asserts nothing, for it assert(s i ) is the empty string, assumps(s i ) = ∅, and formal(assert(s i )) = True. Fill Stage Objects. The fill stage proves each φ ′ i that the map stage left as sorry: for each it produces a se- quence of steps κ 1 ,...,κ t such that Lean checks ∆ ∪ α,φ ′ 1 ,...,φ ′ i−1 ,κ 1 ,...,κ t ⊢ φ ′ i (Sec. 3.2). Fig. 11 shows an example of how this happens concretely. Output Objects. Fig. 12 gives a bird’s-eye view of a fully completed proposition, showing an example of what the full output looks like in practice. A.2 Map Stage Details This section explains how the map stage is executed in the code. The map stage runs as skills (Tab. 3) which are prompt files. The first skill ran is (1) faithful-split, which gets the LLM to read the proposition’s English text and splits it into an ordered list of NL segments satisfy- ing Atomicity and Coverage, and finally written to a file split.json. A script (check_faithful.py --split) then confirms this partition tiles the source text byte-for-byte, enforcing Coverage before any Lean is written. Then (2) faithful-map turns that split into Main.lean. It first stamps a placeholder file, a euclid_sentence "Book#.Prop#.Step#" "NL segment" (stepN : True) := by sorry per entry, using the faithful_map_assemble.py --placeholders script, which copies each sentence’s "NL segment" and locator directly from split.json. Then the agent replaces each True with (what the agent thinks) is the sentence’s real claim formal(assert(s i )) and each placeholder tag with a real @assumption ("text", type). At the end check_faithful.py re-checks Coverage and Order, while the oracle checks Atomicity and Atomic Faithfulness. One may wonder how Order is possible to check. After all, the definition in Tab. 1 references ̄ φ the final proof, which does not yet exist. Recall that the fill stage is only allowed -- ============ formal(P_NL) : the Lean theorem (Book1/Prop06/Main.lean) ============ theorem proposition_6 : ∀ (a b c : Point) (AB BC AC : Line), formTriangle a b c AB BC AC ∧ (∠ a:b:c =∠ a:c:b) -- hypothesis α = α 1 ∧ ... → |(a-b)| = |(a-c)| -- conclusion β -- free variables v 1 ..v k : a b c, AB BC AC -- ============ P_NL : the natural-language proposition ============ -- "If a triangle has two angles equal to one another then the sides subtending -- the equal angles will also be equal to one another." -- ============ F_NL : the natural-language proof that gets segmented ============ -- "Let ABC be a triangle having the angle ABC equal to the angle ACB. I say that -- side AB is also equal to side AC. For if AB is unequal to AC then one of them -- is greater. Let AB be greater. And let DB, equal to the lesser AC, have been -- cut off from the greater AB [Prop. 1.3]. And let DC have been joined [Post. 1]. -- Therefore, since DB is equal to AC, and BC (is) common, the two sides DB, BC are -- equal to the two sides AC, CB, respectively, and the angle DBC is equal to the -- angle ACB. Thus, the base DC is equal to the base AB, and the triangle DBC will -- be equal to the triangle ACB [Prop. 1.4], the lesser to the greater. The very -- notion (is) absurd [C.N. 5]. Thus, AB is not unequal to AC. Thus, (it is) equal." -- ============ ∆ : the fixed System E axiom set (SystemE/Theory/ ** ), e.g. ============ axiom two_points_determine_line : ∀ (a b : Point) (L M : Line), distinctPointsOnLine a b L ∧ (a.onLine M) ∧ (b.onLine M) → L = M axiom segment_symmetric : ∀ (a b : Point), |(a-b)| = |(b-a)| axiom angle_symm : ∀ (a b c : Point), (a ̸= b) ∧ (b ̸= c) → ((∠ a:b:c) = (∠ c:b:a)) axiom superposition : ∀ (a b c d g h : Point) (AB BC AC L : Line), ... -- ... Figure 9: The input tuple⟨P NL , formal(P NL ),F NL , ∆⟩ instantiated on Book I, Prop. 6. Every component is reproduced verbatim from the released artifact. to insert formulae κ in between two existing φ ′ i ,φ ′ j . This is enforced in practice by telling the LLM, and script checkers such as check_faithful.py. Thus checking the order is correct in the map stage guarantees the order stays correct in the fill stage. Once the oracle approves all checks in the end, check_steps.py --save saves these objects so the fill stage cannot silently alter them (the LLM agent is denied write access). A.3 Fill Stage (OrderDecompose) Details Similar to how map stage is implemented, the fill stage re- lies on skills, but also relies on hooks, and tools to follow OrderDecompose. It starts by calling the faithful-prove skill (Tab. 3), which contains the core instructions of OrderDecompose. During the algorithm, a set of tools (Tab. 4) help the agent in the proof search process, and hooks/settings make the agent actually follow the algorithm rather than merely being told to. One example of a setting to enforce good behavior, is that the agent is denied raw lake build, and can only build using one of the tools, so all its build commands can be checked. An example of a hook, is that we hard-deny the agent from writing anystepN.lean that is past the latest step checked, so it physically cannot skip ahead or prove a later step before an earlier one is certified, enforcing the in-order iteration of line 1 of Alg. 1. Routing every build through these scripts likewise forces the SF/SP/P (sufficiency, suppliability, and provability) discipline on each new lemma: it is first checked for sufficiency (line 16), then suppliability (line 18), and only then proven (line 20). A final check_step.py --all certifies the whole proof end-to-end; in practice it rarely surfaces anything new, since each step was already certified in isolation as it was proved. Resume. check_step.py records which steps are al- ready proven. Because the agent proves the steps in order, if it stops after finishing φ ′ i−1 it simply continues from φ ′ i rather than starting over. This is correct because each φ ′ i is proved using only α,φ ′ 1 ,...,φ ′ i−1 , so it can never depend on a later step; the steps already proven stay valid, and if the oracle later fixes a map-stage mistake only that step and the ones after it need re-proving. B Accept, Refute, and Gaps In this section, we validate our formal refutation methods, then go into more detail on gaps. B.1 Why Refutation Creates a Logical Contradiction This section goes into detail how we are able to prove a logical contradiction if either of the following are true: A ∃i, ∆∪α⊢¬ formal(assert(s i )) B ∃i, ∆ ⊢ ∃v 1 ,...,v k ,¬(α → formal(assert(s i ))), where v 1 ,...,v k are all the free variables occurring in α We begin by assuming that System E axioms cannot prove the contradiction, denoted False in Lean, and nor can the hypotheses ( ∆∪α ⊬ False). Recall that if, Pistis is able to accept the proof, then a proof (φ 1 ,....,φ N ) of ∆∪α⊢ β, is outputted. A property of this proof, is that for every φ i , ∆∪α ⊢ φ i (according to first order logic). Also, recall that every formal(assert(s i )) = φ k for some k (output 4 of Sec. 3). If A is true, then ∆∪α⊢¬φ k , but because ̄ φ is a proof of ∆∪α⊢ β, ∆∪α⊢ φ k hence we prove False. We assumed we cannot prove False so this is a contradiction. theorem proposition_6 : ∀ (a b c : Point) (AB BC AC : Line), formTriangle a b c AB BC AC ∧ (∠ a:b:c =∠ a:c:b) → |(a-b)| = |(a-c)| := by euclid_intros have habsurd : ¬ (|(a-b)| ̸= |(a-c)|) := by intro hne -- s 1 = "For if AB is unequal to AC then one of them is greater." -- assert(s 1 ) = "one of them is greater" -- formal(assert(s 1 )) = |(a-b)| > |(a-c)| ∨ |(a-c)| > |(a-b)| -- assumptions(s 1 ) = "AB is unequal to AC" , -- formal(a) = |(a-b)| ̸= |(a-c)|, where a is the one element in assumptions(s 1 ) -- @assumption ("AB is unequal to AC", |(a-b)| ̸= |(a-c)|) have step1_assumption1 : |(a-b)| ̸= |(a-c)| := by assumption -- materialized assumption euclid_sentence "1.6.1" "For if AB is unequal to AC then one of them is greater." (step1 : |(a-b)| > |(a-c)| ∨ |(a-c)| > |(a-b)|) := by sorry wlog hgt : |(a-b)| > |(a-c)| generalizing b c AB BC AC with Hsym · have swapfig : -- another helper ‘have‘ in φ (∠ a:c:b =∠ a:b:c) ∧ (a ̸= c) ∧ (AC ̸= BC) ∧ (BC ̸= AB) ∧ (AB ̸= AC) ∧ (|(a-c)| ̸= |(a-b)|) ∧ (|(a-c)| > |(a-b)| ∨ |(a-b)| > |(a-c)|) ∧ (|(a-c)| > |(a-b)|) := by sorry obtain ⟨...⟩ := swapfig exact Hsym c b AC BC AB ... · euclid_sentence "1.6.2" "Let AB be greater." (step2 : |(a-b)| > |(a-c)|) := by sorry . . . euclid_sentence "1.6.9" "The very notion (is) absurd [C.N. 5]." (step9 : False) := by sorry exact step9 euclid_sentence "1.6.10" "Thus, AB is not unequal to AC." (step10 : ¬ (|(a-b)| ̸= |(a-c)|)) := by sorry euclid_sentence "1.6.11" "Thus, (it is) equal." (step11 : |(a-b)| = |(a-c)|) := by sorry exact step11 -- ----------- separately, a mid-proof "what-to-show" sentence (Book I Prop. 19) ----------- -- euclid_wts announces a goal instead of asserting a fact, so: -- assert(s i ) = "" (empty), assumptions(s i ) = ∅, formal(assert(s i )) = True euclid_wts "1.19.2" "In fact, AC is not equal to AB." Figure 10: Example of artifact at the end of map-stage, M= ⟨ ̄ φ ′ , ̄s, assumps(·), assert(·), formal(·)⟩. The euclid_sentence tactic is the mapping-object constructor: it emits the ordered NL partition ̄s = s 1 ,...,s n , and for each s i its type (stepi : τ ) is formal(assert(s i )) while the -- @assumption tags above it pinpoint assumps(s i ) together with each formal(a). Each @assumption is also materialized as a have (e.g. step1_assumption1) by the assumption stage (Sec. B.2). A euclid_wts is also shown at the end. The way to know if it is “wts“ or not is by context of what is around it. If B is true, we show that it will also lead to a contradiction. Like case A, ∆∪α ⊢ φ k , and therefore ∆ ⊢ α → φ k , which implies that for variables v 1 ,...,v k occurring free in α: ∆ ⊢ ∀v 1 ,...,v k , (α → φ k ). But by assumption B, ∆ ⊢ ∃v 1 ,...,v k ,¬(α → φ k ), so ∆ ⊢ ¬(∀v 1 ,...,v k , (α → φ k )) hence we prove False. B.2 Assumption Gap Implementation Details Recall the (optional) assumption gap tagging stage, which tries automated tactics to close the assumption. This section goes into more detail, such as explaining the exact tactics to close the assumption. The exact automated tactics tried are: rfl, assumption, simp, linarith, nlinarith, euclid_finish, where euclid_finish is essen- tially an SMT solver. These are tried one at a time in the order listed, and if none of them close the assumption, we mark it as a gap (@assumption_gap) and leave a sorry placeholder. We justify this choice of measuring gaps since assump- tions are notions that should already be proven, not new steps to prove, and we believe these automated tactics are generous (they are already powerful), so if they claim there is an assumption gap, then it is trustworthy. Across our 92 proofs, the stage materializes 311 assump- tions in total, of which 33 are marked as gaps and passed to the fill stage (11, 5, and 17 in Books I, I, and I respectively). B.3 Citation Gap A citation gap is a cited [Prop. B.N] that the Citation check cannot satisfy. We mark it with a -- @suppress_deps_check "reason" line above the sentence, which tells the checker script (check_faithful.py) to skip that one citation. This is needed in two cases: the citation is an actual mistake in the source edition (as explained in the main text), or it points to a proposition we skipped (one of the Book I propositions we leave out of scope; see Sec. H). We use 7 such tags across Book I. -- BEFORE (map stage): step9 is left as ‘sorry‘ -- the missing κ 1 ,...,κ t euclid_sentence "1.6.9" "The very notion (is) absurd [C.N. 5]." (step9 : False) := by sorry -- AFTER (fill stage): the sorry is replaced by a call to the backing lemma, which supplies κ 1 ,...,κ t . euclid_sentence "1.6.9" "The very notion (is) absurd [C.N. 5]." (step9 : False) := by euclid_apply (helper_1_6_step9 a b c d AB BC AC ...) theorem helper_1_6_step9 (a b c d : Point) (AB BC AC : Line) (hbda : between b d a) (hbdac : |(b-d)| = |(a-c)|) (hdbc_acb :∠ d:b:c =∠ a:c:b) (harea : Triangle.area △d:b:c = Triangle.area △a:c:b) ... : False := by have hoff : ¬ c.onLine AB := by euclid_finish -- one of the κ i have hdec : Triangle.area △a:d:c + Triangle.area △c:d:b = Triangle.area △a:c:b := by euclid_apply (sum_areas_if a b d c AB); assumption have hpos : 0 < Triangle.area △a:d:c := by euclid_finish have hsymm : Triangle.area △c:d:b = Triangle.area △d:b:c := by euclid_finish linarith Figure 11: The fill stage on sentence 1.6.9 of Prop. 6. Before, the map stage leaves step9 as sorry, the placeholder for the missing steps κ 1 ,...,κ t . After, the body after being filled becomes := by euclid_apply (helper_1_6_step9 ...) SkillRoleExample instruction (verbatim excerpt) faithful-split Map stage, part 1: split the NL proof into atomic assertions “Your ONLY job: take the raw English text of a Euclid proposition and split it into atomic assertions. [. . . ] You do NOT translate to Lean, you do NOT look at any .lean file.” faithful-mapMap stage, part 2: turn each assertion into a Lean claim type “Your job: fill . . . a Lean claim type per sentence . . . one sentence at a time. [. . . ] RULE 0: THE SENTENCE IS THE CLAIM. [. . . ]” faithful-prove Fill stage: main instructions to follow Or- derDecompose “prove each Euclid sentence’s step, IN ISOLATION, using the recursive... . . . the SCRIPT does all wiring . . . you only ever write proof bodies and add have+backing-file decom- positions.” Table 3: The agent skills (prompt files under .claude/skills/) and a verbatim excerpt of each one’s core instruction. The map stage runs faithful-split then faithful-map; the fill stage then runs faithful-prove. B.4 Generic Gap Implementation Details A generic gap is a gap in Euclid’s reasoning itself, distinct from an assumption and citation gap. These surface when OrderDecompose cannot close a step and returns False: if the oracle agrees the step is a genuine gap rather than anM or mapping failure, we mark it with a -- @euclid_gap: <why> comment. For example, Book I Prop. 35 says that if two straight- lines AC and BD in a circle cut one another at E, the rectangle on the two pieces of AC equals the rectangle on the two pieces of BD. Euclid proves two cases: both lines pass through the centre, and neither line passes through the centre. He does not treat the remaining case, where one line passes through the centre and the other does not, even though his hypotheses allow it. We add this missing case and tag the site -- @euclid_gap. Across Book I we mark 17 such generic gaps. None were marked in Book I and we do not claim any gaps in Book I as these were already found by (Murphy et al. 2024). Note ordinary System-E plumbing should not be consid- ered a gap, and what truly constitutes a gap is subjective so these are simply what we judged to be a gap. C Human Evaluation Protocol Reviewers used a custom web interface to evaluate anonymized pairs of formalizations. The interface supported the full review workflow, from an interactive tutorial to step- fidelity scoring and final pairwise preferences. The review itself proceeded in two stages. 1. They rated the step fidelity of each formalization inde- pendently. 2. They answered pairwise preference questions comparing the two anonymized formalizations. To ensure fairness, we compare only the for- mal Lean proofs, and remove any non-essential objects. That is, out of the output objects ⟨ ̄ φ, ̄s, assumps(·), assert(·), formal(·)⟩ that Pistis cre- ates, we remove ̄s, assumps(·), assert(·), formal(·) from the Lean file of our version, so we are only compar- ing the proof ̄ φ. We do this in practice by replacing euclid_sentence with have and removing comments. Figure 12: Bird’s-eye view of the completed Book I Prop. 6 artifact. In the codebase, these are interactive html artifacts (map.html). C.1 Step Fidelity The first rubric item reviewers were asked to rate is step fidelity. This was rated on a 0–5 scale for each formalization. Reviewers were asked to assess how well the Lean proof preserves the mathematical route of the textbook proof. The full scoring rubric is shown in Tab. 5. C.2 Pairwise Preferences For each proposition, reviewers answered three seven-tier pairwise preference questions. The interface did not show numeric values: the center choice indicated no preference, and choices farther to either side indicated stronger prefer- ence for one anonymized method. Tab. 6 summarizes the three pairwise criteria. C.3 Evaluation Interface Fig. 13 illustrates the website used for the human-expert eval- uation. Reviewers first completed an interactive tutorial that introduced the task, the anonymized presentation, and the available controls. For each proposition, the interface showed the textbook theorem and proof beside one formalization at a time, so reviewers could compare the formal proof against the natural-language argument without seeing the method identity. A live Lean server was available for querying proof states and inspecting what each line establishes. After exam- ining each formalization, reviewers assigned a step-fidelity score using the detailed 0–5 rubric shown in the interface, then reported pairwise preferences for mathematical trans- parency, textbook representation, and overall preference. D LLM as a Judge Complementing the human study, we assess faithfulness with an LLM-as-judge protocol using two judges: a closed model, Claude Opus 4.6 (whose radar is Fig. 4 in the main text), and an open model, GLM-5 (Fig. 14). For each proposition the judge scores the formalization on five independent 0–5 di- mensions, each defined by a strict rubric (Tab. 7): object cor- respondence, proof-step coverage, proof-structure fidelity, cited-dependency fidelity, and assumption/side-condition fi- delity. Pistis (Ours)Baseline (LeanEuclid)Baseline (Claude Code) OC PSC PSFCDF ASC (a) Book I OC PSC PSFCDF ASC (b) Book I OC PSC PSFCDF ASC (c) Book I Figure 14: GLM-5 LLM-as-judge faithfulness by book (axes as in Fig. 4). The full prompt given to each judge, which embeds the shared five-dimension rubric of Tab. 7, is: ToolPurpose and Role in Faithfulness check_step.pyThe agent’s only build tool in Phase B. Implements SF/SP/P checks for each φ ′ i . check_step --context Dumps exact hypotheses available at a proof node, showing context ∆∪φ ′ 1 ,...,φ ′ i−1 for proving φ ′ i . Operationalizes InContext predicate (Alg. 1, line 5). find.pyDeclarative query interface over indexed database of System E axioms, definitions, and previously proven propositions. Agent uses it during CreateLemmas (Alg. 1) to locate relevant axioms, or propositions. An example is that agents can search for all formal statements that conclude a specific property. scaffold_step.pyGenerates boilerplate backing files for each φ ′ i left as sorry after mapping stage. Table 4: Examples of custom Python tools provided to LLM agents during the filling stage. Score Description 0The Lean proof does not represent the textbook proof’s mathematical content. 1Only isolated textbook-like facts appear. 2Some essential steps are present, but important ob- jects, constructions, dependencies, or conclusions are missing or hidden. 3The main route is recognizable, but there are notable omissions, compression, ordering issues, or unclear automation. 4The essential steps and dependencies are represented with only minor formal differences. 5The formalization closely preserves the textbook’s mathematical route in a readable and recoverable way. Table 5: Step-fidelity rubric shown to reviewers. MetricQuestion Mathematical trans- parency Which formalization makes the mathe- matical argument more transparent and easier to follow? Textbook representa- tion Which formalization better represents the textbook proof? Overall preferenceWhich formalization is preferred over- all for the proposition? Table 6: Pairwise preference criteria used in the human eval- uation. You are an expert in Euclidean geometry, mathematical logic, and formal verification in Lean 4. Your task is to evaluate how faithfully a Lean formalization represents the mathematical content of a textbook proposition and proof from Euclid’s Elements. The textbook is the reference standard. You should not evaluate general elegance, maintainability, proof brevity, annotation quality, or code style except insofar as these affect mathematical faithfulness to the textbook. Formal encoding overhead -- such as extra type parameters (e.g. requiring a Line object where the textbook just names two points), additional binders for type-checking, imported helper lemmas whose internals are not shown, or sentence-level annotations -- is a routine artifact of formalization in a proof assistant. Do not penalize a formalization for these formal necessities . Evaluate only whether the mathematical content (objects, claims, proof steps, dependencies, assumptions) is faithful to the textbook. You will score the formalization on 5 independent metrics, each on a 0-5 scale, using the rubric below. [ RUBRIC -- the five-dimension scoring rubric ] For each of the 5 metrics, provide a brief justification (2-4 sentences) citing specific parts of the Lean code and textbook proof. After all justifications, output your final scores as five integers (0-5) in angle brackets in the following order: <object_correspondence, proof_step_coverage, proof_structure_fidelity, cited_dependency_fidelity, assumption_side_condition_fidelity> For example: <4, 3, 5, 4, 3> You MUST end your response with exactly one set of angle brackets containing the five scores. --- EVALUATION DATA --- TEXTBOOK PROOF: [ natural-language proof ] LEAN FORMALIZATION (Main file): [ Main.lean ] HELPER LEMMA FILES (backing proofs for each sentence-level step): [ each stepN.lean, separated by --- ] E Ablation Study Details This section details precisely how the ablation experiment was done. We compared the ablated arm, and full arm (OrderDecompose) using the same model Opus 4.8. Isolation: two worktrees, one arm at a time. Each arm runs in its own git worktree on its own branch, be- cause the arms require different repo contents: The ablated branch removes the tools, hooks, and skills the full method (OrderDecompose) relies on, so the two cannot share a working tree. We also never run the two arms concurrently since models may update a memory file, so simultaneous runs could cross-contaminate. Memory is wiped before every run and runs execute one arm at a time. Prevent Cheating. The answers (fully proven proposi- tions) exist in the git history, so agents could cheat. We could deny the raw usage of git in settings.json, but there are ways an agent can get around this, so instead we tell the agent what it is not allowed to do, and check suspicious behavior after the agent is done. We specifically tell the agent that reading anything out- side the repository or under the experiment folder, the eval harness, or any use of git, auto-fails the attempt. The prompts, and why the comparison is fair. Crucially, the ablated arm is not handicapped by ignorance of what it must produce: its prompt spells specifies how to output things, and what it is or is not allowed to do (for example that it cannot change the original formal claim). The two task prompts are: FULL (--my-method): Prove LeanEuclidF/<prop>/Main.lean end to end using the /faithful-prove skill... ABLATED (--ablated): Prove LeanEuclidF/<prop>/Main.lean -- fill every ’:= by sorry’ so it builds with ZERO sorry. Do NOT change the theorem statement, the ’(stepN : ...)’ claim types, or the ’-- @assumption (...)’ lines. Anything Euclid cites must be cited in Lean too... SHARED (both arms): Do NOT read anything outside this repository, or under reproducable_experiments/. Do NOT use git in any way. Either DISQUALIFIES the attempt -- AUTO-FAILED. No gaming the eval. What the transcripts show. The ablated arm characteris- tically fails by attempting the whole proof at once, running a massive lake build, then rewriting files and re-firing another massive build. The full method instead decomposes into small step lemmas built in fast scoped batches, making steady in-order progress. F Compile Performance Details The compile-time benchmark measures, per proposition, the wall-clock time to compile the faithful decom- posed proof (Book1/PropN) against the original proof (OldBook1/PropN) done by Murphy et al. (2024); both prove the same proposition_N and differ only in struc- ture. The procedure is: (1) wipe .lake/build (the cached Mathlib packages are left untouched, so Mathlib is never re- built); (2) build SystemE once, untimed; (3) compile each proposition cold, one at a time, and record its wall-clock time, with a per-proposition 1-hour cap. SMT is left uncapped (systemE.solverTime raised to 100000) so the 1-hour wall is the only cutoff, and both experiments were ran on the same exclusive node (one after the other, not at the same time). All runs used a single exclusive AMD EPYC 9634 (84-core) node. The ablation compile-time companion which eval- uates the artifacts the ablated, and OrderDecompose created (Fig. 5b) follows the same procedure on an AMD EPYC 9754 (128-core) node. The drivers, hard- ware metadata, and result CSVs are in the archive under reproducable_experiments/compile_time/ (and /ablation_study/compile_time/). G Further Refutation Examples The main paper showed one example of a refuta- tion. The released code contains further examples under LeanEuclidF/accept_refute/1.5/. Importantly, it also contains a type B refutation example (only type A was shown in the main text). Further, this folder contains example proofs that we accept that differ from Euclid’s own proof, showcasing that there are various ways to proove the same statement, to which our methodology can figure out which one to accept or refute formally. H Limitation Details Skipped propositions. We complete 30 of the 37 proposi- tions of Book I. The remaining 7 (Props. 24, 26–31) each require extending the current implementation of System E with a new primitive: an arc-length (circumference) measure for Props. 26–30, a circle-superposition rule for Prop. 24, and a horn angle for Prop. 31. System E is prior work (Avigad, Dean, and Mumma 2009), implemented in Lean by Murphy et al. (2024), and adding such primitives was decided to be out of scope. Reliance on the oracle. Pistis is oracle-guided: a human (or automated) oracle validates the Atomicity and Atomic Faithfulness of the map stage. While LLM oracle is a valid option, the quality of proofs may degrade compared to using a human oracle, which is a limitation of the current system. However, our methodology still minimizes human-oracle ef- fort so it is better than having the oracle complete the proof fully. Nonetheless, reducing oracle use is a natural direction for future work. (a) Tutorial(b) Textbook proof and formalization (c) Live Lean query(d) Step-fidelity scoring (e) Pairwise preferences Figure 13: Human-evaluation interface. Reviewers complete a tutorial, inspect each anonymized formalization against the textbook proof, query a live Lean server, score step fidelity with the rubric available in the interface, and finally record pairwise preferences across the three preference criteria. Score Description (a) Object Correspondence 0Object mapping invalid. The main objects are mapped incorrectly, making the formalization about different geometric entities than the textbook. 1Major object-role errors. Several important objects or roles are confused, omitted, or swapped in ways that materially change the proposition or proof. 2Partial object correspondence. The principal objects are identifiable, but important constructed objects, incidences, angle vertices, side correspondences, or role assignments are wrong or ambiguous. 3Mostly correct object correspondence with notable issues. Most objects are mapped correctly, but there are nontrivial local mismatches, such as an incorrect orientation, a missing constructed object, or a questionable side/angle correspondence. 4Faithful object correspondence with minor formal differences. All central objects and roles match the textbook. Minor discrep- ancies are limited to harmless naming, orientation conventions, or formal encodings that preserve the mathematical content. 5Fully faithful object correspondence. Every relevant textbook object, including constructed objects and their roles, is represented by the corresponding Lean object or relation with no substantive mismatch. (b) Proof-Step Coverage 0Textbook proof not represented. The Lean proof does not contain the textbook’s essential proof strategy or steps, even if it proves a related result. 1Minimal overlap with textbook proof. Only isolated pieces of the textbook argument appear; most essential proof moves are absent or replaced by unrelated reasoning. 2Some central proof steps are present, but multiple essential steps are missing, bypassed, or replaced by substantially different mathematical arguments. 3Mostly covered with significant gaps. The Lean proof includes the main proof strategy and several essential steps, but one or more important steps are absent, compressed beyond recoverability, or only indirectly represented. 4Nearly complete step coverage. All essential textbook steps are present, with only minor omissions or compressions that do not change the mathematical proof strategy. 5Every essential mathematical step of the textbook proof is represented in the Lean proof, allowing for routine formal elaboration and harmless decomposition into sublemmas. (c) Proof-Structure Fidelity 0Incompatible proof structure. The formal proof follows a fundamentally different dependency structure from the textbook proof. 1Severe structural mismatch. The proof contains some textbook-like steps but combines or orders them in a way that changes the argument’s mathematical logic. 2Partial structural fidelity. The broad strategy is recognizable, but important dependencies, branches, or contradiction structure are missing, reversed, or replaced. 3Mostly faithful structure with notable deviations. The proof follows the textbook’s main dependency pattern, but one or more significant structural components are altered, hidden, or not justified in the same way. 4Faithful structure with minor formal differences. The proof preserves the textbook’s dependency structure. Differences are limited to formal necessities, such as making implicit cases explicit or splitting bundled steps into lemmas. 5Fully faithful structure. The proof’s mathematical dependencies match the textbook argument closely, including construction order, use of intermediate facts, branching, contradiction structure, and final conclusion. (d) Cited-Dependency Fidelity 0Cited dependencies ignored or replaced wholesale. The formal proof does not use the textbook’s cited mathematical dependencies or equivalent principles, and instead relies on unrelated results. 1Major dependency mismatch. Most important cited dependencies are absent, replaced by stronger later results, or used in ways that do not correspond to the textbook. 2Partial dependency fidelity. Some cited dependencies are represented, but several important ones are missing, mismatched, or replaced by non-equivalent principles. 3Mostly faithful dependencies with significant caveats. The main cited dependencies are present, but at least one important dependency is replaced by a stronger or less directly corresponding formal result. 4Faithful dependencies with minor formal substitutions. The proof uses formal analogues of the cited dependencies. Any substitutions are mathematically equivalent or are unavoidable due to the formal library’s organization. 5Fully faithful dependencies. Each cited textbook dependency is represented by a direct formal analogue or a clearly equivalent formal principle used at the corresponding mathematical point in the proof. (e) Assumption and Side-Condition Fidelity 0Unjustified assumptions central to the proof. The proof relies on assumptions or side conditions that are not in the textbook, not implied by the setup, and materially affect the result. 1Major assumption problems. Several important side conditions are unjustified, too strong, or inconsistent with the textbook configuration. 2Partial assumption fidelity. Some side conditions are justified, but important assumptions remain unsupported, stronger than what the textbook permits, or mathematically unclear. 3Mostly justified assumptions with notable concerns. Most added formal obligations follow from the textbook setup, but at least one nontrivial side condition is unjustified, uncertain, or requires a stronger reading of the textbook than warranted. 4Faithful assumptions with minor gaps. Added assumptions and side conditions are justified by the textbook setup or standard Euclidean background. Remaining issues are minor, local, or evidentially uncertain without threatening the proof’s mathematical faithfulness. 5Fully faithful assumptions and side conditions. Every formal side condition used by the proof is justified by the textbook statement, the constructed configuration, prior established facts, or accepted Euclidean background principles. This score is compatible with automation when the automated obligations are mathematically justified. Table 7: The five-dimension rubric shown to the LLM judge. Each dimension is scored independently on the same 0–5 scale.