Reproducibility
Verification and provenance
The library and its independent statement compile with Lean 4.33.1. Their axiom reports contain only propext, Classical.choice, and Quot.sound. The two deliberate Challenge placeholders are not part of the proof.
October 17, 2026: fresh library build passed (9254 jobs); axiom audit passed with only propext, Classical.choice and Quot.sound; Comparator replay of the independent statement of Theorems A and B passed, including 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.