Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2610.03214

Quantum error-correcting code parameters, checkable by a certificate of provable size

Shuoming An, Fusheng Yang

quant-phSubmitted Oct 2, 2026• Announced Oct 5, 2026• 0 citations• Revised Oct 5, 2026 (v2)
v1 · Oct 2, 2026v2 · Oct 5, 2026
arXivHTMLPDF

Abstract

Quantum error correction protects quantum information by encoding it in a code described by three numbers: how many physical qubits it uses, how many logical qubits it protects, and the smallest error it cannot detect. The last is an optimum over exponentially many candidates, so it is read off a solver rather than checked. Here we show that code parameters can be certified by a short certificate, a list or a pairing or a symbolic instance, whose correctness the kernel of a proof assistant decides by computation, and whose size is itself a theorem rather than an estimate. Two published code families have distances settled here: the bivariate bicycle code's $[[144,12,12]]$, certified, and the affine-permutation codes printed at $[[1152,580,\le 12]]$ and $[[2304,1156,\le 14]]$, settled at twelve and fourteen. Eleven code families and thirty-nine parameter sets follow, with nothing beyond three standard axioms trusted and the pipeline's specification step preset to twenty columns.

Related papers

End-to-End Formalization of Quantum Error Correction

Mattias Ehatamm, Yi Lee, Xiaodi Wu +1 more

Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.

quant-pharXiv:2605.16523•May 19, 2026•0 citations

Certificates That Touch: Exact Quantum Code Distance from One Witness and One Scan

The Institute for Applied Ontological Mathematics

Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all — only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix — it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement — no logical operator lives below weight w — discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie — the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 × 3 toric code — and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations

Bayesian Optimization for Quantum Error-Correcting Code Discovery

Yihua Chengyu, Richard Meister, Conor Carty +2 more

Quantum error-correcting codes protect fragile quantum information by encoding it redundantly, but identifying codes that perform well in practice with minimal overhead remains difficult due to the combinatorial search space and the high cost of logical error rate evaluation. We propose a Bayesian optimization framework to discover quantum error-correcting codes that improves data efficiency and scalability with respect to previous machine learning approaches to this task. Our main contribution is a multi-view chain-complex neural embedding that allows us to predict the logical error rate of quantum LDPC codes without performing expensive simulations. Using bivariate bicycle codes and code capacity noise as a testbed, our algorithm discovers a high-rate code [[144,36]] that achieves competitive per-qubit error rate compared to the gross code, as well as a low-error code [[144,16]] that outperforms the gross code in terms of error rate per qubit. These results highlight the ability of our pipeline to automatically discover codes balancing rate and noise suppression, while the generality of the framework enables application across diverse code families, decoders, and noise models.

quant-pharXiv:2601.18562•Jan 27, 2026•0 citations

Lower overhead fault-tolerant building blocks for noisy quantum computers

Prithviraj Prabhu

Quantum computation holds the promise of solving certain complex problems exponentially faster than classical computers. However, the high prevalent noise in current quantum devices impedes the accurate execution of even basic algorithms. This can be remedied by protecting quantum information with a quantum error-correcting code, where the logical information of an algorithmic qubit is spread across multiple physical qubits. Individual quantum errors are then located and corrected by the fault-tolerant measurement of multi-qubit stabilizer operators (parity checks). Unfortunately, error correction and fault tolerance both impose large demands on the qubit overhead: hundreds to thousands of physical qubits per logical qubit. We reduce the spacetime cost of fault tolerance by redesigning key building blocks of an error-corrected quantum computer. First, we develop a combinatorial proof with flag fault tolerance that exponentially reduces the extra qubits needed to measure a stabilizer of any size, while tolerating one fault. We leverage these proofs to then design state preparation circuits for the Steane and Golay codes with 100% yield. Next, we improve error correction on a planar layout by showing that a distance-four code encoding six logical qubits protects information as well as the distance-five surface code, using one-tenth as many physical qubits. Finally, we optimize the time overhead of logical gates in surface code quantum computers by protecting measurement results with a classical code, cutting computation time by a factor of two to six. Our hardware-agnostic optimizations of fault tolerance overheads thus suggest new routes to advance the timeline of error-free quantum computing.

quant-pharXiv:2605.12385•May 13, 2026•0 citations

No Such Code: Certified Invariants for Quantum Codes, Circuits, and Measurement

The Institute for Applied Ontological Mathematics

