Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Dual-Differentiable • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can proof search be turned into gradient descent? Ehrhard and Regnier’s Differential Linear Logic shows that proofs can be differentiated. This project applies DiLL semantics to SKY combinators: terms become vectors (formal linear combinations), rewrite rules extend linearly with computable Jacobians, and a gradient descent loop searches for programs satisfying I/O specifications. The chain rule is proved exact, and codereliction is shown to be the derivative of the exponential — connecting proof differentiation to classical calculus.
Original Researchers
Key Verified Results
chainRuleExact chain rule for dual-number derivatives
Derivative.lean
codereliction_is_derivativeCodereliction = derivative of exponential
Codereliction.lean
nucleusLinear_idempotentLinear extension preserves nucleus idempotence
NucleusDifferential.lean
stepEdgesList_soundEnumerated edges are valid Step relations
SKYMultiway.lean
stepEdges_completeAll Step successors are enumerated
SKYMultiway.lean