Formal-proof fidelity audit
Which “formally solved” Erdős problems rest on an unconditional Lean proof, and which silently assume an unproven result.
A proof can be sorry-free and
#print axioms-clean and still prove the problem only conditionally, by taking a deep
theorem as a hypothesis parameter the axiom check never sees.
How the audit works, and what it cannot do →
Problems the frozen AI-contributions wiki lists as a full solution, where the hosted Lean proof proves the goal only under an undischarged assumption.
The wiki’s claim may rest on a different or informal argument; the point is that the machine-checkable proof, as written, is not unconditional. #print axioms invisible marks the cases an axiom check alone would pass.
Axis 1 · the proof
Is the proof unconditional?
Read mechanically from each hosted Lean proof: the axioms it uses and the Prop hypotheses it takes as parameters. A fact, not a judgment.
machine · deterministicAxis 2 · the statement
Is that the right problem?
Whether the formal statement faithfully states the boxed problem. A passing proof checks the statement, not that the statement is the problem.
signed · named reviewerWhere an independent human review of the GPT-5.2 candidates (gpt-erdos) and this proof audit both speak to a problem. They read different artifacts, the informal argument versus the hosted Lean proof, so where they diverge is the signal.
| # | Proof | Conditional on | Statement | External claim |
|---|---|---|---|---|