OpenAI publishes ten claimed advances in mathematics and theoretical computer science with Lean 4 certificates under Apache-2.0

Sources: repository, HN discussion
Summary: OpenAI published a repository of ten claimed results in mathematics and theoretical computer science, each accompanied by a Lean 4 formalization under Apache-2.0, targeting Lean 4.32.0 with mathlib and containing ten named proof files including ConnesRigidity.lean. The results have not been through peer review. The repository routes independent checking through Comparator, and the postmortem above records as part of the response to kernel bug 14576 that comparator.live now runs the external checker nanoda by default and that nanoda is tracked daily.
Why it matters: The formalizations are machine-checkable artifacts rather than a benchmark score, which is a materially different evidence standard for an AI capability claim, though the postmortem above bounds a Lean certificate to current versions of both the kernel and the external checker.
Follow-up: A claimed rebuttal of the Connes rigidity result circulated on Hacker News but the hosting site returned HTTP 403 from this environment, so it is unverified and excluded. Recheck it.