- The AI-generated math results OpenAI released total about 400, spread across more than 700 papers, according to the source. They cover several fields, including combinatorics, geometry, number theory, and theoretical computer science.
- OpenAI said it formalized about 300 of the key results from 719 papers in Lean. Lean is a programming language that helps a computer check whether a proof is logically correct. The source describes this as about 42%.
- Mathematicians said that even with Lean code, they must separately check whether a proof actually matches the claims in the paper. Some papers also drew criticism that their reference lists are short and their source citations are insufficient.
- Stanford mathematician Jared Duker Lichtman rated results on progress toward the Riemann hypothesis, a special case of the Hodge conjecture, and results related to the 4-dimensional Kakeya conjecture as important. This is the assessment of a researcher who spoke to reporters, and the article does not confirm that verification of these results was complete at the time of the source.
The fact that there is a paper with a short reference list catches my eye. To check whether a citation was left out, you end up having to read the manuscripts one by one, but the article doesn't make clear who would review the results close to 400 or in what order. The fact that 3 papers were withdrawn because of a sign error also suggests that public results are hard to treat as settled right away. I'm curious how you mark the verification status when your lab refers to this kind of material.