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.

Corpus v1 (29 September 2026)

The LeanFrontier corpus as of 29 September 2026: 96 accepted submissions (12 August to 28 September 2026), 96 modules, 74 internal import edges, on Lean and Mathlib v4.34.1.

Asset: leanfrontier-corpus-v1.jsonl.gz, one JSON record per accepted submission. Each record holds the claim as submitted, the accepting commit and date, the modules it added and their internal imports, and the receiver's observation (axiom closures, statement digests, the constants each statement mentions, probe outcomes). Schema: docs/dataset.md, record version 1.

SHA-256: 4986dfaf21aba5343ead6c3d01f16f8a91a08e6dda41d87ccd9472a8406cb447

Verify by regenerating it from the tag (needs a full clone, not a shallow one):

git clone https://github.com/carlok/LeanFrontier && cd LeanFrontier && git checkout corpus-v1
python3 tools/export_dataset.py --output corpus.jsonl.gz && shasum -a 256 corpus.jsonl.gz

Alongside it, at the same commit:

• experiments/accumulation.csv: the pre-registered accumulation series, including statement-level reuse;
• experiments/rejections.csv: weekly receiver verdicts by diagnostic code;
• PREREGISTRATION.md and docs/threat-model.md.

This is a data release. The library's software release remains v0.1.1.

LeanFrontier v0.1.1

First tested public release after LeanFrontier's first accepted submission.

• Includes the generalized-circle reflection module and its two public theorems.
• Preserves versioned receiver observations and a generated theorem catalogue.
• Fixes the umbrella module so downstream projects can import LeanFrontier directly.

Validated with a fresh downstream Lake project pinned to this tag.