Found first: a primary source the press has not covered yet.
Kevin Buzzard, who runs the Xena Project at Imperial College London, checked the Lean code in OpenAI's October 2026 release of 722 mathematics papers and found that 38 of roughly 290 files with accompanying Lean code do not state the main theorem of the paper they accompany, let alone prove it. The post lays out a four-step verification standard Buzzard argues any AI-generated Lean proof should pass.
What the source says
Of OpenAI's 722 papers, roughly 45% came with Lean code. Buzzard checked those files against the stated theorems and found 38 do not state, let alone prove, the main theorem of the paper they accompany. He sets out four verification steps: does the Lean statement match the informal statement in the PDF; does the code compile; does a lake comparator run confirm the proof; and does a paranoid kernel check rule out exploited bugs in Lean itself. He states that frontier AI models are capable of performing all four checks, though at potentially high computational cost.
Why it matters
OpenAI's October release was widely reported as a landmark in AI-driven mathematics. Buzzard's check finds that 38 of roughly 290 Lean files fail the most basic test: confirming the code states the theorem the paper claims. The four-step standard he outlines is replicable by any lab or researcher with access to Lean tooling. His post also notes that for many papers in the dump, the remaining three verification steps have not yet been completed.