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.
