Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Semantic Closure in Lean 4 • Lean 4 + Mathlib • Apoth3osis Labs
What makes living systems different from machines?
A car engine converts fuel to motion, but it cannot repair itself. A computer executes programs, but it cannot rewrite its own circuitry. Yet every living cell continuously rebuilds its own components while simultaneously using those components to function.
This is the puzzle of semantic closure: How can a system be both the message and the reader, both the machine and the mechanic?
Robert Rosen called this the "(M,R)-system" problem: metabolism (M) produces components, repair (R) rebuilds the metabolic machinery, but critically—what repairs the repair system? The answer must involve a kind of self-reference that seems paradoxical.
"Closing the Loop" by Lopez-Diaz & Gershenson
In 2024, Amahury Lopez-Diaz and Carlos Gershenson published a breakthrough paper showing that semantic closure is not just a philosophical concept—it can be formalized mathematically and traced through evolutionary history from simple autocatalytic reactions to self-replicating life.
"Self-referentiality is not only a necessary condition for life but also essential even for the simplest autocatalytic systems."
Their key insight: the closure operator—a mathematical function that iterates until it reaches a fixed point—captures exactly how living systems stabilize their self-reference into something coherent rather than paradoxical.
Click to expand
The Innovation: Proofs That Run
Traditional scientific modeling separates theory from implementation: you write equations on paper, then translate them into code, hoping the translation is correct. Bugs hide in the gap between mathematical intent and computational reality.
We use Lean 4 differently. Instead of treating the proof assistant as just a verifier, we use it as a modeling language. The theorems themselves become executable specifications—when Lean accepts the proof, the model is guaranteed to be mathematically coherent.
This means the visualization you see on our models page is not an artist's interpretation—it's driven directly by data exported from the verified Lean proofs. The closure iterations, the nucleus transformations, the fixed-point convergence are all certified by the proof assistant before they reach your screen.
Understanding Closure: An Analogy
Imagine a factory that makes robots. One robot's job is to repair other robots. But who repairs the repair robot? Another repair robot? This leads to infinite regress.
The closure operator is like a repair robot that can fix itself. When you apply the repair function to the repair function, you get... the same repair function. It's a fixed point.
Formally: close(close(x)) = close(x). The closure operator is idempotent. This is exactly what the Lean theorem closeSelector.idem proves.
The proof dependency lattice. Each node is a verified theorem; edges show which theorems depend on which. The structure itself demonstrates the mathematical coherence of semantic closure.
What We Proved
| THEOREM | PLAIN ENGLISH | WHY IT MATTERS |
|---|---|---|
| closeSelector.idem | Applying closure twice equals applying it once | Self-repair is stable, not recursive |
| InjectiveEvalAt | Each selector maps to a unique component | No ambiguity in repair instructions |
| EvalImage.betaOnImage | The inverse selector exists on the image | Repair can always find its target |
| reluNucleus_idempotent | ReLU transformation reaches fixed point | Neural-like gates stabilize |
| thresholdNucleus_fixed_iff | Threshold triggers exactly at boundary | Decision boundaries are precise |
All core equations machine-verified
Proofs compile to embeddable code
Proof data drives WebGL scene
See the Proofs in Action
Our visual model shows the closure operator converging to a fixed point. The bars represent actual vector values from the Lean proofs; the color transitions show ReLU and threshold transformations; the particle burst marks the moment of closure.
View Live ModelThis project formalizes and extends the theoretical framework developed by these researchers. Our Lean 4 mechanization translates their mathematical insights into machine-verified proofs.
Amahury J. López-Díaz
Physicist · Complex Systems
Facultad de Ciencias, UNAM
Physicist with interests in biology and linguistics. Explores the evolutionary emergence of semantic closure—the self-referential mechanism through which symbols actively construct and interpret their own functional contexts—by integrating relational biology, biosemiotics, and ecological psychology.
Carlos Gershenson
Empire Professor of Innovation
Binghamton University (SUNY) · UNAM
Complexity scientist and president of the Complex Systems Society (2024–2027). Research spans self-organizing systems, artificial life, information, and urban systems. PhD from Vrije Universiteit Brussel under Francis Heylighen. Editor-in-Chief of Complexity Digest.
“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.