AI Safety Formalization Atlas

Machine-checked mathematical infrastructure for AI safety.

AISFA is an open Lean 4 library for formalizing, reproducing, auditing and extending mathematical results relevant to AI safety: shared definitions, theorems, counterexamples, open conjectures, and reviewed bridges from the mathematics to AI systems.

• Whitepaper: The AI Safety Formalization Atlas: a machine-checked memory for AI safety mathematics (preprint, 2026; DOI for all versions)
• Software: DOI for all versions; latest release v0.8.0, DOI
• Start: Open in Codespaces — the toolchain provisions itself and one example compiles in minutes — then pick a first task. Prefer local? scripts/setup.sh --pointer (docs only, no Lean) or scripts/setup.sh --quick (one example). Full detail: Get started.

At a glance

EXACT/EQUIVALENT = conservative citation grade (completely formalization-covered source statements). RELATED = value-based scoped formalization, with documented deltas; it does not by itself mean unfinished, but postponed until justified (paper residuals stay in provenance). The two grade rows count claim results, not formalization records: one result may carry several, and an artifact row's own grade is never in these numbers. Detail: formalization status; by mathematical area; per-source reports under docs/status/sources/.

Statement coverage of the 28 graded sources is 300 Yes / 17 Partial / 208 No / 41 Beyond, graded by hand against the printed text in source-coverage-audit.md. Builds are reproducible against pinned Lean and Mathlib, and CI checks the axioms of every headline declaration. What the atlas does not have is counted too: Library status.

Why AISFA

AI-safety mathematics lives in papers, prose, scattered proofs and incompatible formalisms, so every citation rebuilds the model and words it a little differently. AISFA turns claims into reusable, machine-checked objects with explicit assumptions, provenance and interpretation boundaries.

It keeps three questions apart, because they fail independently:

1. Is the proof valid? The Lean kernel decides this.
2. Is the formal statement the claim in the source? Graded per statement, by hand, in the coverage audit.
3. Does the result say anything about a real AI system? Only through a separately reviewed bridge, and a kernel-checked proof does not by itself establish it.

Explore

The longer argument

The situation. AI systems are gaining capability faster than anyone is gaining understanding of them, and they are being deployed on the near side of that gap. Decisions about what is safe to build and release are being made now.

Why mathematics. Most of the evidence behind those decisions is empirical — evaluations, red-teaming, incident review. That evidence is one-sided by construction: testing can show that a system fails, never that it cannot. As capability grows the space of behaviors grows with it, so the fraction any test suite covers shrinks. A proof is the only form of evidence that speaks about every case. Its assumptions can still stop matching the system, which is why nothing here is read as a claim about a real system without a separate reviewed step.

Why now. The same systems that make this urgent are what make it tractable. Autoformalization has turned mechanization from a specialist craft into ordinary work: models draft the Lean, and a kernel that does not care who wrote it decides whether the proof holds. Trust never routes through the model. What this accelerates is implementation, not discovery — stating the right property, and reviewing whether it matches the system, still move at human speed. AI is the subject, the instrument, and the deadline at once.

What the kernel settles is whether a proof is valid. Whether it is the right statement stays a human question — and that is the bottleneck. Stating a safety property exactly enough to be checkable is the hard part, and it does not require knowing what a proof assistant is.

Bring a question. Alignment, control, oversight, interpretability, robustness—if you can make a safety property precise, this is where you turn it into something machine-checked. Impossibility and possibility both count (e.g. DeepMind debate reproduced as LAND-DEBATE-001; continuous free lunches BY-022 open).

If the question is causal identifiability, the AISafetyAtlas.Causal.* modules carry finite categorical Bayesian networks over an ordered field, interventions and regret, Everitt's structural models and influence diagrams, and the objects the MAIS-A2 agenda phrases its query problems over — a semialgebraic class, the K(G) parameter chart, and a rational-weight query layer. Two behaviourally identical models with different graphs are exhibited, not assumed.

