Quantum theory

The Lean Pool projects whose card's first MSC2020 code is in class 81, Quantum theory: 8 articles, one per card.

TheoremThe BKAR forest interpolation formula#

Proves the Brydges–Kennedy–Abdesselam–Rivasseau forest interpolation formula for smooth functions on a finite complete graph’s edge-coupling space, with unordered forest-cube contributions, ordered sector variants, and choice independence.

Quoted from the card LeanPool/projects/bkarforestformula.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanBKAR.bkar_formula_forestIndex_cube_contributions

TheoremExact adaptive single-copy stabilizer learning#

Exact recovery of pure qubit stabilizer states from adaptive single-copy measurements, with explicit confidence, copy and elementary gate upper bounds.

Quoted from the card LeanPool/projects/single-copy-stabilizer-learning.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.SingleCopyStabilizer.ExactLearningTheorem.exact_learning

TheoremLean-QuantumAlg#

Provides a Mathlib-based library of formally verified quantum-algorithm definitions, primitives, and endpoints, including QFT, QSP, quantum kernels, amplitude amplification, Grover search, phase estimation, order finding, teleportation, and a Lie-algebraic barren-plateau witness.

Quoted from the card LeanPool/projects/lean-quantumalg.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanQuantumAlg.GroverSearch.main_success_probability

TheoremLow-weight Pauli dynamics and truncation error#

Derives a normalized Pauli 2-norm truncation-error bound for concrete circuits of disjoint-support Hermitian Pauli rotations, with explicit locality, angle, step-count, and cutoff hypotheses. Develops a faithful matrix representation, Pauli coefficient reconstruction, finite Schur bounds, and reusable scalar multi-jump ladder estimates. Also proves a combinatorial light-cone bound and exact counterexamples showing why repeated product-formula layers must count toward the layer exponent. This is the norm-level analysis, not a formalization of expectation-value accuracy, Hamiltonian approximation, or the paper's full algorithm.

Quoted from the card LeanPool/projects/low-weight-pauli-dynamics.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Lean4LPD.PauliString.pauliNorm_layerStep_error_le_model_of_source_regime (theorem; a main declaration), declared in LeanPool/LowWeightPauliDynamics/Pauli/LayerError.lean, line 591: “For an observable supported on Pauli weights at most ko, a block of Γ positive-many disjoint-support layers of Hermitian rotations of weight at most kh, kh ≥ 2, and |sin θ| ≤ a ≤ αt/r with α > 0 and t ≥ 0, truncation to weight ko + m(kh - 1) after each of r blocks has Pauli 2-norm error at most (2Γ(kh - 1)αt)^(m+1) (e(m+1))^(ko/(kh-1)) times the input norm. The conditions include m ≥ 1, r ≥ 5, m ≤ r, rΓ ≥ 8(m+1)^2, and r ≥ 8e^2(ko+kh-1)αt. Γ counts every layer of the actual block, including repeated product-formula layers.” Its source, as the card gives it: “Upstream STATEMENTS.md and Pauli/LayerError.lean at the pinned commit; norm-level counterpart of the revised supplement's truncation bound.”
  • Lean4LPD.l2_opNorm_le_schur (theorem), declared in LeanPool/LowWeightPauliDynamics/SchurCore.lean, line 113: “A finite rectangular matrix over any RCLike field, with absolute row sums bounded by nonnegative R and absolute column sums bounded by nonnegative C, has Euclidean operator norm at most sqrt(RC).” Its source, as the card gives it: “Upstream Schur.lean, finite-dimensional Schur test.”
  • Lean4LPD.PauliString.reachable_weight_le (theorem), declared in LeanPool/LowWeightPauliDynamics/Pauli/LayerWitness.lean, line 411: “Every Pauli string reachable through a list of disjoint-support kh-local layers, kh ≥ 1, has weight at most its initial weight times kh raised to the number of layers. Reachability is combinatorial; this theorem does not assert that a reachable coefficient is nonzero.” Its source, as the card gives it: “Upstream Pauli/LayerWitness.lean, effective-layer light cone.”
  • Lean4LPD.LayerCounterexample.actual_discard_exceeds_gamma_bound (theorem), declared in LeanPool/LowWeightPauliDynamics/Pauli/LayerCounterexample.lean, line 592: “For the explicit eight-qubit second-order word L1,L2,L2,L1 and angles 0 < θ < π/2, truncating the evolved weight-one input at weight one discards a nonzero coefficient of weight greater than four. Thus the two distinct layer types give an invalid bound 1*2^2; repetitions must be counted.” Its source, as the card gives it: “Upstream Pauli/LayerCounterexample.lean, exact symbolic witness.”
Project
Sources
LeanLean4LPD.PauliString.pauliNorm_layerStep_error_le_model_of_source_regime

TheoremOsterwalder-Schrader Axioms for the Gaussian Free Field#

Formalizes Osterwalder-Schrader axioms for the massive Gaussian free field using Minlos, covariance, and reflection-positivity infrastructure.

Quoted from the card LeanPool/projects/osforgff.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim.
  • Project repository: mrdouglasny/OSforGFF.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
  • License: Apache-2.0.
  • MSC2020: 81T08, 60G15, 46G12.
  • In Lean Pool: LeanPool/OSforGFF, from the card LeanPool/projects/osforgff.yaml.
Sources
LeanOSforGFF.gaussianFreeField_satisfies_all_OS_axioms

TheoremQuantum code certificates and hypergraph-product theory#

