Glossary

The words this atlas uses for what has and has not been checked, in plain terms. Pages show these definitions when you hover a marked word.

A

A Lean statement with no confident match: Neither the Lean text nor the catalogue words picked out one paper statement clearly, so the atlas pairs nothing and lists the closest statements instead.

Candidate pairing: A possible link between a paper statement and a Lean statement, selected automatically from words they share. Atlas records no review that their mathematical meanings agree.
cert-machine: Carlos Toledo’s audit of the release, one of the two outside readers. It re-runs every Lean statement through Comparator with nanoda switched on, reads each family’s Lean statements against the headline clause by clause, and decides finite parts of some papers with exact code.
Comparator: A program that tests OpenAI’s separate proof against a Lean statement. Acceptance means that Lean’s proof verifier accepts the configured theorem using only the allowed axioms. It does not establish that the statement means the same thing as a paper’s theorem.

Definition hole: A definition a configuration lists for the solution to supply. Comparator compares it by name and type only, so its body comes from the solution and must be read there.

Earlier edition: A paper OpenAI later replaced with a revised edition. The atlas keeps the earlier edition, marked, beside the current one in the same family.
Exact check: A calculation that decides a finite claim using exact arithmetic or exhaustive enumeration, implemented independently of the paper. A successful calculation establishes the specific tested property. An undecided result is not evidence that the claim is false.

Family: OpenAI’s group of related papers about a main result. Each group has a number in its catalogue; Atlas uses that number to link the papers and reports about them.

Headline result: The main claim OpenAI’s catalogue gives for a family. A family’s Lean statements may state all of it, part of it, or a supporting step.
HOL Light: A proof assistant separate from Lean. Ben Knill’s reports use it to prove selected steps in some of the release’s papers. They also test deliberately incorrect examples that the program should reject.

Lean: A language and program for writing mathematical statements and proofs, then verifying each proof step. A verified proof establishes the statement as written; comparing that statement and its definitions with a paper is a separate task.
Lean kernel: The small core of Lean that checks every step of a proof. Everything Lean accepts passes through it.
Lean statement (a Comparator challenge file): A file stating a theorem in Lean, usually with sorry in place of its proof. Comparator’s settings identify the statement to verify, the definitions the proof may supply and the axioms it may use. OpenAI provides its proof separately.
Local vocabulary declarations: Definitions written in the Lean statement file, in addition to those imported from Mathlib. To judge whether the statement means the same thing as a paper theorem, compare these definitions with the paper as well.

Mathlib: The community-maintained library of mathematical definitions, theorems and proofs written in Lean. OpenAI’s release specifies the version it uses.
MathVet: One of the two outside readers. It reads each family’s Lean statements against the headline under a published rubric, with help from a model, and runs Comparator itself. Its verdict and note are quoted in its own terms.

nanoda: A second proof-verification program for Lean, written independently in Rust. Comparator can run it alongside Lean’s own verifier. The report for each run states which verifiers were used when that information is available.

Outside readers: MathVet and Carlos Toledo’s cert-machine, who each read every family’s Lean statements against its headline, independently of OpenAI and of each other, under their own published rules. Each states its own method; the atlas quotes their verdicts and notes and adds none of its own.

Paired by a citation in the Lean source: The Lean source cites a paper statement, and Atlas records that citation. Atlas records no review that the statements mean the same thing.
Paired by the release’s own declaration: OpenAI’s release explicitly links the Lean statement to a paper statement. Atlas records that link, with no recorded review that the statements mean the same thing.
Paired from the catalogue’s words, as a fallback: When Lean wording gives no clear paper match, Atlas uses a possible match selected from OpenAI’s catalogue description, provided it belongs to the relevant paper. Atlas records no review that their mathematical meanings agree.
Paired from the Lean statement’s own words: Atlas selects a possible paper match from words in the Lean statement, when one statement has a sufficiently clear match. Atlas records no review that their mathematical meanings agree.
Permitted axioms: The axioms a configuration allows a proof to use, here the three standard ones: propext, Classical.choice and Quot.sound. A replay shows which ones a proof actually uses.

Re-run: An independent group’s attempt to verify OpenAI’s proof with Comparator. Atlas records the group’s reported result and the release version used. Atlas has not repeated the attempts.
Reading page: The atlas’s HTML version of a paper, converted from its TeX at the pinned commit. The PDF stays the reference; a page that did not convert in full lists what is missing.

Scope note: OpenAI’s note on what a family’s Lean statements cover, in lean/docs of the release. The atlas quotes it beside other people’s readings.
sorry: Lean’s placeholder for a missing proof. A Lean statement leaves its proof as sorry on purpose; the proof is in OpenAI’s separate solution module.

Withdrawn paper: A paper OpenAI removed after the release, with a notice explaining the gap. The atlas keeps it, marked, under the family it was listed in on release day.