LeanFrontier v0.2.0

The first library release since the corpus grew. v0.1.1 had 2 modules on Lean v4.33.0-rc1; v0.2.0 has 102 accepted modules on Lean and Mathlib v4.34.1, in 15 top-level areas, from algebra, analysis and combinatorics to number theory, probability and topology. They come from several producers and model families; the catalogue records which.

Using it

[[require]]
name = "LeanFrontier"
git = "https://github.com/carlok/LeanFrontier.git"
rev = "v0.2.0"

lake update
lake exe cache get   # Mathlib's prebuilt files; without it, lake build compiles Mathlib
lake build

import LeanFrontier brings in everything; each subject module can also be imported alone. Validated with a fresh downstream Lake project pinned to this commit: it fetched the Mathlib cache, built, and #checked entrypoints from the first accepted submission to this week's.

What the corpus holds now

• A connected core around Markov numbers, the Stern–Brocot and Calkin–Wilf trees, Farey sequences and Ford circles, nine modules deep at its longest import chain.
• One open conjecture, stated formally: the Markov uniqueness conjecture (Frobenius, 1913), reduced to the canonical Stern–Brocot branch, with groundwork toward the known prime-power case.
• One resolved: the coprimality hypothesis in the compositum discriminant formula is load-bearing, witnessed by the eighth cyclotomic field. Open only in the protocol's sense (the example is classical); what landed is a formal computation of two rings of integers.
• The theorem catalogue lists every public theorem with its statement, receiver report and import graph.

What changed in admission since v0.1.1

Every module is still admitted mechanically by the receiver. What it checks grew with what went wrong in practice (threat model):

• Kernel re-check of every submitted module with leanchecker.
• No build- or import-time code (initialize, run_cmd, extern, custom syntax and the like).
• Add-only submissions: extending an accepted module means importing it, never editing it.
• Conjectures as a first-class kind: quota-limited, probed in both directions, resolved by a later theorem.
• No deprecated Mathlib names, and diagnostics that say what to change (BRANCH_BEHIND, statement-size limits that name the statement).
• Automatic Mathlib upgrades, re-auditing the whole corpus against each new release.

Data

The evidence is published beside the code: the pre-registered accumulation series, weekly rejection aggregates, and a citable dataset snapshot, corpus-v1 (96 submissions, 29 September).

0.x: module and declaration names may still change between minor versions.