Formalizes general binary row reduction, kernel bases and rank certificates; quantum-code distance bounds from witnesses and exhaustive low-weight enumeration; arbitrary-matrix hypergraph-product dimension and X/Z cleaning bounds; and CSS orthogonality of lifted products over finite groups. Includes a Pauli expression translation modulo global phase, a Boolean encoding with proved soundness and model extension, and sound checking of RUP additions in LRAT certificates, bridged to matrix-level distance bounds. Concrete code-family datasets, large certificate replays and measurement protocols are outside this import.

Quoted from the card LeanPool/projects/qec-certificates.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 9 main results, each with its informal statement quoted from the card. The scan finds 9 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • QECCertificates.hgp_kunneth (theorem; a main declaration), declared in LeanPool/QECCertificates/GF2/HGPKunneth.lean, line 277: “For arbitrary finite binary matrices A and B, the number of columns of their hypergraph product minus its X and Z ranks equals nullity(A) times nullity(B) plus nullity(transpose A) times nullity(transpose B), expressed with natural-number rank differences.” Its source, as the card gives it: “Upstream GF2/HGPKunneth.lean; the Tillich–Zémor hypergraph-product construction.”
  • QECCertificates.hgp_X_distance_ge (theorem), declared in LeanPool/QECCertificates/GF2/HGPCleaning.lean, line 574: “If a binary vector is killed by the hypergraph-product X check and is outside the Z row space, its Hamming weight is at least the minimum of supplied lower bounds for nonzero vectors in the kernels of the first input and the transpose of the second input.”
  • QECCertificates.hgp_Z_distance_ge (theorem), declared in LeanPool/QECCertificates/GF2/HGPCleaningDual.lean, line 62: “Dually, a vector killed by the Z check and outside the X row space has weight at least the minimum of supplied lower bounds for the kernels of the transpose of the first input and the second input.”
  • QECCertificates.lp_orthogonal (theorem), declared in LeanPool/QECCertificates/GF2/LiftedProduct.lean, line 258: “For arbitrary matrices of binary-valued functions on a finite group, the left/right regular expansion gives lifted-product X and Z checks whose every pair of rows has zero binary dot product.”
  • QECCertificates.Matrix.rank_eq_length_rowReduce (theorem), declared in LeanPool/QECCertificates/GF2/RankCertificate.lean, line 224: “The rank of a finite binary matrix equals the length of the verified row-reduction output for its list of rows.”
  • QECCertificates.eq_minWeight_of_decide (theorem), declared in LeanPool/QECCertificates/GF2/LowerBound.lean, line 219: “For two binary matrices, if d is at most the number of columns, exhaustive enumeration finds no vector of weight below d in the first kernel outside the second row space, and a supplied vector has those membership properties and weight d, then the minimum such weight is d. The empty-set distance convention is the number of columns plus one.”
  • QECCertificates.LRAT.unsat_of_checkSteps (theorem), declared in LeanPool/QECCertificates/Reflect/LRAT.lean, line 406: “Acceptance by the RUP certificate checker implies unsatisfiability of the original CNF. No correctness assumption on an external SAT solver is needed; the clause-database interface carries proved soundness laws.”
  • QECCertificates.LRAT.buildPair_complete (theorem), declared in LeanPool/QECCertificates/Reflect/Complete.lean, line 1057: “For a positive number n of input bits and nonempty row supports within that range, a Boolean assignment satisfying the parity constraints, odd bilinear pairing and weight bound extends to a model of buildPair while agreeing on all 2n input variables. The complementary soundness theorem extracts those constraints from every model.” Its source, as the card gives it: “Upstream Reflect/Encode.lean and Reflect/Complete.lean. The import retains general theorems, not the paper's concrete instance results. First public paper announcement: 2026-10-02 12:31:45 UTC, arXiv v1. The upstream paper discloses AI-generated Lean proofs reviewed and validated by the author. RowspaceKernel is derived from QCL-SUAT/Lean-QEC at a0855f8a6374c1dda2097bbf07f33ba53760fdcd (Apache-2.0), credited to Mattias Ehatamm, Yi Lee, Xiaodi Wu and Runzhou Tao, and their paper End-to-End Formalization of Quantum Error Correction, arXiv:2605.16523.”
  • QECCertificates.LRAT.le_minWeight_of_unsat (theorem), declared in LeanPool/QECCertificates/Reflect/Distance.lean, line 322: “For a positive number n of columns and k + 1 ≤ n, an unsatisfiable Boolean encoding gives a matrix-level distance lower bound of k + 1. Support-row correspondence, nonemptiness, index bounds and duplicate-free hypotheses are explicit. This composes with kernel-checked RUP replay.” Its source, as the card gives it: “General bridge from upstream Reflect/Certified.lean; the minimum-weight distance wrapper is added during the Lean Pool port.”
Project
Sources
LeanQECCertificates.hgp_kunneth

TheoremQuantum parallel repetition#

Proves a quantitative parallel-repetition theorem for finite two-player quantum games: whenever the entangled value is below one, the entangled values of parallel repetitions decay exponentially, with an explicit universal exponent in the game gap and answer-alphabet sizes.

Quoted from the card LeanPool/projects/quantum-parallel-repetition.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanQuantumParallelRepetition.distributionUniformExponential

TheoremStability of matter and the kinetic Lieb–Thirring inequality#

Formalizes stability of non-relativistic fermionic Coulomb matter in three dimensions, the kinetic Lieb–Thirring inequality with Rumin's explicit coefficient, Baxter's electrostatic inequality with its positive nuclear correction, and real quadratic-form stability with Coulomb finiteness. Preserves the Fourier, Pauli-occupation, Hardy and Voronoi infrastructure in the 184-module dependency closure of these results. The separate ionization, thermodynamic-limit and Thomas–Fermi developments are outside the imported scope.

Quoted from the card LeanPool/projects/stability-of-matter.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLiebThirring.stability_of_matter

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.