---
title: "AI Safety Formalization Atlas"
author: "Mario Brcic"
author_url: "https://mariobrcic.com/about-me/"
canonical_url: "https://mariobrcic.com/ai-safety-atlas/"
summary: "An open Lean 4 library and ledger of machine-checked AI-safety mathematics, by Mario Brcic."
license: "all-rights-reserved"
---
> *Canonical HTML version: [https://mariobrcic.com/ai-safety-atlas/](https://mariobrcic.com/ai-safety-atlas/). © Mario Brcic. All rights reserved.*

# AI Safety Formalization Atlas (AISFA)

The open Lean library for formal AI-safety results.

The AI Safety Formalization Atlas is an open Lean 4 library of machine-checked AI-safety mathematics: shared definitions, theorems and counterexamples, all kernel-checked with no `sorry`. 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.

## 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.

## Links

- Repository: https://github.com/mbrcic/ai-safety-formalization-atlas
- Documentation: https://mbrcic.github.io/ai-safety-formalization-atlas/
- Software DOI (all versions): https://doi.org/10.5281/zenodo.21483033
- License: Apache-2.0