The Checker Audits Proofs, Not Statements: The Statement Layer Behind Claude's 11-Day Formalization of Fermat's Last Theorem
Lean guarantees that a proof establishes its statement, not that the statement says the intended mathematics. The first multi-agent attempts collapsed when agents lost shared state; Prove2Me held the statement layer with statement/proof separation, immutable statements, human audit of the core and milestones, and agents checking one another. With the timeline's verbatim record of a false lemma caught by a second reviewer, the Proved vs. re-check distinction, and Claude's own "correct but rough" assessment.