engineering/lumbda
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lumbda/proof/lean/EmlProof
History
Exact
russell@unturf.com b5e24e98b1 Add formal Lean 4 proof of EML universality (no sorry) 
Lean's type checker verifies all 5 theorems:
  1. exp(x) = eml(x, 1)
  2. e      = eml(1, 1)
  3. ln(x)  = eml(1, eml(eml(1,x), 1))
  4. 0      = eml(1, eml(eml(1,1), 1))
  5. a - b  = eml(ln(a), exp(b))

Zero sorry. Machine-verified. This is a proof, not numerical analysis.
2026-04-13 20:23:30 -04:00
..
Basic.lean Add formal Lean 4 proof of EML universality (no sorry) 2026-04-13 20:23:30 -04:00