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 Model