AI can produce checkable proofs; the specification still determines what they establish

The guarantees concern modeled RISC-V programs and specified failure conditions, with inputs below 64 MB. They do not certify entire libraries, all memory errors, or the x86 and ARM environments where much of this software actually runs. The public repository currently lists 61 proved entry points in 26 libraries—a released subset of the larger reported effort. [1][2]

OpenAI’s October 26 release takes a related idea into research mathematics: it publishes natural-language arguments and Lean artifacts for claims concerning local smoothing and the Exponential Time Hypothesis. The company is organizing external academic examination, and calls the manuscripts raw research material. Its mathematical output was generated October 18 and formalized October 19; the complexity-theory output dates to October 16–17. Those research dates remain separate from publication. [3][4]

Axiom’s October 26 announcement concerns formalizing an existing mathematical achievement: the classification of finite simple groups. It reports a 24-day effort involving mathematicians, engineers and agent teams, producing about 43.1 million Lean lines. That scale describes the project; it is not an independent measure of correctness or scientific importance. [5]