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.
Causal Confluence in Wolfram Physics • Lean 4 + Mathlib • Apoth3osis Labs
Are determinism and relativity the same thing?
In the Wolfram Physics Project, the universe is modeled as a network of relationships evolving according to simple rules. Two properties seemed fundamental:
Like computing 2+3 vs 3+2—different orders give the same answer. No matter which path you take through the computation, you end up at the same result.
Like Einstein's relativity—different observers see the same causal structure. The "what caused what" is the same regardless of your reference frame.
The assumption was that these are equivalent. If a system always gives the same answer (confluence), surely all observers must agree on causation (causal invariance)?
Max Piskunov's 2020 discovery: They're independent. You can have one without the other.
The Wolfram Physics Project
Stephen Wolfram proposes that space itself is a hypergraph—a network of abstract relationships that evolves according to simple rewriting rules. What we experience as physics emerges from the structure of this evolving network.
"The balance between branching and merging that we call causal invariance turns out to be at the core of why relativity works, why there's a meaningful objective reality in quantum mechanics, and a host of other core features of fundamental physics."
— Stephen Wolfram
Click to expand
Piskunov's Counterexamples
In 2020, Max Piskunov constructed explicit systems that disprove the assumed equivalence. These aren't edge cases—they demonstrate a fundamental independence between computational determinism and relativistic causality.
This system always reaches the same final state no matter what order you apply the rules. But different observers see different causal histories—they disagree about what caused what.
All observers agree on the causal structure—they see the same "light cones" and can agree on what caused what. But the system can end up in different final states.
Machine-Verified Independence
Piskunov's examples were presented in Wolfram Language. But how do we know they're correct? Graph isomorphism checking is notoriously subtle—bugs can hide in edge cases.
We formalized the counterexamples in Lean 4. The proof assistant mechanically verifies every step: the hypergraph rewriting, the causal graph construction, the isomorphism checks (or lack thereof).
This isn't just verification—it's a new way to do physics. The Lean proofs export structured data that drives our visualization. What you see on the models page is the actual mathematical content, rendered in 3D.
Why This Matters for Physics
A system can be fully deterministic—always reaching the same result—while observers disagree about what happened. Computation and observation are distinct.
Relativistic agreement on causation doesn't require computational determinism. Observers can agree on "what caused what" even when the outcome varies.
If the universe is computational, causal invariance and confluence are separate constraints that a "theory of everything" must satisfy independently.
Multiway graph showing how different evaluation orders create branching paths. The structure of this graph determines whether confluence and causal invariance hold.
See the Counterexamples in Action
Our visual model shows CE1 and CE2 side by side, with their graph structures rendered from the Lean proof data. Watch how CE1's paths converge (confluence) while its causal cones diverge, and how CE2's cones align while its paths don't.
View Live ModelThe proof uses only standard Lean 4 axioms—no custom postulates required:
Our Lean 4 formalization mechanizes Piskunov's counterexamples and Wolfram's hypergraph rewriting framework, providing machine-verified proofs of the independence result.
Maksim (Max) Piskunov
Physics PhD · Set Rewriting Systems
Northeastern University · Wolfram Physics Project
Researcher in discrete models of spacetime and network substitution systems. Author of SetReplace, a C++/Wolfram Language package for exploring set and graph rewriting systems (242+ stars). Demonstrated that confluence and causal invariance are independent properties, disproving a key assumption in the Wolfram Physics Project.
Stephen Wolfram
Founder & CEO, Wolfram Research
Wolfram Research · Wolfram Physics Project
Creator of Mathematica, Wolfram|Alpha, and the Wolfram Language. Author of A New Kind of Science (2002). Originator of the Wolfram Physics Project, which models the universe as an evolving hypergraph governed by simple rewriting rules, from which space, time, and quantum mechanics emerge.
“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.