Code and proofs¶
| repository | what is in it |
|---|---|
| inventor1975/ZTL | the logic, the judge (ztljudge.py), the Lean 4 proofs (lean/), the regression stands and the scripts that recompute the numbers |
| inventor1975/ztlstudio | the studio |
| inventor1975/ztl-engineer | ZTL Engineer |
To check the proofs yourself, from a clone of the ZTL repository:
cd lean && lake build
Lean 4 v4.29.1, core library only. The hand-placed checks print each theorem's axioms, and the answer is an empty list
— no propext, no Quot.sound, no Classical.choice; the repository's CI audits every theorem on every push. The
proofs are about the definitions in Lean, not about the Python program, which is tested against them. To recompute
the numbers on the ZTL pages:
python3 publications/core-logic/paper_numbers.py
The preprint, which states the results and names the Lean theorem behind each, pinned to a commit: ZTL — Zero-Trust Logic, v2.1.6 (Zenodo, not peer-reviewed).