Metraipolis › archive › dc_fec2fb06b280

Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs — arXiv:2608.15432

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.15432
License (as archived): CC0-1.0
Archived: 2026-10-18T17:20:17.530Z
SHA-256 of the archived text: 02322b49e312b5e1b9ba09ba910dd45dacbd756be2ac4717606dd83b189b2609
Stable URL of this page: https://metraipolis.com/documento/dc_fec2fb06b280

How to cite

Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs — arXiv:2608.15432 — arXiv (en), https://arxiv.org/abs/2608.15432 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_fec2fb06b280 (Metraipolis archive dc_fec2fb06b280, sha256 02322b49e312b5e1b9ba09ba910dd45dacbd756be2ac4717606dd83b189b2609)

BibTeX

@misc{dcfec2fb06b280,
  title = {Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs — arXiv:2608.15432},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.15432},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_fec2fb06b280; sha256 02322b49e312b5e1b9ba09ba910dd45dacbd756be2ac4717606dd83b189b2609},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.15432. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: agenti e intelligenza artificiale (retro-catalogo arXiv: annunci del 2026-08-18 in cs.AI).
Categorie arXiv: Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2608.15432 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-18T16:29:13.800Z dalla pagina https://arxiv.org/catchup/cs.AI/2026-08-18?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).