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 <https://www.linkedin.com/feed/update/urn:li:activity:7472291667711295488/>`_

In three days, Fable 5 — `Anthropic <https://www.anthropic.com>`_'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
<https://ai4value.fi>`_. 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 :doc:`QSVT4CRA
<2026-06-09-junction-quantumhack-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 <https://ai4value.fi>`_
under the same umbrella as `sklar-engine <https://github.com/PlayerPlanet>`_,
`EASE Health <https://ease-health.org>`_, and the QSVT4CRA pipeline.
We're hiring — drop me a line if the work resonates.

Links
-----

- Original post: https://www.linkedin.com/feed/update/urn:li:activity:7472291667711295488/
- Tooling: Lean 4 (`leanprover/lean4`); Fable 5 (Anthropic, discontinued)
- Project home: https://ease-health.org (umbrella) · https://github.com/PlayerPlanet
- Hiring: konsta.kiirikki@aalto.fi · konsta.kiirikki@gmail.com
- Related notes:
  :doc:`QSVT4CRA (Junction X OP Pohjola) <2026-06-09-junction-quantumhack-qsvt4cra>` ·
  :doc:`Joint-probability distributions seminar <2026-03-19-joint-probability>` ·
  :doc:`SBI seminar <2026-03-16-sbi-seminar>`