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.