Reproducibility
Verification and provenance
The production theorem and its independent vocabulary compile with Lean 4.33.1. Their axiom reports contain only propext, Classical.choice, and Quot.sound. The deliberate Challenge placeholder is excluded from production proof counts.
The full proof passed library builds, checks of 7 public and 4,090 supporting declarations, and independent NanoDa and Lean-kernel replay. The permitted axioms are propext, Classical.choice and Quot.sound. The proof sources match the September 20–21 verification records. The searchable API covers 1,183 modules.
Build the project
lake exe cache get
python3 scripts/build_lean_serial.py --package . --output .build-audit \
--max-rss-kib 12582912 MagnitudeConjecture.MainResults \
MagnitudeConjecture.PublicAxiomAudit
python3 scripts/generate_challenge.py --checkThe serial helper keeps a per-module log and memory measurement. For the complete library, use targets MagnitudeConjecture MagnitudeConjecture.AxiomAudit. Build Challenge Solution before independent comparison.
Source and attribution
The development is maintained by Haruhisa Enomoto. The provenance record describes AI contributions, source revisions and licences. Adapted categorical foundations retain their attribution and Apache-2.0 licence.