studio/proxy
2
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
mainline
proxy/lean4/lean-toolchain

1 line
28 B
Plaintext
Raw Permalink Normal View History

feat(lean4): add formal verification specs for ensemble models Lean 4 formalization of the decision tree + MLP ensemble architecture. Axiomatizes Float properties (sigmoid bounds, ReLU nonnegativity) since Lean's Float ops are extern-backed. Proves MLP output is bounded in (0,1) and ensemble output is always a valid decision. No mathlib dependency. Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>
2026-03-10 23:38:21 +00:00
leanprover/lean4:v4.29.0-rc4
Reference in New Issue Copy Permalink