Atlas
Atlas is a website that lists the papers in OpenAI’s October 2026 maths release, with other groups’ checking reports linked beside each one. For the paper about π, two groups both report the proof accepted and label its coverage differently. Atlas shows the two labels side by side.
Limits: Each group reported its own labels and proof checks, and Atlas has not rerun them. The suggested matches between paper theorems and Lean statements are unreviewed.
The two reports on the π paper are by MathVet and by Carlos Toledo’s cert-machine. Atlas also uses Neal McBurnett’s Lean tooling.
Lean is a program that checks mathematical proofs.
