According to the report, only 10 of the 719 manuscripts included releases of model chain-of-thought material. It also says 42% of the released proofs had not undergone formalization. AGMAI’s guidance called for machine-readable metadata linking natural-language and formal artifacts; TechCrunch says OpenAI did not provide that correlation. The group’s first request was also that advanced open problems not be tested on proprietary models.
A paper by researchers at the University of Cambridge and King’s College London identified at least two discrepancies between a natural-language proof and Lean code for an OpenAI result derived from the Navier-Stokes equations. The authors say those discrepancies do not necessarily disprove either solution. The report does not establish that OpenAI’s mathematical claims are false, nor does it provide an independent review of every manuscript.