AI researchers built a proof-checking system that cares less about whether a formal math proof compiles and more about whether it thinks the same way the original does.
The system, called Pistis, uses an agentic, oracle-guided search to turn natural-language mathematical proofs into formal Lean proofs that mirror the original argument's structure, not just its conclusion. The team defined five necessary conditions for a formalization to count as 'faithful,' then built a search method called OrderDecompose that tracks citation dependencies between steps and blocks shortcuts that reach the right answer through the wrong logic. A companion refutation search flags gaps or errors in the source proof itself. Applied to the first three books of Euclid's Elements, Pistis closed proofs that baseline methods could not finish in a 12-hour budget, and its output compiled more than 33 times faster than prior approaches.
That distinction matters because most automated theorem provers optimize for a proof that works, not one that reflects human reasoning - useful for confirming a theorem is true, useless for checking whether someone's argument for it holds up. In blinded tests, both human reviewers and an LLM judge preferred Pistis's proofs to prior work by wide margins, and the system surfaced actual gaps in Euclid's 2,300-year-old text and its translations.
Using Euclid as the test case is a neat trick - his axioms are about as clean as mathematics gets - but the real question is whether this kind of faithfulness check survives contact with the messier, less axiomatic proofs mathematicians write today.