The launch

Anyone can claim they solved the measurement problem. Almost no one lets you check.

Physics foundations has a credibility problem, and it’s not hard to see why. The field is a magnet for grand, untestable claims: someone announces they’ve dissolved the measurement problem, or derived gravity, and there’s no practical way for a reader to check — so the sensible default is to ignore it. I’ve spent the last stretch building a foundations program, QIQT-H, that tries to earn attention the only way I think a solo, unaffiliated researcher can: by making it checkable.

Don’t trust me — run the proofs

The entire deductive substrate is formalized in Lean 4 / Mathlib, and the repository ships a verification capsule. On your own machine, with minimal trust in me, it wipes the compiled proofs, rebuilds them from source so the Lean kernel re-checks every step, replays an independent kernel checker, and audits that the complete transitive dependency set is only Lean’s three standard axioms — no sorry, no hidden axiom.

git clone https://github.com/kaplan196883/QIQT-H && cd QIQT-H
cat verify/verify.sh          # read it first — it's short
bash verify/verify.sh         # → verify/out/claim_card.md

(Don’t want to run a stranger’s shell script? A pinned Docker recipe rebuilds the whole stack — Lean, Mathlib, the project — from source in a container; see verify/README.md. Toolchain leanprover/lean4:v4.30.0; the clean-room build takes a while — that’s the point.)

Out comes a claim card: the exact formal theorem, the complete trusted base, and a ledger of every physical assumption still assumed rather than proven. All the mechanical trust in the project collapses to three things — the Lean kernel, your reading of the rendered statement, and the explicitly-listed physical inputs. Nothing else about me matters.

There’s a Physical Review Letters paper for the flagship result

You don’t have to take the gravity claim on faith from a stranger, either. In 2026 Dorau & Much published “From Quantum Relative Entropy to the Semiclassical Einstein Equations” in Physical Review Letters (arXiv:2510.24491) — a clean argument that Einstein’s equations follow from the relative entropy of a quantum field across a horizon (a quantum-information upgrade of Jacobson’s 1995 derivation). It’s a paper: “arguments indicating.”

I formalized that exact chain in Lean, for the free field. Their derivation maps step for step onto machine-checked theorems here — modular flow = geometric boost (Fock.OneParticleBW), relative entropy = horizon energy flux (ModularEnergyBound), area variation via Raychaudhuri (DifferentialAreaLaw), and the Einstein equations by stress-energy conservation (the claim card) — and it even re-derives the 1/4 they assume.

Two honesties, stated up front. Their paper came first — public October 2025, PRL 2026, before my GR chain was formalized — so I claim no priority. And on the load-bearing input: the PRL bare-assumes the entropy–area relation S = δA/4. QIQT-H does more — it proves S = A/4G as a theorem for its own induced area (one weight family carries both capacity and geometry; the separate area label is deleted), reducing the physical input to a single calibration, machine-checked, with a guard proving that calibration is load-bearing (without it the count is unbounded at fixed area). But that one calibration is still carried, not derived from nothing — so their Letter vindicates the shared derivation chain (relative entropy → modular theory → Jacobson → Einstein), not QIQT-H’s finiteness reading. What I add is that a computer checks every line, and you can re-run it. In one sentence: a top-journal result exists for this — I formalized its free-field chain in Lean, and reduced its one entropy–area assumption to a single, guarded calibration.

What’s new here, and what isn’t — stated plainly, because conflating them is what lets a skeptic dismiss the work:

This is a formalization contribution on top of a published physics result — not a physics priority claim, and not a proof that gravity is emergent. See the full PRL equation → Lean theorem mapping for the step-by-step correspondence.

The idea, in one breath

Quantum physics lets a system be in many possible states at once, yet every measurement shows just one. The textbook patch — “collapse” — is bolted on by hand, outside the unitary law. QIQT-H drops the patch. The wave function (Φ) is the whole of reality and never collapses; a single extra, non-dynamical fact — λ — just marks which of the many decohered records is the one we actually experience. No collapse, no parallel universes, no built-in dice. Because any bounded region of space can hold only a finite amount of entropy (a holographic bound from black-hole physics), the same picture also grows a conditional, Lean-checked version of Einstein’s gravity for the free field.

The honest part

Here’s what I am not claiming, stated as loudly as the rest: I have not proved the universe works this way, and I have not solved quantum gravity. The gravity chain is conditional on named inputs; the value of Newton’s constant is a labelled frontier; whether the Lean definitions faithfully model the physics is an adequacy judgment I leave to you (which is why the claim card renders the precise statement). Two adversarial red-team reviews landed the verdict I now stand behind: this is a single-world interpretation, plus a holographic entropy bound, plus a conditional induced-gravity chain — machine-verified where it can be, with the residue named. Not a theory of everything. A program you can audit.

What actually got built

Along the way the formalization produced results that, to my knowledge, existed in no proof assistant before (pointers and corrections welcome): a complete Tomita–Takesaki modular theory for an inductive-limit state, an unbounded Stone theorem and spectral machinery beyond current Mathlib, and the von Neumann double-commutant theorem — plus the headline physics chain, the semiclassical Einstein equations from a finite-entropy bound, conditional and free-field, end to end. Over 5,000 theorems across ~515 files, with no project-specific axioms and no sorry — the final theorems depend only on Lean’s three standard classical axioms.

The ask

I’d genuinely value scrutiny — especially the one thing the capsule can’t mechanize: does the Lean statement mean what the prose says? Read a claim card, poke at the open problems, or just run verify.sh and tell me what breaks. If you find something formalized earlier, or a hole in an argument, I want to know.

— Pawel Kaplanski