An open Lean library
AI Safety Formalization Atlas
The open Lean library for formal AI-safety results.
The AI Safety Formalization Atlas (AISFA) is an open Lean 4 library of machine-checked AI-safety mathematics: shared definitions, theorems and counterexamples, all kernel-checked with nosorry. Testing can show that a system fails, never that it cannot fail. A proof speaks about every case, so the Atlas gives such claims one kernel-checked surface, where each result names its objects once and others can reuse them.
What it is
A Lean 4 library plus a ledger. The library holds the mathematics. It covers computability and logic (Rice, halting, Gödel, Tarski, Löb, Chaitin), social choice (Arrow), learning (no-free-lunch), control (Ashby, Touchette–Lloyd), oversight, reward corruption, knowability and causal models. The ledger records where each result came from, which external formalizations exist for it, their licenses and pinned revisions, and what each development does and does not cover.
Who it is for
- Lean formalizers and AI-safety theory researchers who develop, reproduce or audit formal claims.
- Formal-methods and safety engineers who use its cores as reference specifications inside a larger assurance argument.
- Anyone who can state a safety property precisely. Stating it exactly enough to check does not require knowing what a proof assistant is.
What makes it different
The kernel settles whether a proof is valid. Whether it proves the right statement is still a human question, and the Atlas treats that question as the bottleneck. Scope is stated per result: citation grades are conservative, conditional results name each assumption they do not prove, and the gaps are published as generated numbers rather than left to be found. A theorem is not a safety case. Applying one to a real system takes a separate, reviewed interpretation step.
Open to contributions
Humans and proof agents work in the Atlas together. Language models can draft the Lean, but the kernel decides whether it holds, so trust never routes through the model. Open conjectures, contributor tasks and issue forms give a way in, with or without Lean.
Cite it
The software has a DOI covering all versions: 10.5281/zenodo.21483033. The repository's CITATION.cff carries the current version and release date.
More
Bring a question.
If you can make a safety property precise, this is where it becomes something machine-checked.
Get in touchLast updated .