About, method and limits
What this site is
Open Math Atlas is an independent reader for the public openai/math repository. It is not affiliated with OpenAI. Manuscripts, their abstracts and the formalization catalogue are taken as-is from GitHub.
Where the data comes from
Families and manuscripts come from CONTENTS.md, disciplines from overview.tex, Lean statuses from lean/formalization.yaml and history from history.md. Every page shows the source commit and sync date.
Verification statuses
“Verified by Lean” means the repository links a Lean formalization for this family: the Lean software checked the formalized part of the argument. “To be verified” means no formal proof is referenced: the result is claimed in the manuscript and may contain errors. “Updated version” flags a correction in the repository history. No result is presented as validated by independent mathematicians.
Plain-language explanations
Each result page has one progressive article (essentials, going further, technical details), AI-generated from the repository summary and manuscript abstracts. They are unofficial and never replace the manuscript, which is authoritative.
Licence and credits
The content of openai/math is published by OpenAI under the Apache-2.0 licence. This site keeps the attribution and always links back to the original files.
Designed & built by
Jura Web Excellence
Independent web agency based in Poligny (Jura, France). Precise, high-performance websites with in-depth SEO, for businesses across France.