Status: in build
This page describes a system under active construction. Nothing below is a finished result unless I say so explicitly. I'm publishing the design anyway, because I'd rather be held to a public spec than a private ambition.
The idea, in one sentence
Can a group of AI agents look at raw physical data, guess the equation hiding inside it, and then prove that equation is correct — not "the model sounds confident," an actual machine-checked proof, the kind a computer will refuse to accept if there's a hole in the logic?
That's what the QG-Synthesis Engine does today: it takes numbers (spring displacements, orbital periods), proposes a formula, and hands that formula to a proof checker called Lean 4. If the checker can't verify it, the result doesn't count. No exceptions, no "close enough."
Why "QG" — the honest version
QG stands for quantum gravity: the still-unsolved problem of how gravity and quantum mechanics fit together. It's one of the biggest open questions in physics, and solving it is, by most reasonable estimates, decades away — if it happens at all in my lifetime.
So why build toward it? Because it's the kind of problem that, if it ever gets cracked, doesn't just add a footnote to a textbook — it changes what engineering is possible. A lot of what we currently file under "science fiction" (exotic propulsion, materials that shouldn't exist, the flying-car version of the future we were promised) isn't blocked by imagination. It's blocked by physics we don't understand well enough yet to build on safely. Quantum gravity sits upstream of a lot of that.
I'm not claiming this project gets anywhere near solving it — that would be exactly the kind of promise this whole site exists to avoid. The project's own founding document is precise about this, and I'm quoting it directly rather than softening it: "The generation of quantum gravity theories serves exclusively as a speculative north-star motivation and remains outside the deliverable architecture." In plain terms: quantum gravity is the reason I find this worth doing on a random Tuesday. It is explicitly not something the system is allowed to touch until it has earned that right, one boring, verifiable step at a time.
If you want to see what "earning it" actually looks like in practice, the roadmap below is the honest version — including the part where the current step still has a known gap.
The rule that governs everything else
Here's the one design decision the whole project depends on: a hard line between speculative and established, enforced by software, not by good intentions.
Every equation the system proposes starts out speculative. It only crosses into "established" when it survives a specific gauntlet: translated into formal logic, fed to the Lean 4 proof checker, and accepted by a kernel that only trusts a small, deliberately restricted set of mathematical building blocks. Lean has a built-in escape hatch called sorry — a way of saying "trust me, I didn't actually prove this part." I've configured the system to treat any attempt to use it as an outright failure, not a warning.
I did this because I don't trust myself, and I definitely don't trust an AI model under deadline pressure, to notice when a proof is fake but sounds right. Language models are good at sounding right. That's exactly the skill that makes them dangerous here. So the check that matters doesn't live in a prompt where persuasive writing can sneak past it — it lives in a compiler, which has never once been charmed by confident phrasing.
How the pieces fit together
Three things are in conversation with each other. First, a planning model that reads the data and proposes what to try next; it can think and audit, but it has no ability to actually run anything or touch a file. Second, a sandboxed executor that does the running, cut off from the network and from the planner's memory, so a mistake in one can't quietly corrupt the other. Third, me. I'm the only one who can approve anything that can't be undone. Every handoff between the two AI components is a structured, validated message, not a paragraph of prose one model has to correctly interpret from another.
The actual discovery step uses a tool called PySR, which searches for equations that fit the data well without being needlessly complicated (a spring's force is F = -kx, not a fifth-degree polynomial that happens to pass through the same points). A candidate equation that looks promising then gets translated, piece by piece, into the formal language Lean 4 understands, and the proof checker either accepts it or it doesn't exist as far as the project is concerned.
One more thing, because it matters if this system ever does find something: every step is logged and cryptographically chained to the step before it. Change one recorded result after the fact, even by a single character, and everything downstream of it visibly breaks. If this ever produces something genuinely new, I want the paper trail for how it got there to be as trustworthy as the result itself.
The roadmap, honestly
- —Phase 0 — Kepler. Fed the system raw orbital data and had it re-derive Kepler's third law (the relationship between a planet's orbital period and its distance from the sun), then compiled that as a formal Lean 4 proof, checked line by line, no shortcuts. Closed.
- —Phase 1 — building the pipeline. Wired the pieces together for real: the equation-search tool, the proof-checker connection, and an audit log that records every step with a tamper-evident cryptographic chain. Sealed.
- —Phase 2 — geometry, where the project actually is right now. This turned out to be harder than expected in a specific, boring way: Lean's standard math library doesn't have the geometric tools (the Riemann and Ricci tensors, if you know the terms) that this phase needs, so I'm building them from scratch, one small piece at a time. Four of ten planned pieces are done and verified.
- —Phase N — the actual speculative frontier. This is where quantum gravity itself would eventually live, if the project ever earns its way there. It stays explicitly locked out of the deliverable until every step before it has been checked and passed.
I want to be honest about a real gap in Phase 2 rather than paper over it, because that's the entire point of this page existing. One of the pieces I've proven is that a perfectly flat, constant metric has zero curvature, and it technically passes the proof checker. Here's the uncomfortable part, though: a broken definition, one that's simply wrong and returns zero for everything regardless of the input, would pass that exact same check. A clean compile doesn't yet prove the underlying definitions are correct. It only proves this one theorem doesn't contradict them. I know what test would catch that kind of error (a probe designed to fail if the definitions are hollow), and I haven't built it yet. That's not a footnote. It's the most important unresolved thing about where this project stands today.
This is the same conviction that runs through my shipped work: a system's claims are only as good as what its verification layer can actually enforce, not what it sounds like it's proving. Provenar and Patchward enforce that with pyright and test suites. This project raises the bar to a formal proof kernel — which is exactly why it still gets called "in build," and will keep being called that honestly, gap and all, until the kernel agrees otherwise.