Four questions sit at the base of fault-tolerant quantum computing: whether a code with given parameters can exist, whether two circuits denote the same operation, how much entropy a measurement irreversibly produces, and whether a compiled gate still means what it should. They are normally answered by four disjoint techniques. We show they are one technique. In each case the answer is an invariant—the object a governing transformation leaves fixed—and that invariant can be held as a certificate a proof kernel checks and an operator-native substrate computes. The instruments are the quantum weight enumerator, whose shadow variant yields what is, to our knowledge, the first machine-checked nonexistence certificate for a quantum error-correcting code (no pure [[4, 1, 3]] stabilizer code, reduced to an integer impossibility); the spider normal form, unique both as a linear map and as a content-addressed tree, at the minimal axiomatic footprint of a proof assistant; the measurement boundary defect, whose logical entropy equals a kernel-counted cohomology dimension; and the reduction receipt, round-tripping a certified gate word to bare metal on two independent substrates. Everything downstream of the explicitly labelled modeling step in each domain is exact integer or rational arithmetic. The common shape—find the invariant the transformation fixes, and read it off as a certificate—turns four hard quantum questions into arithmetic a machine can hold. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations

A Certificate Is a Canonical Form

The Institute for Applied Ontological Mathematics

A computational claim you cannot recompute is hearsay. We ask what a certified answer must be so that anyone can recompute it and refuse anything that does not match, and we answer that it must be a canonical form: a representative stable under the ways the answer can be re-expressed. We build three and show each survives a different transport. An optimum survives change of algorithm: one integer reached by exhaustive search below a size wall, by exact tropical variable elimination past that wall (bounded by a graph's width, not by its number of variables), and by the published literature. A quantum code's number of logical qubits survives change of proof: it is the block length minus two matrix ranks certified by a proof kernel, and its distance is either enumerated exactly or witnessed by an exhibited logical operator proven genuine by a rank increase. A certified answer survives change of language: its content hash agrees byte-for-byte across two independent implementations and refuses any value, such as a floating-point number, with no language-independent form. The consequence is operational: a reader re-derives the answer and serves it only if it matches. We place a live 2024 quantum-error-correction result on the classical side of this discipline, certifying the code parameters its own published matrices imply without disputing the demonstration. The through-line is old and exact: truth is invariant under change of notation, and a certificate is that invariant made computable. Published by The Institute for Applied Ontological Mathematics.

•Oct 11, 2026•0 citations
Quantum error correction protects quantum information by encoding it in a code described by three numbers: how many physical qubits it uses, how many logical qubits it protects, and the smallest error it cannot detect. The last is an optimum over exponentially many candidates, so it is read off a solver rather than checked. Here we show that code parameters can be certified by a short certificate, a list or a pairing or a symbolic instance, whose correctness the kernel of a proof assistant decides by computation, and whose size is itself a theorem rather than an estimate. Two published code families have distances settled here: the bivariate bicycle code's [[144,12,12]][[144,12,12]][[144,12,12]], certified, and the affine-permutation codes printed at [[1152,580,≤12]][[1152,580,\le 12]][[1152,580,≤12]] and [[2304,1156,≤14]][[2304,1156,\le 14]][[2304,1156,≤14]], settled at twelve and fourteen. Eleven code families and thirty-nine parameter sets follow, with nothing beyond three standard axioms trusted and the pipeline's specification step preset to twenty columns.
Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from nnn to k⌈log⁡2n⌉k\lceil \log_2 n\rceilk⌈log2​n⌉. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.
Computing the distance of a stabilizer code is NP-hard, yet certifying the distance of a given code needs no search at all — only two one-sided certificates that meet. An upper bound is a single explicit logical operator: one vector, checked in milliseconds against the actual check matrix — it commutes with every stabilizer, it is provably outside their span, and it acts on exactly w qubits. A lower bound is a universal statement — no logical operator lives below weight w — discharged by a finite scan whose completeness is itself a theorem, not a convention: a reconstruction lemma proves that every light Pauli vector appears in the scanned list, so the scan quantifies over the whole space rather than over a table someone chose. When the two certificates touch, the distance is exact, and the receipt can be replayed by a referee who trusts neither the authors nor their software. We build this bracket calculus over the binary symplectic carrier, close it exactly on the classical menagerie — the five-qubit perfect code, Steane, Shor, the distance-three rotated surface code, and the 3 × 3 toric code — and report an instructive refutation: our own frozen reference data claimed distance at least 2 for a punctured code fragment, and the certificate layer produced an explicit weight-one logical operator. Puncturing buys a logical qubit and leaves it bare; the count and the distance are independent shadows of the same subgroup lattice. The same prover-proposes/kernel-disposes architecture certifies logical counts at bivariate-bicycle scale (k = 12 at n = 144) from change-of-basis rank certificates checked in linear time, and every number in the system wears a two-valued trust badge whose semantics is an event, not a citation: no kernel run on your instance, no badge. The results are proved in a machine-checked formal kernel. Published by The Institute for Applied Ontological Mathematics.
Quantum error-correcting codes protect fragile quantum information by encoding it redundantly, but identifying codes that perform well in practice with minimal overhead remains difficult due to the combinatorial search space and the high cost of logical error rate evaluation. We propose a Bayesian optimization framework to discover quantum error-correcting codes that improves data efficiency and scalability with respect to previous machine learning approaches to this task. Our main contribution is a multi-view chain-complex neural embedding that allows us to predict the logical error rate of quantum LDPC codes without performing expensive simulations. Using bivariate bicycle codes and code capacity noise as a testbed, our algorithm discovers a high-rate code [[144,36]] that achieves competitive per-qubit error rate compared to the gross code, as well as a low-error code [[144,16]] that outperforms the gross code in terms of error rate per qubit. These results highlight the ability of our pipeline to automatically discover codes balancing rate and noise suppression, while the generality of the framework enables application across diverse code families, decoders, and noise models.
Quantum computation holds the promise of solving certain complex problems exponentially faster than classical computers. However, the high prevalent noise in current quantum devices impedes the accurate execution of even basic algorithms. This can be remedied by protecting quantum information with a quantum error-correcting code, where the logical information of an algorithmic qubit is spread across multiple physical qubits. Individual quantum errors are then located and corrected by the fault-tolerant measurement of multi-qubit stabilizer operators (parity checks). Unfortunately, error correction and fault tolerance both impose large demands on the qubit overhead: hundreds to thousands of physical qubits per logical qubit. We reduce the spacetime cost of fault tolerance by redesigning key building blocks of an error-corrected quantum computer. First, we develop a combinatorial proof with flag fault tolerance that exponentially reduces the extra qubits needed to measure a stabilizer of any size, while tolerating one fault. We leverage these proofs to then design state preparation circuits for the Steane and Golay codes with 100% yield. Next, we improve error correction on a planar layout by showing that a distance-four code encoding six logical qubits protects information as well as the distance-five surface code, using one-tenth as many physical qubits. Finally, we optimize the time overhead of logical gates in surface code quantum computers by protecting measurement results with a classical code, cutting computation time by a factor of two to six. Our hardware-agnostic optimizations of fault tolerance overheads thus suggest new routes to advance the timeline of error-free quantum computing.
Four questions sit at the base of fault-tolerant quantum computing: whether a code with given parameters can exist, whether two circuits denote the same operation, how much entropy a measurement irreversibly produces, and whether a compiled gate still means what it should. They are normally answered by four disjoint techniques. We show they are one technique. In each case the answer is an invariant—the object a governing transformation leaves fixed—and that invariant can be held as a certificate a proof kernel checks and an operator-native substrate computes. The instruments are the quantum weight enumerator, whose shadow variant yields what is, to our knowledge, the first machine-checked nonexistence certificate for a quantum error-correcting code (no pure [[4, 1, 3]] stabilizer code, reduced to an integer impossibility); the spider normal form, unique both as a linear map and as a content-addressed tree, at the minimal axiomatic footprint of a proof assistant; the measurement boundary defect, whose logical entropy equals a kernel-counted cohomology dimension; and the reduction receipt, round-tripping a certified gate word to bare metal on two independent substrates. Everything downstream of the explicitly labelled modeling step in each domain is exact integer or rational arithmetic. The common shape—find the invariant the transformation fixes, and read it off as a certificate—turns four hard quantum questions into arithmetic a machine can hold. Published by The Institute for Applied Ontological Mathematics.
A computational claim you cannot recompute is hearsay. We ask what a certified answer must be so that anyone can recompute it and refuse anything that does not match, and we answer that it must be a canonical form: a representative stable under the ways the answer can be re-expressed. We build three and show each survives a different transport. An optimum survives change of algorithm: one integer reached by exhaustive search below a size wall, by exact tropical variable elimination past that wall (bounded by a graph's width, not by its number of variables), and by the published literature. A quantum code's number of logical qubits survives change of proof: it is the block length minus two matrix ranks certified by a proof kernel, and its distance is either enumerated exactly or witnessed by an exhibited logical operator proven genuine by a rank increase. A certified answer survives change of language: its content hash agrees byte-for-byte across two independent implementations and refuses any value, such as a floating-point number, with no language-independent form. The consequence is operational: a reader re-derives the answer and serves it only if it matches. We place a live 2024 quantum-error-correction result on the classical side of this discipline, certifying the code parameters its own published matrices imply without disputing the demonstration. The through-line is old and exact: truth is invariant under change of notation, and a certificate is that invariant made computable. Published by The Institute for Applied Ontological Mathematics.