Rex Rowan

Open-source infrastructure for the Qiskit ecosystem

I am a Qiskit Advocate. I build open-source quantum computing tools, mostly for the Qiskit ecosystem. My background is in mathematics — number theory, graph theory, and formal proof in Lean 4 — which shows up directly in how I approach circuit construction and verification: as things to prove correct, not just get working.

What I’ve built

Sixteen projects. Fifteen are Qiskit Ecosystem members, and one has a qiskit-ibm-runtime discussion drafted but not yet filed. Each links to its repo, its docs, and — where it makes sense — a live demo.

Project Category Problem it solves Status Why it matters
Qiberis Interoperability Qiskit, Cirq, and PennyLane circuits don’t share a common IR — cross-framework work means hand-porting circuits. Ecosystem Member Bit-ordering convention enforced by a regression test, not just asserted in a docstring.
Qiskit SQD Dashboard Diagnostics SQD’s configuration-recovery loop runs blind — no visibility into convergence until it finishes. Ecosystem Member Hooks directly into qiskit-addon-sqd’s live callback loop, validated against real N₂ SQD runs.
Qiskit StateViz Visualization Prior statevector visualization tools have bit-rotted against current Qiskit. Ecosystem Member Built fresh against current Qiskit, interactive and Plotly-based rather than a static plot.
Qiskit QKD Lab Protocol simulation BB84 teaching demos usually fake the eavesdropper instead of simulating one. Ecosystem Member Eve is real circuit structure — mid-circuit measurement, reset, conditional re-prep — not a shortcut.
Qiskit Graph Walks Algorithms Quantum walks are usually taught as physics demos, not shipped as usable algorithmic primitives. Ecosystem Member Spatial search and graph-isomorphism fingerprinting as reusable, tested primitives.
Qiskit LEAN Bridge Formal verification Qiskit’s gate-equivalence library is trusted by convention, not proven. Ecosystem Member 130 equivalences bridged to Lean 4 lemma stubs; caught a genuine qubit-ordering bug in the process.
Qiskit ZX Verified Compiler · Formal verification Transpiler rewrite passes can silently produce a circuit that runs but computes the wrong thing. Ecosystem Member Zero sorrys; Lean/Python cross-check on all 16 Clifford-phase fusion cases.
Qiskit Transpile Verify Tooling No standard way to check a transpiled circuit is still equivalent to the original. Ecosystem Member Translation validation checked post-hoc, on real transpiler output — not trusted by construction.
Qiskit Qubit Mapping Toolkit Transpiler plugin Initial layout and routing are graph problems, usually solved with special-cased heuristics. Ecosystem Member Isomorphism- and walk-based heuristics, benchmarked directly against Qiskit’s own LightSABRE default.
Qiskit Cayley Codes Quantum error correction Hand-designing CSS stabilizer codes doesn’t scale or generalize. Ecosystem Member [[8,4,2]] validated against the CDZ construction’s Theorem 10; open issues documented, not hidden.
Qiskit LEAN Verify Game Formal verification · Education Formal proofs are illegible to anyone who doesn’t already read Lean. Ecosystem Member Same gate identities checked two independent ways — Lean’s kernel and Qiskit’s own Statevector.
Qiskit Certified QRNG Cryptography · Formal verification QRNG libraries produce bits and call them “quantum random” without any entropy accounting or statistical soundness check. Ecosystem Member Confidence-bound (not point-estimate) entropy certification, with a Lean proof of extractor soundness in progress — a real, tracked constant discrepancy included, not hidden.
Qiskit Spacetime Bridge Quantum error correction A Clifford circuit’s spacetime structure isn’t connected to a checkable CSS code without hand translation. Ecosystem Member Outcome/spacetime-code construction (Delfosse-Paetznick) feeding stabilizer structure straight into the Cayley Codes analysis backend.
Qiskit Magic Metrics Resource metrics PassManager-native way to measure magic or multipartite entanglement — existing options are hardware-sampled (Qurrium) or unmaintained (qLEET). Ecosystem Member GF(2) stabilizer-tableau shortcuts answer exactly, in polynomial time, what other tools sample or skip.
Qiskit Quantum Backend Selector Tooling Queue- and noise-aware backend selection and routing for IBM Quantum backends. Ecosystem Member Can route job submission with automatic ISA transpilation and failover if a backend errors out mid-attempt.

See all projects →

The thread connecting them

