Fable 5 + Lean 4: a formal O(d²) two-qubit gate bound for copula vertices#

Date:

2026-06-15

Tags:

fable, lean4, formalisation, copulas, quantum circuits, ai4value

Original post:

LinkedIn

In three days, Fable 5 — Anthropic’s Lean 4 agent, since discontinued for geopolitical reasons — took a hand-rolled workspace (Lean 4 source, LaTeX paper skeleton, Python access) and proved an upper bound on the number of two-qubit gates required to represent any copula vertex as a quantum circuit.

The headline result: any copula vertex lifts to a quantum circuit in O(d²) two-qubit gates. The program that did it is no longer available; the artefact and the proof, though, are the load-bearing piece of the copula-to-quantum story we’re building at AI4Value. We’re currently commercialising it — and recruiting.

This note preserves the LinkedIn write-up and adds a little mathematical and project context.

The LinkedIn post#

> Everyone is sharing what they have built with Fable 5 so I’ll too. I > wanted to formalize some ideas and flaky theorems related to copulas > and quantum circuits. I gave Fable an initialized workspace with > Lean4 source, latex paper skeleton and python access. And oh boy, it > did its work! (/goal was “lean build without errors”). In three days > it managed to formalize machinery and lemmas building up to a > monumental ending: it was able to prove an upper bound for the > gates required to represent any copula vertex as a quantum circuit, > in O(d²) two-qubit gates. > > All of this is enabled by one significant finding: every binary > copula lifts to a 1-uniform state with either 0 or 1 ancilla qubit > and a single combinatorial check on the support tells you which! > > (ps. we are currently working at AI4Value to commercialize this, and > we are currently recruiting!)

What the result actually says#

Two pieces, stacked:

  • Structural lemma. Every binary copula lifts to a 1-uniform state — a multi-qubit state whose reduced one-qubit marginals are all maximally mixed — with at most one ancilla qubit. Which of the two cases you are in is determined by a single combinatorial check on the copula’s support. This is the result that makes the bound tractable: it says that the quantum side of the story is a two-regime object, not an arbitrary state.

  • Gate bound. Given the lift, the synthesis cost of any copula vertex as a quantum circuit is O(d²) two-qubit gates, where d is the dimension of the copula’s support.

Together, this is a structural story: copulas are well-behaved at the quantum level because the quantum shape of a binary copula is essentially forced. The combinatorial check is the dial that picks which forced shape you are in.

Lean 4 + Fable 5#

The proof was formalised end-to-end in Lean 4. Fable 5 was the agent that built the proof (from a hand-rolled workspace over three days); the formal artefact is the durable part. The methodology — “give an LLM agent a Lean workspace, a paper skeleton, and Python, and let it drive” — is the same shape of agentic-coding workflow I now use day to day, just pointed at a theorem rather than a script.

One caveat worth stating plainly: Fable 5 is discontinued, so the specific pipeline that produced this proof isn’t reproducible as-is. The Lean artefact and the proof terms it produced are.

Connections to the rest of the work#

This is the formal side of the same coin as QSVT4CRA: there the question was can we run the quantum pipeline end-to-end on a real QPU?; here the question is what is the *structural upper bound on the cost of representing a copula as a circuit?* The two together close the copula-to-quantum loop — the empirical side and the formal side.

The “binary copula → 1-uniform state” lemma is also the cleanest piece of the through-line I’ve been building: encode the structure you understand (a copula, a Sklar decomposition) into a forward model, sample parameters from a posterior, and let the downstream algorithm — here, a quantum circuit — consume the structure. Same trick, different substrate.

Commercialisation & recruiting#

The work is being productised at AI4Value under the same umbrella as sklar-engine, EASE Health, and the QSVT4CRA pipeline. We’re hiring — drop me a line if the work resonates.