Loading papers...
Formally verified projects and research papers
Machine-checked formal verification artifacts
Each project is a complete Lean 4 formalization with machine-checked proofs. The theorems compile, the invariants hold, and the code executes exactly as specified. No hand-waving—every claim is witnessed by a type-checked term.
Machine-verified formalization of semantic closure theory. Mechanizes how self-reference and meaning emergence arise through fixed points of closure operators.
Proof-carrying Koopman autoencoder with nucleus-constrained latent space and Lean-certified ReLU/threshold operators.
Proof-driven computational visualizations
These are not decorative renders. Each visualization is a proof-of-concept demonstrating how Lean 4 theorems compile to executable code for computational modeling. The animations are parameterized by machine-checked invariants—what you see is the proof running.
Auto-playing visualization driven by Lean nuclei proofs.
CE1 vs CE2 hypergraphs with Lean causal certificates.
Nucleus-constrained autoencoder.
Topos-theoretic gluing of branches.
Research papers and whitepapers
