A GUIDE TO THE COLLECTION
Clear links.
Precise boundaries.
AgentLemma is an independent catalogue of public proof releases across AI labs and agents. It is not affiliated with the labs listed. We index evidence and source revisions; we do not claim to cover every lab or every proof.
What the labels mean
- Upstream reports proofs
- The source publishes proof artifacts and reports results. AgentLemma has not independently run the checks.
- Formalization materials listed
- An OpenAI result family has scope notes or a paper in its formalization catalogue. Read the notes for exact coverage.
- In formalization catalogue
- This exact manuscript appears in
lean/formalization.yaml as having a formalized main result. Read the scope notes for coverage and limitations. - No Lean materials listed
- No corresponding materials were identified in the current source catalogue. This does not establish whether the mathematics is correct.
No proof checks have been run by this explorer. Availability, proof scope, successful verification, and peer review are distinct questions.
Sources and syncing
Each source has a separate pinned revision, import date and successful refresh time. The authenticated owner updater refreshes all registered sources, retaining the last good version of a source on failure. Unattended hourly refresh requires the owner’s connected Site plugin; page polling alone does not refresh GitHub. OpenAI descriptions retain upstream attribution. Other entries index artifact paths and our summaries. Source licenses and third-party terms are linked in the register.
Read the upstream Apache-2.0 license ↗Created and maintained by Yassir Laaouach. Original mathematics and proof artifacts remain attributed to their authors and labs.