Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

How to use the Atlas

Each Atlas page is about one result from OpenAI’s mathematics release. It puts the paper’s theorem beside the Lean statement OpenAI wrote for a computer to check, and shows what outside groups found.

How to read a result

  1. Find a result. Press / and type a few words from its title, or click a subject on the map and then a dot. Each dot is one result and its papers.
  2. Read the first screen. The paper’s theorem is on the left. On the right is the statement OpenAI wrote in Lean, a language in which a computer checks every step of a proof. The line underneath says how the two were linked and whether anyone has reviewed that they say the same thing.
  3. See what the outside groups found. They answer two separate questions, each in its own words: whether the Lean says what the paper claims, and whether OpenAI’s proof passed Comparator, the program that checks the proof against the Lean. A pass means the proof proves the Lean statement, not that the Lean says what the paper says.
  4. Use the tabs for more. They hold the full papers, every Lean statement, each group’s full reasons with a link to its report, and related reading.

Try it on one result: the irrationality exponent of π

Words you will see

Family
OpenAI’s group of papers about one result. Each dot on the map is a family.
Lean statement
A theorem written in Lean with its proof left out (the file says sorry in its place). OpenAI supplies the proof in a separate file.
Comparator
The program that checks OpenAI’s proof against a Lean statement. A pass does not show that the Lean means what the paper says.
The outside groups
MathVet and Carlos Toledo’s cert-machine compared each family’s Lean statements with OpenAI’s description of the result and gave their verdicts in their own words. Other groups report Comparator runs.
Possible match
A paper theorem linked to a Lean statement by a citation in the Lean source, by an AI agent’s reading of both, or by words they share. No review that they mean the same thing is recorded.

Every term, in the glossaryThis guide as a page

Atlas collects these reports and links to them. It runs no checks itself.

Press ? to open this guide and Esc to close it.

How to use the Atlas

Each Atlas page is about one result from OpenAI’s mathematics release. It puts the paper’s theorem beside the Lean statement OpenAI wrote for a computer to check, and shows what outside groups found.

This page is for anyone opening the Atlas for the first time: four steps, and the few words you will see on every page.

Plectis Atlas: compare maths papers with the reports that check them, video on YouTube, 5 minutes 27 seconds

How to read a result

  1. Find a result. Press / and type a few words from its title, or click a subject on the map and then a dot. Each dot is one result and its papers.
  2. Read the first screen. The paper’s theorem is on the left. On the right is the statement OpenAI wrote in Lean, a language in which a computer checks every step of a proof. The line underneath says how the two were linked and whether anyone has reviewed that they say the same thing.
  3. See what the outside groups found. They answer two separate questions, each in its own words: whether the Lean says what the paper claims, and whether OpenAI’s proof passed Comparator, the program that checks the proof against the Lean. A pass means the proof proves the Lean statement, not that the Lean says what the paper says.
  4. Use the tabs for more. They hold the full papers, every Lean statement, each group’s full reasons with a link to its report, and related reading.

Try it on one result: the irrationality exponent of π

Words you will see

Family
OpenAI’s group of papers about one result. Each dot on the map is a family.
Lean statement
A theorem written in Lean with its proof left out (the file says sorry in its place). OpenAI supplies the proof in a separate file.
Comparator
The program that checks OpenAI’s proof against a Lean statement. A pass does not show that the Lean means what the paper says.
The outside groups
MathVet and Carlos Toledo’s cert-machine compared each family’s Lean statements with OpenAI’s description of the result and gave their verdicts in their own words. Other groups report Comparator runs.
Possible match
A paper theorem linked to a Lean statement by a citation in the Lean source, by an AI agent’s reading of both, or by words they share. No review that they mean the same thing is recorded.

Every term, in the glossary

Atlas collects these reports and links to them. It runs no checks itself.