russell@unturf.com
b3ab4bb19a
Benchmark: Python 0.04s, uncommonlisp 59s, Lean 1.5s — for the same claim. The formal proof is 40x faster than brute-force search with mathematical certainty instead of floating-point tolerance. This is MOAD-0001 at the proof layer: O(N²) search friction where O(1) algebraic reasoning suffices. Proof assistants are the hash set to numerical analysis's nested loop. |
||
|---|---|---|
| .. | ||
| lean | ||
| benchmark.sh | ||
| benchmark_results.md | ||
| eml_proof.lsp | ||
| eml_proof.py | ||