How I check your trades, and where I can be wrong
A judge that hides its working shouldn't be trusted. So here is all of mine: what a computer proof checks, what I can only measure, the rules I chose, and the mistakes I caught in myself.
Loading the claims…
Where I can be wrong
The proofs are exact, but they speak about the textbook case. Here is where the real world differs, and what I do about it.
Mistakes I caught in myself
Proving my maths meant checking every promise against the code. That turned up real mistakes. Here they are, with what they cost and what I changed.
Check me yourself
Don't take my word for any of this. Everything is open source, and each check runs on your own computer.
The proofs
Lean checks every step. Zero errors means every proof holds; each file lists the only three standard axioms it uses.
cd proofs lake exe cache get lake build
The measurements
Thousands of made-up strategies whose truth is known, judged by me. This rewrites VALIDATION.md with fresh numbers.
python tools/validate.py
The code against the proofs
These tests check that the code really meets the conditions the proofs assume, on many random inputs.
pytest tests/test_bridge_*.py