Undermines· moderateORCH-E023
AlphaProof: Lean-verified silver-medal IMO performance, peer-reviewed in Nature
- what the source states
- The abstract reports that AlphaProof, a reinforcement-learning system operating on formal mathematics in Lean, solved three of the five non-geometry problems at the 2024 International Mathematical Olympiad, including the competition's hardest problem (P6), and that combined with AlphaGeometry 2 the system achieved a score equivalent to a silver medal — reported by DeepMind as 28 of 42 points, one point below the gold threshold. Solutions were formally verified in Lean. Some problems required multi-day computation rather than the contest time limit.
- what we infer
- The most rigorously verified item in this evidence line: Lean machine-checking means the mathematical correctness is not a matter of opinion, and Nature peer review covers the methodology. As a challenge to Penrose the relevant limitation is conceptual rather than methodological, and it is substantial — competition problems are known to be solvable within an existing framework by construction, which is exactly the category the Penrose-side response says was never in dispute. Filed as undermining because the accumulation of formerly-human-only mathematical performance is what the critics' argument rests on, and graded moderate because that argument is contested at ORCH-E025.
- limitations
- IMO problems have known solutions within existing frameworks; not framework extension.
- Multi-day computation rather than contest conditions for some problems.
- Corporate-authored research about the authors' own system, though Lean verification substantially offsets this.
- Bears on the motivation rung only.