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
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is cryptographically anchored with IPFS CIDs.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerDifferential Linear Logic: Differentiation of Proofs
Contributor
Thomas Ehrhard
Université Paris Cité
Core insight that proofs can be differentiated. In linear logic, the exponential modality (!) creates an analogue of the Taylor expansion, and the codereliction rule extracts the linear approximation — the derivative — of a proof. This connects proof theory to analysis via a denotational semantics in vector spaces.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerDiLL Semantics and Differential λ-Calculus
Contributor
Laurent Regnier
Université d’Aix-Marseille
Complete framework: differential λ-calculus with sums (formal linear combinations), differential application, and the chain rule. Resource-sensitive semantics where differentiation tracks how a proof uses its resources linearly vs. non-linearly. Foundation for quantitative semantics of proofs.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization — DiLL for SKY Combinators
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization applying DiLL semantics to SKY combinators. Key results: chainRule (exact chain rule for dual-number derivatives), app_single_single (basis application), codereliction_is_derivative (codereliction = derivative of exponential), nucleusLinear_idempotent (linear extension preserves nucleus idempotence), stepEdges soundness and completeness. Executable gradient descent synthesis loop.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerDual-Differentiable Verified Kernel
Contributor
Apoth3osis Labs
R&D Division
All theorems kernel-checked by Lean 4. Guard-no-sorry passes. Standard axioms only.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerStandalone Repository + Proof Maps
Contributor
Apoth3osis Labs
R&D Division
Published as standalone GitHub repository with interactive 2D/3D proof maps, executable gradient descent synthesis loop, and integration with the HeytingLean DifferentiableATP engine.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026