Mathematicians are pushing back on the large batch of AI-generated proofs OpenAI released this week, saying most of the work lacks the transparency and verification the field expects, TechCrunch reported Thursday. Researchers at the University of Cambridge and King's College London also found a mismatch between one of OpenAI's written proofs and its formal, machine-checkable version.

What Happened

OpenAI late Tuesday posted a collection of mathematics manuscripts produced by an unreleased internal model, spanning about 20 fields. The Primary Wire reported Wednesday, citing SiliconANGLE, that the release included 722 papers; TechCrunch counts 719 proofs, and the figures below are TechCrunch's.

According to TechCrunch, only 10 of the manuscripts include the model's chain of reasoning, and just 42% had been formalized in Lean, a programming language in which a proof can be checked by computer.

RelatedOpenAI Says Its Models Broke Into Two Outside Data Sites and Left It Out of Their Answers

Fields medalist Terence Tao criticized a pattern in which problems are solved autonomously by AI prompters who have no interest in the broader field and little grasp of what the outputs mean, TechCrunch reported. Harvard mathematician Melanie Wood said no human understands the results at the moment they are released, adding "now the work begins."

The Cambridge and King's College London researchers examined a result on a Navier-Stokes problem, which concerns the equations that describe fluid flow. They found discrepancies between OpenAI's natural-language explanation and the Lean code meant to capture it, and concluded that automatically formalized Lean proofs should not be trusted without the same peer review and scrutiny applied to other proofs.

Why It Matters

Lean files were supposed to be the answer to the scale problem. Hundreds of papers in many subfields cannot be refereed quickly, but a proof that compiles in Lean has been checked by machine. The Navier-Stokes finding exposes the weak link: the computer verifies the statement as it was encoded, and if the translation from prose to code drifts, a valid formal proof can certify something other than the claimed result.

The missing reasoning traces matter for a different reason. Mathematicians judge new work partly by whether its methods are understandable and reusable. A finished proof without the path that produced it gives other researchers less to build on, and makes errors harder to find.

Context

The Advisory Group on Mathematics and AI had asked frontier labs not to test advanced problems on proprietary models and to publish machine-readable metadata linking natural-language proofs to their formal counterparts. TechCrunch reported that OpenAI did not fully follow either recommendation. The article did not include a response from OpenAI.

When it released the papers, OpenAI said it would publish Lean proofs for more of them and fund events where mathematicians review the results, according to SiliconANGLE's earlier report.

What to Watch

The next phase is ordinary peer review: specialists working through individual claims, starting with the most prominent ones. Also watch whether OpenAI releases more reasoning traces and formal proofs, whether it publishes metadata tying formal statements to the written claims, and whether further formalization mismatches surface as outside researchers check the Lean files.