descriptive claim
AlphaProof produced proofs in Lean and used Lean to verify its solutions to the competition problems.
Unresolved speaker · Mathematics Just Changed Forever — Kevin Hartnett · 26 Oct 2026
In their words
The transcript segments this claim was taken from
“It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal-level score, and the way in which it, it solves the problems is by outputting Lean proofs and then using Lean to verify them.”57:10Report a misattribution
0.95how strongly it was put, not whether it is true
0.85importance to the conversation
0.99confidence the claim was read correctly