OpenAI's math proofs passed Lean checks, then got a 4-page patch 5 days later

一份通过检查的证明，为什么在 5 天后补写了 4 页？当 AI 逼出做完的真相

OpenAI released 10 math results on Aug 1 with Lean 4 proofs that all compiled. Five days later the paper grew from 249 to 253 pages to fix a gap in an edge case. Terence Tao proposed that priority for AI-generated proofs should go to the first team that delivers the full package—paper, explanation, and formal certificate—not just the code. The post breaks “done” into five levels: candidate generated, rules checked, intent aligned, peers understood, community absorbed. Only one of the ten results has reached level five so far.

Why it matters: A concrete case study that makes the gap between machine verification and human understanding tangible. OpenAI's results, Tao's proposal, and the 5-level staircase framework all deliver substance. Not scored higher because this reads as deep commentary rather than breaking new...