Status: in build
This page describes a system under active construction. Nothing below is a shipped result unless it says so explicitly. I'm publishing the architecture anyway, because the discipline of the design is the point, and because I'd rather be held to a public spec than a private ambition.
The idea
Can a fleet of agents take raw physical data — spring displacements, orbital periods — rediscover the law underneath it, and then prove that law, formally, in a theorem prover? Not "the model is confident." Not "the fit looks great." A machine-checked proof that compiles in Lean 4 with exit code 0.
That's the QG-Synthesis Engine. The name points at quantum gravity, and I should be straight about what that means: quantum gravity is the north star, not the deliverable. The system is gated so it must re-derive known, established physics before it's allowed anywhere near an open problem. If it never gets past Kepler, it will still have been worth building. If it does get past Kepler, everything it produces beyond that is labelled speculative until a kernel says otherwise.
The epistemic boundary
The design principle everything hangs on: a hard, compiler-enforced line between speculative and established.
Every generated hypothesis, every intermediate representation, every plausible-looking equation is speculative by default. An artifact crosses the line only when it survives the formalization bridge and compiles in a Lean 4 kernel restricted to a whitelist of structurally sound axioms. The sorry placeholder — Lean's escape hatch for "trust me" — is rejected outright, as is any unsafe declaration. An agent that tries to sneak a proof through with sorry doesn't get a warning. It gets logged as a capability failure.
LLMs are persuasive. That's precisely why the boundary can't live in a prompt. It lives in the compiler, which has never once been impressed by confident prose.
Architecture
The workflow is governed by a triad: a large-context architect model that plans and audits but has no terminal access at all, a sandboxed local executor that runs code but is blocked from the network and from the architect's memory, and me — the only node with authority to approve destructive actions. Handoffs between the machine nodes are schema-validated JSON, and destructive proposals suspend the whole graph until I approve them.
The pipeline itself: empirical data goes into PySR, a Julia-backed symbolic regression engine that evolves candidate equations along a Pareto front of accuracy versus simplicity. Winning candidates cross the SITA bridge — structure-to-instance autoformalization — which maps a raw algebraic expression into typed Lean 4 definitions, conditions, and theorem instances. The result is compiled by a strict verification kernel that replays the environment from scratch, so no agent can pre-poison it.
Every state transition is hashed against its parent, so the full derivation chain — hypothesis, test, result — is tamper-evident. Flip one byte in step 42 and steps 43 through 100 flag themselves as compromised. If this system ever finds something new, the receipt for how will matter as much as the result.
The roadmap, honestly
- —Phase 0 — the harmonic sandbox. Ingest spring-displacement data, recover Hooke's law (F = −kx), and autoformalize it in Lean 4 without compilation errors. This is where the project stands now.
- —Phase 1 — Kepler. Re-derive T² ∝ a³ from raw orbital data, with a compiled proof as the exit criterion.
- —Phase 2 — geometry. Extend to the tensor machinery needed for general relativity: evaluating Calabi-Yau metrics and formally proving properties of them within tolerance.
- —Phase N — the speculative frontier. Only reachable if every prior gate closed with exit code 0.
Each phase has a falsifiable done-condition. No phase is declared complete because it feels close.
This is the same conviction that runs through my shipped work: a system's claims are worth exactly what its verification layer can enforce. Symbiote and RepoMend enforce it with pyright, test suites, and diff bounds. This project raises the bar to a proof kernel — which is why it gets to be called "in build" until the kernel agrees.