Reproducibility
Verification and provenance
The library and its independent statement compile with Lean 4.35.0-rc3. Their axiom reports contain only propext, Classical.choice, and Quot.sound. The two deliberate Challenge placeholders are not part of the proof.
October 23, 2026 (Lean v4.35.0-rc3, module system): fresh library build passed (9519 jobs); axiom audit passed with only propext, Classical.choice and Quot.sound; lake comparator check of the independent statement of Theorems A and B passed, with con-ron, NanoDa and Lean kernel replay.
Build the project
lake exe cache get
lake build
python3 scripts/audit_axioms.py
python3 scripts/generate_challenge.py --check
lake build Challenge SolutionA fresh build of the library takes about twenty minutes on a desktop machine and needs about 9 GB of memory. Build Challenge Solution before independent comparison with scripts/verify-comparator.sh.
Source and attribution
The development is maintained by Haruhisa Enomoto. The provenance record describes AI contributions, source revisions and licences. The vendored Auslander–Reiten foundations retain their attribution and Apache-2.0 licence.