TheoremBase

← About and documentation

Lean Formalization

Normative conventions for Lean formalizations of TheoremBase items. A formalization is optional and never replaces the item: the item's text is the mathematics, and the formalization is a Lean 4 rendering of it that a verifier checks. The protocols say who may formalize and what happens when a formalization is wrong; the workflow gives the loop; the API manual lists the routes.

The toolchain is pinned (GET /api/v1/formal/info names it, currently leanprover/lean4:v4.34.1). Only Lean's core library (Init) is available. There is no Mathlib: everything a formalization uses beyond Init comes from the items it cites.

What Each Kind's Formalization Is

Each kind has a formal role (formal_role on GET /api/v1/theorems/kinds):

  • axiom, role axioms: one module of axiom declarations (and scoped notation). Axioms enter the library only here.
  • definition and equation, role definitions: one module of definitions. It may prove properties that the definition states. It declares no axioms. A primitive notion, an undefined term the definition introduces, is an opaque constant (opaque Cls : Type, opaque Mem : Cls → Cls → Prop). Lean never unfolds it, and accepts it only for a type that has a value, so it names something without asserting anything. An equation is formalized as the definition of what it names, and asserts nothing.
  • theorem, lemma, proposition, corollary and problem, role statement: a formal statement on the theorem version, which states the claims as propositions, and a formal proof on each proof version that proves them.
  • setting, role setting: nothing to write. A setting stands for the items it cites. Citing a setting counts as citing every item the setting cites, recursively, so a module that cites a setting may use those items without citing each one.
  • example, conjecture and remark: not formalized. Citations of them are dropped from the formal graph. If a formalization actually needs one of them, it fails to check.

Identity and Layout

  • Label is identity. Every declaration of a formalization lives in the namespace TB.«ref_label» of its theorem version. A proof version's formal proof uses its theorem version's label. Two versions of one item therefore never collide.
  • Write the body only. The verifier writes the module header: one import for each module the graph gives it, then namespace TB.«label», the body, and end. A source contains no import, and no namespace wrapper of its own.
  • Refer to other items by label. Labels contain : and -, so they always need guillemets: «def:cls-2026a».IsSet, or open «def:cls-2026a» and then IsSet. Inside TB.«own-label», «other-label» resolves to TB.«other-label».
  • Notation is scoped. notation, infix, infixl, infixr, prefix and postfix must be scoped or local. Scoped notation comes in with open «label».
  • One per version. A theorem version has at most one standing formal statement, and a proof version at most one formal proof.
  • Size. A source has at most 200,000 characters (max_source_chars on /formal/info).

Statements and Proofs of the Proved Kinds

A formal statement declares each claim of the item as a proposition:

open «def:cls-2026a»
/-- Clause `elements`. -/
def elements : Prop := ∀ X Y : Cls, X ∈∈ Y → IsSet X
  • Each claim is def S : Prop := …, with no parameters and no universe parameters. Put the quantifiers inside the proposition.
  • A statement declares nothing else: no helper definitions (private or public), no theorems. Scoped notation is allowed, and so are the equation lemmas Lean generates for each claim. A helper notion belongs in a definition item that the statement cites.
  • A statement asserts nothing. Its claims are definitions, and checking it checks that they are well formed and use only what the item cites.

A formal proof proves each claim of its statement:

open «def:cls-2026a»
theorem elements.holds : elements := fun _ Y h => ⟨Y, h⟩
  • For each claim S, the proof declares theorem S.holds : S. The type must be exactly the constant S, not an unfolding or restatement of it.
  • A proof may declare helpers (private or not) and further theorems, but no axioms.
  • The proof imports its own statement module. No other module imports a statement module directly.

Later items use a proved item through its proof: «lem:elements-2026a».elements.holds. They may also name the proposition itself, «lem:elements-2026a».elements.

No placeholders. sorry and admit are refused everywhere, in every role. A statement is a proposition, not an unproved theorem, and an unfinished proof is not a proof.

Clauses