If you want an open question instead of a theorem, conjectures.yaml tracks precise statements — mostly causal-identifiability questions from MAIS's open-problems agenda, together with three singular-learning problems from its A6 and A7 agendas, plus one question from an information-theory survey. Every conjecture entry names a closed, compiling Prop, and the ledger also holds determine-problem specifications and printed problems with no Lean object at all; defining one asserts nothing about its truth, and the rows that are settled say so and name the proof. Worked models establish that the hypotheses can be met where a row says so, and the rows whose antecedents still have no witness disclose it — the MAIS-O26 row needs a solution to MAIS-O24, and no such solution is exhibited in this tree, so that statement may hold vacuously. See conjectures.

Solutions other people submitted to those problems are transcribed and checked here too, and what checking them found is a generated table: MAIS submitted solutions. It separates two facts a reader will otherwise merge — whether the mathematics checks, and which artifact the ledger row is graded against — because a submission can be fully proved and still be graded against the printed problem rather than against itself. Checking someone's mathematics is not peer review and not co-authorship, and no row says a submission is accepted upstream.

If the question is singular learning, the AISafetyAtlas.SingularLearning.* modules carry the local-pair machinery for the two-layer linear network x ↦ BAx against the square loss: the local invariant as MAIS-A7 defines it, by the band volume vol{|L(w') − L(w)| < ε} ≍ ε^λ (log 1/ε)^(m−1), together with the elimination chart, the orbit reduction and the chamber calculus that the reduced-rank fibre needs. It is an off-root facade, so import AISafetyAtlas.SingularLearning is explicit rather than carried by the root. Three MAIS problems sit on top of it, and two of the answers are unconditional: MAIS-O7 is false — isO7Counterexample refutes the opposing-staircases conjecture at every positive scalar target — and MAIS-O77(b) holds, pair (1,1) at every point of every nonterminal critical set. The Morse lemma this rests on is not ours: eight modules of the Tau Ceti development are vendored under vendor/TauCeti/, Apache-2.0 and pinned.

Some results in that layer are conditional, and the atlas says which. MAIS-O77(a) and the first two clauses of MAIS-O70 are proved over propositions this tree states and does not prove — the real-Wishart eigenvalue law chief among them. A theorem frontier → X reads exactly as strong whether the frontier is true or false, and neither a green build nor a clean axiom audit tells the two apart, so each assumption is named, frozen, given unconditional stress artifacts, and recorded with who it is owed to and what discharging it would cost. Two of the three are owed to the candidate solution, which cites them rather than deriving them; one is owed to the printed source. The table is the MAIS source report, and scripts/check_frontier_evidence.py prints the whole debt on every run. Passing that check is not evidence a frontier is true.

If the question is control, AISafetyAtlas.Control carries Ashby's variety bounds and Touchette–Lloyd's information limits at their printed quantifiers: a regulator cannot hold an outcome steadier than its own repertoire allows, and feedback improves on open loop by at most the information the sensor actually supplied. If it is the reach of a no-free-lunch argument, AISafetyAtlas.Learning.Sharp proves the characterization in both directions — performance is algorithm-independent exactly on priors closed under relabelling the search space — together with the count saying almost no prior is one. Several of the survey's control rows are still empty; see open work. Reading these across domains: symmetry and impossibility.

Who this is for

• Lean formalizers and AI-safety theory researchers (and proof agents) developing, reproducing, or auditing formal claims.
• Formal-methods and safety engineers using cores as reference specifications or to pressure-test assumptions in a larger assurance argument.
• Contributors willing to make a claim precise, including with help from formal-methods collaborators or agents.

A theorem is not a system safety case. Applying it to a real system needs a scoped reviewed bridge where relevant, implementation evidence, and the rest of the assurance argument. Bridge review validates a scoped interpretation; it does not by itself prove operational safety.

Library status

Primary goal: develop, reproduce, and machine-check formal AI-safety results (including using shared foundations to discover new ones), for AI safety and related computable governance/ethics. Also: keep cores usable as reference specifications downstream. Not a goal: growing counts, or growing a product monorepo in-tree. Reusable structure and honest grading over volume.

The counts are under At a glance.

What the atlas does not have, stated here rather than left to be found. The table above counts registry rows, not the tree: the working tree pins far more public names than it records results. Three ratios a reader is entitled to before reading further:

• Statement coverage of the graded sources: 300 Yes / 17 Partial / 208 No / 41 Beyond, across 28 sources. A No is a printed statement the atlas does not have. The per-statement grading is source-coverage-audit.md.
• Scope debt: 4 cells graded Narrower or Mixed are owed a closure, a regrade, an unclosability proof or a cost, and each declares one; 2 more record a closure. The standing rule is scope ≥ print, so each of those is a defect until discharged. scripts/check_coverage_audit.py computes both figures.
• Witness debt: 3 theorems of 2,686 are ungrounded and 31 reach no worked application under AISafetyAtlas/Examples/. The second is the number that says how much of the library the build actually exercises; the first also counts a registry citation, and a citation is not built. Two of the three are leaves, and both cannot be witnessed at all: their antecedent is a type the tree proves empty. They are recorded in docs/status/witness-vacuity.json with the emptiness proof named, stay inside both counts, and leave the work queue.

None of these is an argument against the results that are here. They are the numbers that make the results legible, and they are generated rather than asserted.

Published units must rebuild under documented commands and the axiom policy (Validation).

Depending on the Atlas from your own project

Add it to your lakefile.toml. There is no Reservoir entry, so require it by git:

[[require]]
name = "ai-safety-formalization-atlas"
git = "https://github.com/mbrcic/ai-safety-formalization-atlas.git"
rev = "v0.8.0"

v0.8.0 is the published release and is what that stanza gets you. The module list below describes the working tree, which is ahead of it — anything added since the tag is not in v0.8.0, so check the tag's own module list before depending on a name you read here.

Then import AISafetyAtlas.Knowledge (or whichever module below) and instantiate the statements at your own types — they are unbundled maps, not an atlas-specific agent structure, so your State does not have to be one of ours.

Three things worth knowing before you do:

• Your toolchain has to match, exactly. Lean v4.33.0, Mathlib at the v4.33.0 tag, and Foundation and PFR pinned by commit — PFR is a research development whose API is not stable across revisions, which is why it is pinned that way. If your project already sits on a different Mathlib, this is not a drop-in.
• You inherit every dependency, Mathlib, Foundation and PFR, because Lake resolves requirements per package rather than per import. Splitting the counting half of Ashby's law out of the PFR-importing module (Control.VarietyCounting) means less has to be elaborated, not less fetched.
• warningAsError is this package's option and does not reach yours — verified, not assumed.

Domain imports

Prefer a facade over the full root import when starting a proof. Some parents re-export their domain (Wireheading, Compositional, Control, Oversight.JointObservation); the kernels do not, so Knowledge and Preference specializations are imported one by one, and Verification supplies its mathematical base without the AgentBehavior and Robot bridges. Inference re-exports its own subtree, so one import carries the whole Wolpert development; Knowledge.Devices is the transport between the two and imports both. InformationTheory deliberately has no parent — each module is one result and none is built on the others, so there is no surface for a facade to aggregate. Causal has no parent either, for a stronger reason: the domain holds two different objects, and an aggregating import would force a consumer of one to take the other. Causal.Model is a causal Bayesian network — a graph with conditional probability tables. Causal.StructuralModel is Everitt's structural causal model, influence diagram and SCIM, where the randomness sits in exogenous variables and the endogenous variables are related deterministically. Neither is a special case of the other as rendered here. Import contracts per module: AISafetyAtlas.lean.

Two senses of "control" live in this tree. Inference has Wolpert's, which is a device controlling another device; Control has Ashby's and Touchette–Lloyd's, which is a regulator against a disturbance. No theorem identifies them.

import AISafetyAtlas.Control       -- Ashby variety bounds + Touchette–Lloyd limits (facade)
import AISafetyAtlas.Control.RequisiteVariety -- or one module at a time
import AISafetyAtlas.InformationTheory.Fano   -- peers, no facade: import the one needed
import AISafetyAtlas.InformationTheory.DataProcessing
import AISafetyAtlas.InformationTheory.ChannelCapacity
import AISafetyAtlas.Combinatorics.PermInvariance -- relabelling-invariance machinery
import AISafetyAtlas.SingularLearning         -- local pairs for the two-layer linear network (off-root facade)
import AISafetyAtlas.Learning      -- finite NFL cores
import AISafetyAtlas.Learning.Sharp -- the permutation-closed characterization, both directions
import AISafetyAtlas.Preference    -- planner/reward unidentifiability (kernel)
import AISafetyAtlas.Preference.Override -- overriding human reward functions
import AISafetyAtlas.Preference.Regret   -- half-maximal regret not ruled out
import AISafetyAtlas.Wireheading   -- reward channels, self-modification
import AISafetyAtlas.Compositional -- rectangles, hyperproperties, networks
import AISafetyAtlas.Oversight.JointObservation -- coalition evidence, coverage, collision
import AISafetyAtlas.Knowledge     -- exact knowability, decoders, indistinguishability (kernel)
import AISafetyAtlas.Knowledge.Embedded -- restriction, meshing, self-measurement limits
import AISafetyAtlas.Knowledge.Embedded.Composition -- complement ⇒ proper inclusion; positive boundary
import AISafetyAtlas.Knowledge.Embedded.Finite -- finite cardinality gap ⇒ proper inclusion
import AISafetyAtlas.Knowledge.Temporal -- time-indexed knowability, collisions, delay
import AISafetyAtlas.Knowledge.Ambiguity -- finite fibre ambiguity, counting obstruction
import AISafetyAtlas.Knowledge.SelfReference -- model as part of the state it models
import AISafetyAtlas.Knowledge.Accumulation -- window ambiguity bounds over time
import AISafetyAtlas.Knowledge.Devices -- transports between the kernel and inference devices
import AISafetyAtlas.Knowledge.Check -- executable checkers, each with an agreement theorem
import AISafetyAtlas.Inference     -- Wolpert devices: weak/strong inference, control, physical knowledge
import AISafetyAtlas.SelfAwareness -- process composition and complete-awareness limits
import AISafetyAtlas.Oversight.Debate -- doubly-efficient debate (vendored; NOT on the root import)

Cross-surface consumer pattern (compositional boundary + nonzero regret + preference certificate): AISafetyAtlas.Examples.WorkbenchConsumers. Primary names live in each facade docstring; root import AISafetyAtlas remains available.

Oversight.Debate is the one facade root import AISafetyAtlas does not bring in: it wraps a vendored development that declares its names in the root namespace, so it is imported on its own and audited separately. Its module docstring gives the reason.

Epistemic scope

A machine-checked proof establishes its encoded mathematical statement. It does not by itself establish that the statement fully captures an informal AI-safety claim. Math results and AI-system bridges are separate layers; bridges need human review.

Citation grades stay conservative: do not raise EXACT/EQUIVALENT by weakening fidelity. RELATED is a useful core with an explicit scope delta; it does not by itself mean unfinished, and residual paper gaps remain documented. A bridge may be REVIEWED while the formalization stays RELATED (e.g. robot). See the v0.7 release scope and docs/guide/methodology.md.

Repository contents

• registry.yaml records every result: claim rows carrying source provenance, and artifact rows for formalizations and public Lean surface the library develops or reproduces on its own account.
• AISafetyAtlas/ contains attributed Lean integrations.
• Main.lean is atlas-check: it reads a finite model as JSON and prints the verdict together with the declaration that certifies it, so a question about a particular model can be answered without writing Lean. Every checker behind it is paired with a theorem saying it agrees with the Prop. See the guide — including what the output is not, which is a proof term the kernel has checked for that instance.
• CONTRIBUTING.md explains how to propose and verify changes.
• ROADMAP.md presents the public strategy and contributor entry points.
• STATE.md reports the current phase, blockers, and next tasks.
• conjectures.yaml records source-faithful conjecture statements that compile in Lean without a proof, together with settled rows; an open row asserts nothing, and a settled one names its proof.
• tasks.yaml is the maintained task board; docs/guide/contributor-tasks.md is generated from it.
• docs/ is split by role — start with the documentation map:
  • docs/guide/ — methodology, open work, model notes, tasks
  • docs/status/ — generated coverage tables and indexes
  • docs/provenance/ — discovery search + external reproduction
  • docs/interpretation-reviews/ — bridge review packages and evidence
  • docs/releases/ — release evidence notes

Lean API

Downstream proofs need only the root import:

import AISafetyAtlas

The stable entry points are conventional theorem names under domain namespaces:

• AISafetyAtlas.Computability.rice and rice_code_iff
• AISafetyAtlas.Computability.halting_problem
• AISafetyAtlas.SocialChoice.arrow
• AISafetyAtlas.SocialChoice.Utility.arrow
• AISafetyAtlas.Logic.chaitin_incompleteness and chaitin_bound
• AISafetyAtlas.Logic.godel_first_incompleteness and godel_second_incompleteness
• AISafetyAtlas.Logic.tarski_undefinability
• AISafetyAtlas.Logic.loeb
• AISafetyAtlas.Verification.rice
• AISafetyAtlas.Verification.AgentBehavior.no_behavioral_safety_verifier
• AISafetyAtlas.Verification.Robot.action_safety_unverifiable
• AISafetyAtlas.Composition.independent_iff_rectangular and not_independent_of_failed_splice
• AISafetyAtlas.Observability.factors_through_iff_fiber_invariant and no_perfect_monitor_of_collision
• AISafetyAtlas.Compositional — rectangularity, hyperproperties, and network symmetry
• AISafetyAtlas.Wireheading — objective, corruption, and goal-preservation cores
• AISafetyAtlas.Preference — preference-unidentifiability and override cores
• AISafetyAtlas.Oversight.JointObservation — covers_iff_no_collision, the certified finite checker decideCoverage, the repair boundary, and the bounded portfolio target (landscape LAND-JOINTOBS-001; see the joint observation model)
• AISafetyAtlas.Logic.lawvere_fixed_point — the types-and-functions Lawvere fixed-point wrapper (not the categorical statement; see CLM-LAWVERE-CCC-001)
• AISafetyAtlas.Learning.no_free_lunch and no_free_lunch_supervised — finite NFL cores
• AISafetyAtlas.Learning.Sharp.nfl_adaptive_iff_permInvariant — the sharp form: performance is algorithm-independent iff the prior is closed under relabelling the search space. With card_closedUnderPermutation_nonempty (almost no prior is) this is the result that says where an NFL argument may be used at all
• AISafetyAtlas.Control — Ashby and Touchette–Lloyd behind one import. ashby_variety_ge and ashby_logVariety_ge are the law in counting and logarithmic form, ashby_variety_ge_isSharp says it is attained; outcome_eq_comp and exists_strategy_forcing are §11/14; controlLoss_eq_condMutualInfo identifies control loss with a conditional mutual information and entropyReduction_le_of_openLoopBound bounds feedback's advantage over open loop. Every one of those is in namespace AISafetyAtlas.Control, whichever of the ten modules declares it, so each is importable one at a time; see the facade docstring for the map
• AISafetyAtlas.InformationTheory.Fano and .DataProcessing — Fano's inequality at printed constants and the data-processing inequality with its equality case, both over an arbitrary probability space. .ChannelCapacity is the noiseless capacity, owned by neither
• AISafetyAtlas.Combinatorics.PermInvariance — what relabelling-invariance forces. spectrum_eq_iff_mem_permOrbit (the multiset of values is the complete invariant), closedUnderPermutationEquivSet (invariant families are families of multisets), and exists_perm_rel_not_iff (no non-trivial relation survives). Domain-neutral, reusable, and the shared half of the NFL result above
• AISafetyAtlas.Knowledge — start with the knowability model. Knowable in decoder form, knowable_iff_no_collision, IndistinguishabilityWitness, and the informativeness boundary Knowable.mono / not_knowable_comp. JointObservation's coverage laws are this kernel applied to q.observe
• AISafetyAtlas.Knowledge.Embedded — restriction, inference maps, meshing, and the abstract self-measurement no-gos (EQUIVALENT to Breuer 1995 §3.5; see LAND-SELFMEAS-002)
• AISafetyAtlas.Knowledge.Temporal — KnowableFrom / KnowableAt, CollisionAt, EvidenceMonotone, DelayedKnowable. Keeps knowing the state as of s from evidence at t apart from knowing the current state at t, which is the difference distributed snapshots exploit
• AISafetyAtlas.Knowledge.Ambiguity — ambiguity counts the target values one observation leaves open. card_image_le_of_knowable is a counting obstruction that never names a colliding pair; ambiguity_le_of_comp says coarsening never lowers the shortfall. Finite counting only — no probability or entropy
• AISafetyAtlas.Knowledge.SelfReference — where the observation stops being an arbitrary map: the observer's model is a component of the state. Complete self-knowledge holds iff nothing else is in the state (selfComplete_iff_subsingleton_rest), so it is achievable only degenerately
• AISafetyAtlas.Knowledge.Accumulation — ambiguity about a window of targets. Widening never reduces it and never exceeds the product of the steps. Growth itself is not a theorem: it depends on dynamics, and both extremes are exhibited
• AISafetyAtlas.SelfAwareness — active observation-and-predictive-modelling of internal processes during a bounded horizon. process_not_self_aware is the local strict-extension result; limited_self_awareness lifts it through recursive process composition without assuming the awareness graph is acyclic

Every facade above carries a short primary-surface table and explicit non-claims in its module docstring; read that before the declarations. Residual gaps are recorded per cluster, not in one place: Compositional, Wireheading, Preference and Oversight.JointObservation in the A1–A3/B1–B3/B7 re-verification, and the Knowledge facades in the self-measurement kernel note and the landscape sweep. The process-compositional BY-044 interpretation has its own source map and fidelity residual.

Landscape declarations — results the library develops or reproduces on its own account rather than as coverage of a catalogued source. Most carry root_import: true — the count is in the table above; most are the Knowledge, Oversight and Compositional entry points listed above. The full list, with the declarations each row owns, is generated: landscape index, and how the rows stand to one another is relations.

The one that has no facade bullet above:

• AISafetyAtlas.Explainability.attribution_impossibility (DASH trilemma; not BY-029/BY-042 without a separate statement map)
• AISafetyAtlas.Composition.independent_iff_rectangular (LAND-COMP-001, native): a global safe set decomposes into independent per-agent contracts iff it is splice-closed; certified multi-agent counterexamples in AISafetyAtlas/Examples/Composition/
• AISafetyAtlas.Observability.no_perfect_monitor_of_collision (LAND-OBS-001, native): perfect monitoring is exactly hazard observability; see compositional boundaries

Reproduced external formalizations that carry no Lean interface are pinned in registry.yaml, listed in the landscape index, and rebuilt with scripts/reproduce_isabelle.sh:

• Gibbard_Satterthwaite (LAND-GS-001, Isabelle/HOL; Arrow-session provenance related to BY-007). Lean consumer interface: AISafetyAtlas.SocialChoice.gibbard_satterthwaite (LAND-GS-002, vendored SocialChoiceLean GS closure)
• no_free_lunch_ML (LAND-NFL-001, Isabelle/HOL; the Shalev-Shwartz–Ben-David PAC no-free-lunch — the formal core of "generalization needs inductive bias" — distinct from the Wolpert NFL survey rows BY-020/BY-021; see CT-2 triage)

The Rice verification bridge concerns properties of partial input/output behavior; AgentBehavior is a downstream consumer that models encoded agents and total behavioral safety verifiers. The independent Robot bridge concerns total reactive action traces under an explicit effective switching certificate and reduces directly to the halting problem. The Logic layer covers Chaitin (BY-015, vendored KolmogorovMathlib), classical Gödel I/II (BY-013, Foundation), Tarski undefinability (BY-016), and Löb (BY-027); see logic incompleteness. Neither classical nor bridge theorem asserts that a particular AI system or practical verification task satisfies its model. Generated checks in AISafetyAtlas.Examples.Registry compile every registry-listed declaration through the root import. The hand-written examples in AISafetyAtlas.Examples.PublicAPI additionally protect the intended theorem signatures; the explicit targets in scripts/lean_build_targets.txt also build worked examples, most of which are intentionally outside the public root import. The twelve AISafetyAtlas.Examples.Causal.* modules are the exception and are on the root import. Kernel axiom cleanliness of the headline surface is checked by scripts/check_print_axioms.py.

External reproduction of the Kolmogorov pin (upstream checkout, not the vendored tree):

scripts/reproduce_chaitin.sh

Get started

regenerate python3 scripts/generate_registry_views.py · gate ./scripts/agent_gate.sh · build lake build

Nothing here needs the whole picture: take the row that matches what you have and ignore the rest.

No toolchain needed for the first row — the validators need only Python 3.12 or newer and its standard library. One check reads a ledger through PyYAML and is skipped with a notice if that is absent; pytest and ty are likewise optional locally. CI installs all three, so none of them is optional on a pull request:

scripts/setup.sh --pointer   # cheap validators only; no Lean toolchain

For anything touching Lean, one command provisions everything — it installs elan if it's missing, fetches the prebuilt Mathlib, builds, and runs the validators:

scripts/setup.sh --quick   # fast path: toolchain + Mathlib cache + one example compiling
scripts/setup.sh           # full: whole build closure + validators (run before a Lean PR)

Zero local install: open the repo in GitHub Codespaces — or any editor's Dev Container — and the toolchain provisions itself on first boot (via --quick, so the cold start stays short; run the full scripts/setup.sh before submitting a Lean change).

lake exe cache get   # fetch prebuilt Mathlib — skips an hours-long local compile
lake build
xargs lake build < scripts/lean_build_targets.txt
./scripts/agent_gate.sh

The repository pins Lean, Mathlib, and every transitive dependency: lake-manifest.json is the lock. Build from it directly — do not run lake update unless you are deliberately bumping a dependency, as it re-resolves floating revisions off the pinned set. Released Lean files follow the strict-trust and build-closure policy.

Contributing

There is always something to do. Get started routes what you have to the one file it belongs in; bounded units are in contributor tasks.

Working with an LLM or agent: draft against a facade, then lake build → agent_gate.sh → check_print_axioms.py (see CONTRIBUTING). Green Lean is kernel validity of the encoding — not source match, model adequacy, or system interpretation.

Full tracks and rungs: CONTRIBUTING.md. Issue forms for proposals that change coverage, dependencies, or the public Lean interface.

Tooling an agent may use

None of this is required to contribute, and none of it is a dependency — the gate and CI use only what lake-manifest.json pins. It is listed because an agent that does not know these exist re-derives things the ecosystem already has.

A semantic search is not evidence. These indexes are not pinned by this repository, so a miss is not reproducible and cannot support a claim that a result does not exist. docs/agent/policy/lean-reuse-sources.md says what such a claim may cite, and lists the libraries worth searching before you write a proof of your own.

License

Apache-2.0. Individual external formalizations remain subject to their own licenses; the registry records those licenses when verified.