Artificial intelligence is making history in the field of basic scientific research. Recently, independent developer Charlie Reams successfully completed a formal proof of the ternary Goldbach conjecture using Claude Code. This breakthrough produced a total of 194,000 lines of zero-sorry Lean 4 code, and all mathematical reasoning passed rigorous machine verification.
The Machine’s Eagle Eye: Autonomously Uncovering and Fixing 11 Flaws in a 13-Year-Old Proof
During this arduous proof process, AI demonstrated extreme rigor beyond traditional human peer review.
While running and deriving, the AI autonomously discovered 11 critical issues in the original proof published by mathematician Harald Helfgott in 2013. These successfully uncovered flaws covered multiple dimensions, including incorrect constants, inequalities that did not hold, discrepancies in cited data, and confusion over major arc scales, and the AI patched each of them one by one.
On this basis, researchers further reduced the additional external assumptions on which the proof relied from the initial 5 to only 2 existing publicly available numerical verification results, thereby greatly advancing the construction of a rigorous closed loop for the proof.
Driving a Paradigm Shift: “Proof Completion” in Mathematics Is Moving Toward a Machine-Verifiable Era
This milestone event not only cracked an important problem in the history of mathematics, but also, at a deeper level, drove a fundamental shift in the entire mathematics community’s criteria for judging “proof completion”—from traditional peer review taking great strides toward a formalization that relies entirely on machine verification.
