ArchytasZX

Develop quantum algorithms without fixing the size or dimensionality of the machine. Write a circuit once, for n qudits of dimension d, and get its states, measurement statistics and proofs of its identities as closed forms that hold for every n and every d at once.

ArchytasZX is a symbolic engine built on the qufinite ZX-calculus, with integration into Dirac notation. Qudit count and dimension are symbols, so nothing is ever enumerated, sampled or simulated: every result comes from exact rewriting and has the same shape for every size.

Example: Deutsch–Jozsa for every n

examples/deutsch_jozsa.azx, a balanced oracle on an n-qubit register, with n never given a value:

var n
gate U_f = |x>|y> -> |x>|y xor bit(x, 0)>
|psi> = |0>^@n @ |1>
(H^@n @ H)|psi>
U_f|psi>
(H^@n @ I)|psi>
var z = floor(measure|psi>/2)

$ archytaszx --unicode examples/deutsch_jozsa.azx
|ψ⟩ = |0⟩^⊗n ⊗ |1⟩
|ψ⟩ = 2^(-n/2 - 1/2) Σ_{y=0}^{1} Σ_{x=0}^{2^n - 1} (-1)^y |x⟩ ⊗ |y⟩
|ψ⟩ = 2^(-n/2 - 1/2) Σ_{y=0}^{1} Σ_{x=0}^{2^n - 1} (-1)^y |x⟩ ⊗ |(y ⊕ bit(x, 0))⟩
|ψ⟩ = 2^(-n - 1/2) Σ_{y=0}^{1} Σ_{x=0}^{2^n - 1} Σ_{x'=0}^{2^n - 1} (-1)^(y + x·x') |x'⟩ ⊗ |(y ⊕ bit(x, 0))⟩
z = [(1, 1)]
|ψ⟩⟨ψ| = 1/2 Σ_{k1=0}^{1} |1⟩⟨1| ⊗ |k1⟩⟨k1|

The measurement is a Born distribution derived symbolically: outcome 1 with probability 1, so the oracle is balanced, for every register size. The post-measurement state is the mixed state on the last line. The same states can be drawn as ZX diagrams (--zx), where the register is a bang box of multiplicity n - 1 rather than n copies:

The constant-oracle case over qudits, examples/deutsch_jozsa_proof.azx, proves that F†^⊗n F^⊗n |0⟩^⊗n = |0⟩^⊗n for every n and every d and writes the proof out as a Lean 4 file.

What it does

• Symbolic size. Qudit count, dimension and multiplicities stay symbols. |0>^@30 is one leg under a bang box, not thirty, and a concrete value is substituted into the closed form at the end at no cost in its size.
• Exact arithmetic. Scalars are tracked exactly (roots of unity, character sums, Gauss sums); no global factor is ever dropped, so results are equalities, not proportionalities.
• Proofs for all n. Diagram rewriting, a normal-form procedure, equality saturation and proof search decide equalities; induction over bang-box multiplicities proves whole families.
• Independent checking. Every proof emits a replayable certificate, is re-checked by a small proof kernel, and can be exported to Lean 4 and Mathlib, where it is checked again from scratch.
• A language for algorithms. Dirac notation with gates, sums, measurement, control flow and f-strings, run as scripts or interactively, and embeddable in Python and Jupyter.

Install

Python ≥ 3.11. numpy and sympy are the only runtime dependencies. With matplotlib installed, output is typeset and ZX diagrams are drawn as images in terminals that show them; without it, both fall back to Unicode text.

pip install archytaszx           # or 'archytaszx[viz]' to add matplotlib
archytaszx                       # interactive shell
archytaszx script.azx            # run a script

Quickstart

The .azx language

var n
gate F = |x>_d -> 1/sqrt(d) sum(y in 0..d){ e^(2*pi*i*x*y/d) |y>_d }
|psi> = H^@n |0>^@n
var z = measure|psi>
show(z, |psi>)
print(f"z = {z}")

Output styles are --render (default, typeset images), --unicode, --ascii and --latex; several style flags print every output in each style, and --order groups the output by style at the end. --zx, --both and --raw switch between Dirac notation and ZX diagrams, and --images DIR saves every rendered image as a PNG. In the shell, commands starting with : drive the engine directly (:help lists them).

examples/learn_azx.azx is a guided tour of the whole language, ending in Deutsch–Jozsa for every n; the complete reference is docs/LANGUAGE.txt.

From Python

from archytaszx import azx               # a shared Program; archytaszx.Program() for a fresh one

azx("var n")
azx.psi = azx.H ** azx.n | azx.ket(0) ** azx.n      # |psi> = H^@n |0>^@n
azx["|phi>"] = azx["|psi> - 2 |0><0|psi>"]
azx.phi       # |φ⟩ = 2^(-n/2) Σ_{x=0}^{2^n - 1} |x⟩ - 2^(1 - n/2) |0⟩^⊗n
azx.phi.latex()                          # also rendered by Jupyter

y = azx.measure | azx.psi
y             # [(k, 2^(-n)) : k ∈ {0,…,2^n - 1}]

examples/learn_azx.py is the same tour from Python.

The diagram engine

Build two Z spiders over a symbolic dimension d, fuse them, check the rewrite, and prove it for every count at once.

from archytaszx.algebra.dimension import Dim
from archytaszx.diagram.generators import Z_SPIDER
from archytaszx.diagram.graph import Diagram, Direction, PortRef
from archytaszx.rewrite.match import find_matches
from archytaszx.rewrite.engine import apply
from archytaszx.rewrite.rules_library import SPIDER_FUSION

d = Dim.symbol("d")

