A certificate
A single file holding your circuit, what was claimed about it, the evidence, and the exact software environment used. Anyone can re-check it later without trusting you — or us.
The Institute for Applied Ontological Mathematics
Quantum circuits that come with proof
Design a circuit, or bring your own. Get back a certificate you can check, a machine-verified proof of what it does, and code that runs on IBM, Google and AWS hardware.
What this is for
Quantum hardware is metered, queued, and noisy. Every run costs, and when a run comes back wrong you are left with one expensive question.
Was my mathematics wrong, or was the hardware just noisy?
Those are different failures with different fixes, and today they arrive tangled together. This system separates them before you spend anything. If the circuit is proved to do what you intended, a bad result on hardware is physics — decoherence, gate error, readout — and never your algebra. You find the mathematical mistakes where they cost nothing: at the desk, not on the device.
What you get, every time
One circuit in. Three things out — each one stands on its own.
A machine-checked proof
Not a test that passed. A proof the Lean theorem prover verified, shipped as readable source, with the logical assumptions it leans on listed in the open.
Code that runs
The same circuit as OpenQASM 3, Qiskit, Cirq and Braket — each bundled with the certificate it came from, so the program and its proof never drift apart.
How it works
- 1
Design or import
Place gates in the browser, or load a circuit, a certificate, or a Lean proof you already have.
- 2
Watch it exactly
Every gate you place is evaluated exactly, and all ten views update at once — including a state readout on each wire.
- 3
Certify
The circuit is bundled, its claims are proved, and the proof is replayed in the Lean kernel.
- 4
Export
Take the certificate, the proof source, and runnable code for the platform you use.
Why this is different
Most quantum tools simulate in floating point and ask you to trust the result. Four things here work differently.
Exact arithmetic, not approximation
Amplitudes are exact algebraic numbers. Where other tools show 0.7071067811865476, this shows (ω − ω³)/2 — the actual value, not a rounding of it. No floating point appears anywhere a pass or fail decision depends on it.
Checked by simulators we did not write
A system that only agrees with itself proves nothing. Every circuit was re-run on independent simulators — Qiskit Aer and Stim — inside a sandbox with no network, and without being handed our predicted answer. They agreed. That is the difference between a claim and a check.
The same circuit always gets the same name
Circuits are addressed by their content. Build one in the browser or author it in Lean — identical circuits produce an identical address. That is what makes a result reproducible rather than merely repeatable.
It tells you what it cannot do
Views that do not apply to your circuit stay visibly empty instead of showing plausible filler. Unsupported features say so. A tool that hides its limits is not one you can build on.
Ten ways to see one circuit
A circuit is one object with many faces. In the designer you work from whichever face suits the problem, and watch all of them update as you place each gate.
Circuit diagram
The familiar picture: wires and gates, left to right.
Bloch sphere
Where each qubit points, and how each gate turns it.
Exact matrix
The precise transformation, as algebraic numbers rather than decimals.
Measurement outcomes
Which results are possible and their exact probabilities.
Pauli correlations
Which qubits are linked, and how.
Stabilizer tableau
The compact algebraic form used for error-correction circuits.
Gate word
The circuit written as a word — edit the word, edit the circuit.
Proof structure
How each verified claim depends on the others.
Hardware layout
How the circuit maps onto real device qubits.
Topological invariants
Shape-based properties that survive deformation.
The evidence behind that
Claims are cheap, so here are the numbers, checked against simulators we did not write.
12
circuits certified
each re-checkable by anyone
108
theorems proved
machine-checked, not tested
0
rounding errors
no result depends on a float
21 / 21
independent agreements
Qiskit Aer 12/12 · Stim 9/9
Stim covers 9 of the 12 circuits because it is a stabilizer simulator — a T gate lies outside its model, which is a property of Stim, not a gap in the corpus. The independent runs were executed with no network and without being given our certified answer, so they could not simply echo it back.
Where this comes from
The Institute for Applied Ontological Mathematics is the public research arm of Apoth3osis. Apoth3osis is an applied R&D lab. IAOM publishes its work into the open scholarly commons, where it can be read, checked, and built on by anyone.
What you have been using
A working specimen of what we do. Under the Curry–Howard / BHK correspondence a proof is a program and a program is a proof — so a theorem about what your mathematics does can be turned into software that does exactly that, carrying the theorem with it for anyone to re-check. Here we have turned that method on Clifford+T quantum circuits and shown it end to end: design, exact evaluation, a kernel-checked proof, a content-addressed certificate, and runnable code for four platforms. Quantum is the demonstration, not the limit.
What we build with partners
The correspondence underneath is domain-agnostic. We take the mathematics that governs a hard problem and make it into verifiable software — exact semantics, a kernel-checked proof, and an artifact anyone can re-check without trusting whoever produced it. After the proof of concept we partner with a small number of researchers and operators on scopes they define: built to the invariants that matter to your work, bound into the systems you already run, and hardened for daily operations. You bring the domain; we make its correctness a theorem.
Tell us where being wrong is expensive. If your correctness currently rests on tests and trust, there is a stronger floor available — and a direct conversation is how it starts. An API and MCP server are launching shortly; partner scopes are open now.
IAOM@apoth3osis.io →