Fanal

Quantum programs, formally verified.

Try PlaygroundGitHub

Fanal is a Lean 4 library for foundational formalization and verification of quantum programs. Write Dirac notation. Prove correctness.

Textbook
(va†⋅Aa⋅va)⊗(wb†⋅Bb⋅wb)(v^\dagger_a \cdot A_a \cdot v_a) \otimes (w^\dagger_b \cdot B_b \cdot w_b)
=  (v† ⁣⋅ ⁣A ⁣⋅ ⁣v)⊗(w† ⁣⋅ ⁣B ⁣⋅ ⁣w)= \; (v^\dagger \!\cdot\! A \!\cdot\! v) \otimes (w^\dagger \!\cdot\! B \!\cdot\! w)

Tensor of expectation values — labelled Dirac notation

Fanal / Lean 4
theorem dh_tensor_expectation_values :
  `[wtldirac ctx_expect |
    (⟦ v† ⟧_(( ), a) ·ₗ (
      ⟦ A ⟧_(a, a) ·ₗ ⟦ v ⟧_(a, ( ))))
    ⊗ₗ (⟦ w† ⟧_(( ), b) ·ₗ (
      ⟦ B ⟧_(b, b) ·ₗ ⟦ w ⟧_(b, ( )))) ]
  ≈ₗ `[wtldirac ctx_expect |
    ⟦ v† · A · v ⟧_(( ), ( ))
    ⊗ₗ ⟦ w† · B · w ⟧_(( ), ( )) ]
:= by ldirac_eq
Verified by Lean

Why Fanal?

𝛴

Expressive

Write quantum programs with Dirac notation — bras, kets, tensor products, and operator sums — directly in Lean 4 syntax.

✓

Verified

Every identity is machine-checked. The dirac_eq tactic automates equational reasoning over the Hilbert-space algebra.

⚙

AI-Friendly

Galleon, the auto-formalization pipeline, continuously harvests textbook results and encodes them as verified Lean theorems.

Featured Examples

Textbook quantum-information results, encoded and verified in Fanal.

Labelled Dirac

Tensor Expectation Values

Tensor product of independent expectation values on separate quantum registers, verified with a single tactic.

Gate Verification

Pauli X Gate

X|0⟩ = |1⟩ — the fundamental bit-flip gate identity, proven by automated equational reasoning.

Circuit Equivalence

CNOT Controlled Sum

CNOT gate decomposition into controlled sum form, verified as a two-qubit circuit identity.

207materials archived
190examples encoded
102verified