g = Diagram()
a = g.add_node(Z_SPIDER, input_dims=[], output_dims=[d, d])
b = g.add_node(Z_SPIDER, input_dims=[d], output_dims=[d, d])
g.add_wire(PortRef(a, Direction.OUTPUT, 0), PortRef(b, Direction.INPUT, 0))
g.set_boundary_outputs([
    PortRef(a, Direction.OUTPUT, 1),
    PortRef(b, Direction.OUTPUT, 0),
    PortRef(b, Direction.OUTPUT, 1),
])

result = apply(g, SPIDER_FUSION, find_matches(g)[0])

len(result.diagram.nodes)             # 1         -- two spiders became one
len(result.diagram.boundary_outputs)  # 3         -- the boundary is unchanged
result.diagram.scalar                 # Scalar(1) -- exact, never discarded

A certificate records the derivation; verify replays it step by step, and tampering with any recorded field (scalar, rule, consumed wire, side condition, multiplicity) fails the replay.

from archytaszx.semantics.check import compare
from archytaszx.semantics.certificate import certify, verify

compare(g, result.diagram, {"d": 5}).matched   # True -- numeric oracle at d = 5

certificate = certify(g, [result], label="fuse A into B")
verify(certificate, {"d": 3}).verified         # True

Wrap the graph in a bang box of multiplicity m and prove the fusion for every m, with d still symbolic:

from archytaszx.diagram.bangbox import abstract_subgraph_count
from archytaszx.semantics.induction import prove_by_induction

boxed, box_id, mult = abstract_subgraph_count(g, frozenset({a, b}), 1, stem="m")
fused = apply(boxed, SPIDER_FUSION, find_matches(boxed)[0]).diagram

proof = prove_by_induction(boxed, fused, witness={"d": 2})

proof.proved          # True
proof.verdict         # Verdict.PROVED_UNIFORM -- for all m, not a finite schema check
proof.index           # 'm'
proof.discharge       # StepDischarge.UNIFORM_REWRITE -- the tier that settled the step
proof.held_symbolic   # frozenset({'d'}) -- what stayed universally quantified

Concrete numbers typed by the user are abstracted back into symbols, with the values kept for output; prefix a numeral with literal to keep it concrete:

from archytaszx.repl.parser import parse_dirac_source

p = parse_dirac_source("sum_{k=0}^{3-1} |k>^{30}; copy")
dict(p.parameters)   # {'d': 3, 'n': 29}

Documentation

The full reference documentation is in docs/:

Formal proofs in Lean

Proofs found by the engine are exported to Lean 4 (:certificate lean proof.lean) against a Mathlib library bundled in archytaszx/lean, in which a diagram is a tensor network over ℂ and every rewrite rule is a lemma proved once. Families over multiplicities become Lean inductions, equalities the rewriter cannot reach are closed by a verified normaliser of symbolic sums, and verdicts that two diagrams differ export a Lean refutation. #print axioms lists only Lean's standard axioms; any step without a lemma is a named unproved_* axiom, and the REPL reports how many there are.

cd archytaszx/lean && lake exe cache get && lake build      # once
lake env lean /path/to/proof.lean

docs/LEAN.txt has the semantics, the trust boundary, the normaliser and the refutation method.

Architecture

Four engine layers, depending strictly downward, with the language on top:

Sub-package __init__.py files are empty; archytaszx itself exports only Program, Value and azx, so engine objects are imported by full module path. Each module raises only its own <Area>Error hierarchy: <Area>GrammarError for a wrong call and <Area>DomainError for a case not implemented yet.

Status

A research prototype under active development: the API is unstable and changes between releases. Equality checking is sound but not complete, so decide and prove can answer "unknown". Known limits:

• Symbolic contraction slows sharply as the number of phased spiders grows.
• Symbolic contraction refuses a bang box wired to a node outside it, and a port box over two W nodes.
• The dimension unifier reports DEFERRED where an equation has several solution branches (d1*d2 == 6, d**n == d**m); deferred dimensions are recorded as assumptions and appear in certificates and Lean theorems as hypotheses.
• A rule restricted to prime d refuses to fire at a symbolic d.
• compare_symbolic has three outcomes (equal, unequal, indeterminate); read .reason when it does not match.
• Steps the Lean export cannot prove yet are listed in LEAN_GAPS.txt.

Development

git clone https://github.com/Arhip-Dmitriev/ArchytasZX.git
cd ArchytasZX
python -m venv .venv && source .venv/bin/activate
pip install -e '.[dev]'

python -m pytest -n 8     # default tier
python -m pytest -m slow  # fuzz sweeps and oracle differentials
ruff format . && ruff check . && mypy archytaszx

The default tier is 10,072 tests and the slow tier 3,898 (counted 2026-10-22). ruff format is authoritative for layout; mypy runs in strict mode.

Citation

If you use ArchytasZX in academic work, please cite it via CITATION.cff, or:

@software{dmitriev_archytaszx,
  author  = {Dmitriev, Arkhip Alekseyevich},
  title   = {ArchytasZX: Size- and Dimension-Agnostic Engine for Quantum Algorithm Development Based on {ZX}-Calculus},
  year    = {2026},
  url     = {https://github.com/Arhip-Dmitriev/ArchytasZX},
  license = {Apache-2.0}
}

Contributing

Bug reports, counterexamples and questions about the mathematics are the most useful contributions; a soundness bug (a rewrite that changes the denoted map, scalar included) is the most valuable report of all. See CONTRIBUTING.md.

References

ArchytasZX builds chiefly on the qufinite ZX-calculus of Wang (arXiv:2104.06429), the ZXW completeness results of Poór, Wang et al. (arXiv:2302.12135, arXiv:2309.13014), and bang boxes and scalable notation (arXiv:2204.11702). Full BibTeX is in REFERENCES.bib.

License

Apache License 2.0 — see LICENSE.