corpus-v2: 110 accepted submissions

The LeanFrontier corpus as of 15 October 2026: 110 accepted submissions (12 August to 7 October 2026), 110 modules and 90 internal import edges, on Lean and Mathlib v4.35.0. corpus-v1 had 96 submissions, 96 modules and 74 edges, on v4.34.1.

Asset: leanfrontier-corpus-v2.jsonl.gz holds one JSON record per accepted submission, with the same schema as corpus-v1 (docs/dataset.md, record version 1). Each record holds:

• the claim as submitted;
• the accepting commit and date;
• the modules it added and their internal imports;
• the receiver's observation: axiom closures, statement digests, the constants each statement mentions, and probe outcomes.

SHA-256: e5c24edfe364e417c1f20215e3db3dafcfc5f30b2614656bec9dac44e820cebf

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

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

Read the triviality probes with care. Every record in this release was accepted before 7 October 2026, so every baseline_triviality_probes value comes from the receiver's old probe. That probe stated each goal without its module's namespace and context, so a namespace-relative name became a variable, and inconclusive usually means a more general claim was not closed. Re-reading all accepted entrypoints in their real context found no submission that the corrected probe would have rejected. Details are in docs/dataset.md. Records from later releases will carry not elaborated where it applies.

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 matching library release is v0.3.0.