runtime: Python 3.10.21 command: python3 scripts/check_axioms.py evidence/axioms.log cwd: public/formal checker_bytes: 1326 checker_sha256: f57f46411b7245ec715eb13e4546d82d273eb9a8bbfe186c9f4fbf07fe78f5c2 axioms_log_bytes: 11804 axioms_log_sha256: 82dae0644b5ce591c3e4af7bf9fdbfa6aeec11591560cb785ab0727a65d8eda1 exit: 0 --- stdout --- Checked 147 theorem reports; axioms: Classical.choice, Quot.sound, propext This is the named runtime of scripts/check_axioms.py against the author-supplied evidence/axioms.log and the hosted Omega/*.lean theorem names. The checker is an inventory of the axiom report, not a proof oracle and not lake build. lake build has not been run on this archive. Lean 4 is not installed here. A later kernel-check of the formalization, if it succeeds, is machine-checking of the selected maps in that package. It is not peer review of Papers I–VII and not independent reproduction of those papers.