Most of the table above reads as unrelated tooling until you look at the sequence. Qiberis and StateViz solve the ordinary interoperability and visualization gaps every Qiskit user eventually hits. QKD Lab and SQD Dashboard go further — they model real experimental structure (an actual eavesdropper, an actual convergence loop) instead of a simplified stand-in for it. Graph Walks and Cayley Codes push into genuinely underserved territory: quantum walks as algorithmic primitives, and error-correcting codes generated from group-theoretic structure rather than designed by hand. Transpile Verify and the Qubit Mapping Toolkit take on the transpiler itself — checking its output and improving its layout/routing decisions respectively, both benchmarked rather than asserted. And the LEAN bridge, ZX-verified, and LEAN Verify Game do something almost nobody else in the ecosystem is doing — treating Qiskit’s own gate identities and rewrite rules as claims that should be proven, not just tested against expected output, and then making that proof legible to people who don’t read Lean.

Magic Metrics extends that same discipline sideways — treating a circuit’s own entanglement and magic content, not just its gate identities, as something to compute exactly rather than estimate, with the one genuinely new derivation (the Meyer-Wallach stabilizer fast path) queued for the same Lean cross-check treatment.

That progression — from “make Qiskit easier to use” toward “make Qiskit’s own foundations checkable, and make the checking itself legible” — is the actual throughline, not a plan I set out to follow but the direction each project kept pointing the next one toward. Certified QRNG extends that thread outward, from Qiskit’s own gates and passes to a cryptographic security claim built on top of Qiskit circuits — proven the same way, in the open, discrepancies and all.

Recent and ongoing

I’ve worked through the Qiskit Global Summer School curriculum — GHZ state construction and depth optimization, noise models and dynamic circuits, advanced error mitigation (ZNE, PEC, PNA, SLC, noise learning), and SQD/QAOA applications to molecular simulation and combinatorial optimization. I also work on original research in graph theory and number theory — ℓ-zero-sumfree sets, the Davenport constant, and structures related to modular arithmetic and their component topology — and I write explainer content on math and quantum topics using Manim, Observable Framework, and Quarto.

I’m also a contributor to the qLDPC Code Challenge, an open, automatically-verified leaderboard for quantum LDPC codes — my [[42,6,6]] generalized bicycle code sits on the challenge’s track frontier — and I was a prize winner (Overall category) in the UnitaryCON qLDPC Code Sprint (September 2026).

I’m also building CliffordGame, a lean4game submission where quantum circuit puzzles are graded by Lean itself rather than a bespoke checker, playable on the Lean Game Server hosted by HHU Düsseldorf. It shares level content and underlying math with the companion Qiskit-Ecosystem package, qiskit-lean-verify-game, which grades the same circuits using Qiskit’s Statevector instead.

Long-term goals

Two directions I’m scoping but haven’t started building — real enough to be worth stating publicly, honest enough to label as concept-stage rather than dress up as more than they are.

Goal What it would be Status
Quantum Certified Registry A Palomar-style registry for quantum results, with a mandatory physical-hypothesis disclosure Palomar’s pure-math model has no field for. Concept Stage
Quantum Proof Factory A Tau-Ceti-style, continuously-running proof factory for quantum information theory, built on Lean-QIT — peer agents, not a fixed pipeline. Concept Stage

Demos

Smaller, standalone, built to show something rather than ship something — no Ecosystem submission, no package, just a live page.

Demo What it shows Status
Entropy Demo A message decoheres under simulated T1 noise, side by side unprotected, corrupted, and Steane-code corrected. Demo
Unitary vs. Collapse Predicted interference visibility under pure unitary evolution (incl. many-worlds) vs. objective collapse models (GRW/CSL), using the real N² mass-scaling decoherence formula. Demo

Other projects

I have broad interests well outside quantum computing — somewhere around 800 completed certificates across edX, Coursera, FutureLearn, and other platforms, spread across far more fields than any one portfolio page could hold. Not everything I build is Qiskit-related.

Solar Shield started with a solar eclipse: watching four minutes of the Sun’s output get blocked by pure geometry raised an obvious question — what would it take to do that on purpose, and for longer? The site explores two space engineering concepts in answer: a swarm of reflective sails (or an ejected mist/fog) stationed near the Sun-Earth L1 point to reduce incoming solar insolation, and space-based solar power harvesters in the spirit of ESA’s SOLARIS program, aimed the opposite direction — capturing that same energy rather than blocking it. It sits alongside this portfolio as a second, unrelated track of work rather than inside it. Project Repository.

I’m also a participant in the NASA International Space Apps Challenge and the Global Quantum Game Jam 2026 (Sept 25–27, 2026, hosted by IGDA Finland).

Elsewhere: