In October 2026 OpenAI released 722 mathematics papers written by an internal model, grouped into 372 results. They range from the Birch–Swinnerton-Dyer formula for most elliptic curves to a counterexample to Sidorenko's conjecture. This is an independent index of that release. For every result it shows what is claimed and whether it has been machine-checked, and it builds pages that recompute something real wherever the mathematics allows it.
Read the claims as claims. The release itself says its results are "at different stages of verification", and that some of the unformalized ones "could have issues". A green Lean badge means the release's formalization catalogue lists at least one of a family's papers as having its main result proved in Lean. A dashed Lean, uncatalogued badge links to the release's own scope note for a Lean development that is not in the catalogue. Some of those prove the whole result and some prove only part of it, so read the note. Neither badge means anyone here ran it, or that a mathematician has read it. This site is not affiliated with OpenAI. The papers are theirs, under Apache-2.0, and every link goes to their repository.
Tiers came from a first pass: six model readers worked through every family against one rubric, and humans review each one before anything is built. The bars below are the families in each field.