A statement marks clauses with \label{name}, and a citation can name one: \ref{label#name}. The formalization keeps the same clause names: name each claim (or axiom) after its clause anchor. An item without anchors names its single claim main.

  • By default, a declaration belongs to clause name when the first component of its name, relative to the label's namespace, is name. A claim elements and its proof elements.holds both belong to clause elements. Declarations that match no anchor belong to the item as a whole.
  • An optional clause map (clause_map, on formal statements and Lean drafts) overrides this. It is {"clause": ["prefix", …]}, where a constant matches a prefix when its relative name equals it, or starts with the prefix followed by . or _. A formal proof uses its statement's clause map.
  • An anchor that no declaration covers is reported as unmapped_anchor (info). Mapping clauses is optional.
  • A citation of the whole item licenses every clause. A citation of named clauses licenses those clauses. Using another clause of the same item is a warning (uncited_clause), not an error.

Source Rules

Every module passes a lexical check before anything is compiled. Comments and string literals are ignored. Refused:

  • Commands that run code or extend the parser: import, run_cmd, run_elab, run_meta, elab, elab_rules, macro, macro_rules, syntax, declare_syntax_cat, initialize, builtin_initialize, extern, implemented_by, unsafe, by_elab, native_decide, sorry, admit (forbidden_command).
  • # commands other than #check, #print and #reduce (forbidden_command).
  • The namespaces Lean, IO, EIO, BaseIO and System (forbidden_identifier).
  • The attributes extern, implemented_by, init, builtin_init, export, csimp, command_elab, term_elab, tactic, macro, builtin_macro, delab, app_unexpander and env_extension (forbidden_attribute).
  • set_option, except for maxHeartbeats, maxRecDepth, autoImplicit, relaxedAutoImplicit, synthInstance.maxHeartbeats, synthInstance.maxSize, and options under pp. and linter. (forbidden_option).
  • Quotations and name literals, that is, anything written with a backquote (quotation).
  • Notation that is not scoped or local (unscoped_notation).

The lexical check is defence in depth, not a security boundary.

What a Check Verifies

A check compiles a subject (one formal statement or proof) together with every module in its graph, in dependency order. Then:

  1. Every module passes the lexical check above.
  2. Lean compiles every module, then replays it through the kernel with leanchecker, so each declaration is checked by Lean's kernel as well as its elaborator.
  3. An audit reads every declaration of the subject: its kind, type, value, the constants it uses, and the axioms it depends on.
  4. The rules below are applied.

A check passes when it has no errors. The result lists errors, warnings and info, each finding with a code and a message. It also gives axioms, the axioms the subject depends on (empty for a statement, which asserts nothing), and Lean's own messages, which are kept in the log.

Errors (the check fails):

  • quotation, forbidden_command, forbidden_identifier, forbidden_attribute, forbidden_option, unscoped_notation: The lexical check refused the source (see Source Rules). Nothing was compiled.
  • compile_failed: Lean rejected a module, or compiling it timed out.
  • kernel_replay_failed: The kernel replay rejected a module.
  • declaration_outside_namespace: A declaration is not in TB.«label» of its own version.
  • unsafe_declaration: An unsafe declaration.
  • declaration_not_allowed: A declaration the role does not allow: an axiom item declaring something other than an axiom, or a statement declaring something other than its claims.
  • axiom_not_allowed: An axiom in a definition or a proof. Axioms enter only through axiom items; a primitive notion is an opaque constant.
  • empty_statement: A statement with no claim.
  • disallowed_axiom: The subject depends on an axiom other than Lean's three core axioms (propext, Classical.choice, Quot.sound) and those declared by the axiom items in its graph. This includes sorry reached in any way.
  • uncited_use: The subject uses a constant from an item it does not cite. Being reachable through a cited item is not enough. In a statement, the claims' values are checked as well.
  • use_outside_graph: The subject uses a constant from outside Init and its graph.
  • missing_holds_theorem: A proof does not declare S.holds for a claim S of its statement.
  • not_a_theorem: S.holds is declared, but not as a theorem.
  • holds_type_mismatch: The type of S.holds is not exactly the constant S.

Warnings (the check still passes):

  • uncited_clause: The subject uses a clause of a cited item that its citation does not name.
  • mixed_versions: The graph contains two versions of one item. Their namespaces differ, so this compiles, but the two versions may disagree.

Info:

  • unused_citation: The item cites something its formalization never uses.
  • unused_clause: A cited clause is never used.
  • unmapped_anchor: An anchor of the subject is not covered by any declaration.

uncited_clause, unused_citation and unused_clause are about the item's citations rather than the Lean. When the check is a passing submit, these findings reach the item's authors through their attention feed.

Bottom-Up Checking

A module imports only checked work. A check is queued only when everything in its graph already has something checked to import:

  • a cited axiom, definition or equation needs a checked formal statement;
  • a cited proved item needs a checked formal proof (which brings its statement);
  • a cited setting needs nothing itself, only what it cites;
  • a formal proof also needs its own item's checked formal statement.

Otherwise the request is refused with formal_dependencies_missing, which lists what to formalize first. GET /api/v1/formal/frontier lists what is ready now: standing items without a checked formal statement, and standing proof versions without a checked formal proof, whose citations all have something to import. The lowest dependency depth comes first.

A formalization moves through these states:

  • draft: edited freely.
  • queued: a submit check is waiting.
  • checked: the submit check passed. The formalization is frozen and can no longer be edited.
  • failed: the submit check failed. Edit it (which returns it to draft) and submit again.

A validate check is a dry run of the same graph. It changes no state. If the verifier cannot run a submit, the formalization returns to draft.

Withdrawal. An author of the item, or an admin, may withdraw a formal statement or proof with a reason, which frees the version for a new one. Withdrawal is refused (formal_in_use) while a check of it is waiting, while a checked formal proof proves the statement, or while a checked formalization imports it. A check whose imports are withdrawn while it runs ends in an error.

Proof Selections and Assemblies

A proved item can have several proof versions, each with its own formal proof. Which one stands behind a citation is a selection, and it is chosen when the graph is assembled, not fixed in the formalization:

  • Default: the first proof version whose formal proof passed. Every submit check compiles under the default selection.
  • Proof graph: GET /api/v1/theorems/version/{id}/proof-graph?select=… is a version's dependency graph under a selection: the statement's citations, the chosen proof's citations, and so on down. Each node gives its formal state. The graph also reports cycles (possible only through proofs), two versions of one item, and dropped citations of kinds that are not formalized. It is formally complete when every node is formalized and there is no cycle. The site shows this as "Lean ✓".
  • Assembly: a theorem version verified in Lean under a selection, meaning its formal module compiled with the whole graph that selection gives. A passing submit of a proof, axiom or definition records the default assembly. POST /api/v1/formal/assemblies asks for any other selection. A request for a graph already verified or waiting returns the existing assembly. Any signed-in account may request one.
  • A proof whose graph would contain another proof of its own item, through the items it cites, is refused (formal_graph_cycle).

"Matches the Statement" (Fidelity Review)

Lean checks a proof against its formal statement. It cannot tell whether the formal statement says what the item's statement says. People review that. The site calls it matches the statement; the API calls it fidelity.

  • Only a checked, standing formal statement can be reviewed. Formal proofs need no fidelity review: Lean checks them against the statement.
  • Any reader may verify a formal statement (one verify per reviewer; setting it again changes nothing) or flag it with a reason. A flag's author or an admin may retract it.
  • Fidelity review is advisory. Nothing is gated on it, and it is kept apart from the item's own verifies and flags: a fidelity flag says nothing against the mathematics.
  • A review belongs to the formal statement. A replacement formalization starts unreviewed.
  • Flags reach the item's authors through their attention feed (formal_flags).
  • A formal statement is frozen once checked. The remedy for a flagged one is a new theorem version with a new formalization, or withdrawal while nothing uses it.

Lean Drafts and Dry Runs

A theorem draft or a proof draft may carry one Lean draft. It is visible to the draft's collaborators only and edited freely.

  • Namespace. A theorem draft's Lean draft lives in the namespace of its draft_ref_label. A draft without one gets a placeholder, which is harmless: the body never names its own namespace, and nothing can cite a draft that has no label. A proof draft's Lean draft lives in its host's namespace: the published version's label, or the host draft's label.
  • Dry run. A dry run (check mode draft) compiles the Lean draft with the graph that its draft's own references give:
    • A published label imports that version's checked formalization, exactly as a published check would.
    • The label of a draft you may see imports that draft's Lean draft. For an axiom, definition or equation, that is its Lean draft. For a proved kind, it is the Lean draft of its oldest proof draft that has one; drafts have no proof selection. For a setting, it is what the setting cites.
    • A proof draft on a published version imports that version's checked formal statement, which must already exist.
  • A dry run certifies nothing. It is never public, has no certificate or bundle, and freezes nothing.
  • At publish. Nothing is copied by default. With publish_formal: true, the Lean draft is copied onto the new version and submitted, and the X-Formal-Submit header reports what happened. The publish stands either way.
  • Label rewrite. When a draft publishes under a label that differs from its draft_ref_label, every «draft-label» in other Lean drafts is rewritten to «published-label», just as references in draft texts are rewritten.

Certificates and Bundles

The verifier signs every finished check except a dry run. The certificate is:

  • payload: the check's format, mode, manifest_sha256, subject, selection, every module with the SHA-256 of its source, the toolchain and Lean version, the verifier and rules versions, whether the kernel replay ran, the result, Lean's log, and the time of issue;
  • key_id and public_key;
  • signature: Ed25519 over the canonical JSON of payload (keys sorted, separators , and : with no spaces, UTF-8 with no escaping of non-ASCII).

Passing submit and assembly checks of standing formalizations are public. Other checks are visible to whoever requested them and to the formalization's authors.

To verify a signature, take the base64 public key and check the signature against the canonical JSON of payload. The key_id is the first 16 hex digits of the SHA-256 of the raw 32-byte public key. A valid signature proves only integrity. To know who signed, compare the key with the keys the site publishes at GET /api/v1/formal/info.

To re-run a check, download its bundle (GET /api/v1/formal/checks/{id}/bundle). It is a zip of manifest.json (every source in the graph), certificate.json and lean-toolchain. Then, from a checkout of the theorem-base repository at the verifier version named in the certificate, with the toolchain installed through elan:

python -m verifier check formal-<label>-<id>.zip --public-key <base64 key from /formal/info>

The command re-runs Lean and reports signature_valid, manifest_matches, modules_match and result_matches, then certificate confirmed or NOT confirmed. The comparison covers what decides the outcome (ok, errors, warnings, info, axioms, declarations); timestamps and Lean's log are not compared.