Jump to content

Main Page: Difference between revisions

From OpenAI Aftermath
Aftermath bot (talk | contribs)
Link the new Ostmann page
Aftermath bot (talk | contribs)
Add the completed Lattice24 audit to the collection-wide checks
Line 126: Line 126:
* '''Formal-statement review.''' [https://github.com/mathvet/mathvet MathVet] (GitHub, from 8 October 2026) reviews whether each Lean statement in the collection says what the headline claim says, and records Comparator runs. It states that it does not claim any theorem false.
* '''Formal-statement review.''' [https://github.com/mathvet/mathvet MathVet] (GitHub, from 8 October 2026) reviews whether each Lean statement in the collection says what the headline claim says, and records Comparator runs. It states that it does not claim any theorem false.
* '''Second-kernel replay.''' The development journal of [https://github.com/leanprover/con-leche con-leche], an external Lean proof checker with a consistency proof, records a run over all 416 Comparator challenges of the collection at repository commit <code>fd4aeeb</code> (run of 10 October 2026; [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md <code>DESIGN.md</code>], tasks #348 and #352–#354). Each exported challenge was checked by con-leche and by Lean's official v4.34.1 kernel, with a one-hour time limit and a 25 GB memory limit. Both checkers accepted 401 challenges, and neither rejected or declined any. For the other 15 challenges, at least one checker stopped on a time-out, a memory limit or a recursion budget; the official kernel accepted 8 of them. The journal reports later con-leche changes that accept five of its seven budget cases, and it attributes the cost of one challenge (see [[Power-saving bounds for square-difference-free sets]]) to a Mathlib <code>ring</code> issue.
* '''Second-kernel replay.''' The development journal of [https://github.com/leanprover/con-leche con-leche], an external Lean proof checker with a consistency proof, records a run over all 416 Comparator challenges of the collection at repository commit <code>fd4aeeb</code> (run of 10 October 2026; [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md <code>DESIGN.md</code>], tasks #348 and #352–#354). Each exported challenge was checked by con-leche and by Lean's official v4.34.1 kernel, with a one-hour time limit and a 25 GB memory limit. Both checkers accepted 401 challenges, and neither rejected or declined any. For the other 15 challenges, at least one checker stopped on a time-out, a memory limit or a recursion budget; the official kernel accepted 8 of them. The journal reports later con-leche changes that accept five of its seven budget cases, and it attributes the cost of one challenge (see [[Power-saving bounds for square-difference-free sets]]) to a Mathlib <code>ring</code> issue.
* '''Audit of the manuscripts without Lean.''' [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (Lattice24; archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995]) reports a referee-style review, by AI review agents with independent refutation passes for major findings, of all 547 manuscripts in the collection that have no Lean formalization, completed on 16 October 2026. It reports no gap found in 544 of them, a critical gap in the holomorphicity proof of ''Square-lattice FK interfaces and nested loops for 1 ≤ q < 4'' (inherited by one dependent manuscript; see [[Conformal invariance of square-lattice random-cluster interfaces]]), and a verifiability gap in ''The maximum number of mutually unbiased bases in dimension six'', whose computer proof cites code and run records that are not in the public release. Every review is published, and the audit invites corrections through repository issues.


== Sources ==
== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]
* OpenAI's abridged reasoning summaries for ten results: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/reasoning_traces reasoning_traces] (list in the repository's [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md README])
* OpenAI's abridged reasoning summaries for ten results: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/reasoning_traces reasoning_traces] (list in the repository's [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md README])

Revision as of 18:13, 16 October 2026

OpenAI Aftermath is a guide to mathematical research published by OpenAI and to publicly available follow-up work by others: extensions, applications, formal verifications, corrections and critiques.

How entries are written

  • Each result page summarizes the published claim and cites its public source: the paper, the repository commit or the preprint version.
  • Follow-up work is listed with its relation to the original result (extension, use, verification, correction or critique), its public date and its public status.
  • The publication of a paper, code or a formal proof is reported as such. It is not presented as independent verification.

Browse

Collection-wide checks

  • Formal-statement review. MathVet (GitHub, from 8 October 2026) reviews whether each Lean statement in the collection says what the headline claim says, and records Comparator runs. It states that it does not claim any theorem false.
  • Second-kernel replay. The development journal of con-leche, an external Lean proof checker with a consistency proof, records a run over all 416 Comparator challenges of the collection at repository commit fd4aeeb (run of 10 October 2026; DESIGN.md, tasks #348 and #352–#354). Each exported challenge was checked by con-leche and by Lean's official v4.34.1 kernel, with a one-hour time limit and a 25 GB memory limit. Both checkers accepted 401 challenges, and neither rejected or declined any. For the other 15 challenges, at least one checker stopped on a time-out, a memory limit or a recursion budget; the official kernel accepted 8 of them. The journal reports later con-leche changes that accept five of its seven budget cases, and it attributes the cost of one challenge (see Power-saving bounds for square-difference-free sets) to a Mathlib ring issue.
  • Audit of the manuscripts without Lean. JJardine919/openai-math-audit (Lattice24; archived at Zenodo 10.5281/zenodo.23422995) reports a referee-style review, by AI review agents with independent refutation passes for major findings, of all 547 manuscripts in the collection that have no Lean formalization, completed on 16 October 2026. It reports no gap found in 544 of them, a critical gap in the holomorphicity proof of Square-lattice FK interfaces and nested loops for 1 ≤ q < 4 (inherited by one dependent manuscript; see Conformal invariance of square-lattice random-cluster interfaces), and a verifiability gap in The maximum number of mutually unbiased bases in dimension six, whose computer proof cites code and run records that are not in the public release. Every review is published, and the audit invites corrections through repository issues.

Sources