Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The cyclotomic Birman-Murakami-Wenzl (BMW) algebras B_n^k, introduced by R. Häring-Oldenburg, are a generalisation of the BMW algebras associated with the cyclotomic Hecke algebras of type G(k,1,n) (aka Ariki-Koike algebras) and type B knot theory. In this paper, we prove the algebra is free and of rank k^n (2n-1)!! over ground rings with parameters satisfying so-called "admissibility conditions". These conditions are necessary in order for these results to hold and originally arise from the representation theory of B_2^k, which is analysed by the authors in a previous paper. Furthermore, we obtain a geometric realisation of B_n^k as a cyclotomic version of the Kauffman tangle algebra, in terms of affine n-tangles in the solid torus, and produce explicit bases that may be described both algebraically and diagrammatically. The admissibility conditions are the most general offered in the literature for which these results hold; they are necessary and sufficient for all results for general n.
This mission is the statement-level formalization of On the freeness of the cyclotomic BMW algebras: admissibility and an isomorphism with the cyclotomic Kauffman tangle algebras (arXiv:0911.5284v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.2 (Proposition 2.2, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
16 results of the paper are not stated yet, because the library lacks an interface they need:
The Schur basis on n d-dimensional quantum systems is a generalization of the total angular momentum basis that is useful for exploiting symmetry under permutations or collective unitary rotations. We present efficient (size poly(n,d,log(1/ε)) for accuracy ε) quantum circuits for the Schur transform, which is the change of basis between the computational and the Schur bases. These circuits are based on efficient circuits for the Clebsch-Gordan transformation. We also present an efficient circuit for a limited version of the Schur transform in which one needs only to project onto different Schur subspaces. This second circuit is based on a generalization of phase estimation to any nonabelian finite group for which there exists a fast quantum Fourier transform.
This mission is the statement-level formalization of Efficient Quantum Circuits for Schur and Clebsch-Gordan Transforms (arXiv:quant-ph/0407082v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The qubit CG step is three logical register operations (Eq.(6), Fig.1; continued on PDF p.3, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Graph neural networks and geometric learning on meshes rely on operators that combine the features of a node with those of its neighbours. The graph Laplacian is the oldest such operator: it is the discrete analogue of the Laplace–Beltrami operator of a surface, and its eigenvectors play the role of a Fourier basis on a graph. Early spectral graph networks (Bruna et al., 2013) learned filters directly in that eigenbasis. Such filters are expensive, since they need an eigendecomposition, and they do not transfer between graphs. Defferrard, Bresson and Vandergheynst (2016) replaced them with polynomial filters . These are computed with sparse matrix products, and their output at a node depends only on a bounded neighbourhood of that node.
This mission formalizes Section 4.6 of the book Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges by Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2). The section introduces the weighted Laplacian (24) and the spectral and polynomial filters built on it, and states that a polynomial filter of degree is localised in the -hop neighbourhood. The section closes with the view of meshes as operators , which leads to remeshing invariance and to the result of Wang et al. (2019a) that remeshing-invariant functions depend only on the spectrum. The book numbers no theorems, lemmas or definitions, so every item of this mission is cited by section, equation number and printed page.
There are nodes . A weight matrix assigns a weight to each ordered pair of nodes. The neighbourhood of is . Node features form a matrix whose row is the -dimensional feature vector of node .
The degree of is , and the degree matrix is . The Laplacian is
The graph is undirected when ; then is symmetric and has an orthonormal eigenbasis with and . The Fourier coefficients of are .
Given a degree and real coefficients , the polynomial filter is
Hops are measured in a simple graph on the nodes that carries the weights: with implies that and are adjacent. A node is within hops of if some walk in from to has length at most .
A permutation of the nodes acts by its permutation matrix , with and . A function of matrices is remeshing invariant if for every orthogonal . A matrix-valued is remeshing equivariant if .
If and agree at every node within hops of , then
for every choice of . This is the book's sentence "since the Laplacian is local, a polynomial filter of degree is localised in -hop neighbourhood". The statement fixes no coefficients and no graph family.
The result. Locality is what separates polynomial filters from general spectral filters. A spectral filter with an arbitrary transfer function is a dense matrix: every output depends on every input. A degree- polynomial filter has support inside the -hop neighbourhood, so it costs sparse matrix products and has a receptive field controlled by . Milestone 4 shows that the same object is also a spectral filter, with transfer function . A polynomial filter is therefore both a spectral filter and a message-passing operation. The book's discussion of rational filters on the same page, which have exponential decay but no local support, uses this contrast. The remeshing companions give the reason spectral constructions are used across different meshes: a remeshing-invariant function of the operator sees only the spectrum.
The formalization. The mathematics is classical, and the mission is about formalizing it. Mathlib has the unweighted combinatorial Laplacian SimpleGraph.lapMatrix and the spectral theorem for Hermitian matrices. The platform has a proved theorem counting walks with powers of an unweighted adjacency matrix. Neither gives the support of powers of a weighted Laplacian, whose nonzero diagonal is not covered by walk counts of a fixed length. None of the statements here is formalized on the platform. The mission produces a reusable support lemma for matrix polynomials of a graph-supported matrix, and a link between spectral and polynomial filters in the matrix language used by graph neural networks.
A first attempt identifies with a count of walks of length exactly , as for the adjacency matrix. That identification fails here. has the diagonal entries , so sums over walks that may pause at a node, and it can be nonzero for at any distance up to . The claim is therefore "within at most hops", and the induction has to track walks of length at most through a matrix with nonzero diagonal. Two encodings make the claim easy and wrong. Mathlib's SimpleGraph.dist is for unreachable pairs, so "" would place every unreachable node inside the neighbourhood. A filter defined through the eigendecomposition is not visibly local, so the locality statement has to be about itself. For the companions, the difficulty is the spectral theorem and the fact that two symmetric matrices with the same characteristic polynomial are orthogonally similar, which requires matching eigenvalue lists up to a permutation.
Matrices are Matrix (Fin n) (Fin n) ℝ, and features are Matrix (Fin n) (Fin d) ℝ, with rows as nodes. The Laplacian is the published definition SpectralSparsify.Sampling.lapMat (degree matrix minus weight matrix), referenced rather than redefined and used under the local name lap. It imposes no condition on . A diagonal weight cancels in . Symmetry is assumed only where the book needs it: the side-note on p. 64. The polynomial filter is the explicit sum with coefficients indexed by . "Within hops" is the existence of a walk of length at most in a simple graph that contains the support of . The goal is stated for every such and for non-symmetric . Both are generalisations of the book's undirected setting, where is the graph of . Permutation matrices act by moving row to row . Remeshing invariance quantifies over all of Mathlib's orthogonalGroup. "The same spectrum" is equality of characteristic polynomials of symmetric matrices.
A trivializing formalization is ruled out: the filter is not defined through an eigendecomposition, "localised" is not defined as "is a polynomial in ", and the hop condition is not stated through the junk-valued SimpleGraph.dist.
A complete development needs the support of products of graph-supported matrices, the spectral theorem in orthogonal form (Mathlib's Matrix.IsHermitian.eigenvectorUnitary), and orthogonal similarity of symmetric matrices with equal characteristic polynomials. The support lemma is reusable for any message-passing operator that is a polynomial in a local matrix. Contributions of these lemmas, and alternative proofs (for example through Polynomial.aeval), are welcome.
Many graphs that graph neural networks (GNNs) are applied to are embedded in space. In a molecular graph the nodes are atoms, and each atom carries both chemical information (its type) and its three-dimensional position. A prediction about the molecule (an energy, a binding affinity) must not depend on where the molecule sits or how it is oriented, and a predicted geometry must move with the molecule. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2, 2021) treats this in §5.5, Equivariant Message Passing Networks: a layer on such graphs should be equivariant to the Euclidean group E(3) of rigid motions "in addition to the standard permutation equivariance discussed before" (p. 83). The book presents the layer of Satorras, Hoogeboom and Welling, E(n) Equivariant Graph Neural Networks (ICML 2021, arXiv:2102.09844), and asserts that it has this property.
The layer is built from the most general of the three "flavours" of GNN layer that §5.3 uses to organise the literature: convolutional, attentional and message passing. This mission therefore also formalizes the two claims of §5.3 that the E(3) layer relies on: message passing is permutation equivariant, and it contains the other two flavours.
The book numbers no theorem, lemma or definition. Every item of this mission is cited by section, equation number (where there is one) and printed page.
A graph on the nodes is given by an adjacency matrix , with an edge whenever . The neighbourhood of is (eq. (11), p. 34). Each node carries a feature ; collected as rows they form the feature matrix . A permutation of the nodes, with permutation matrix , acts by and . A layer is permutation equivariant if (eq. (10), p. 33).
A permutation-invariant aggregator is a function of the multiset of incoming values ("sum, mean, or maximum", p. 78). The three flavours of §5.3 (p. 79), with an update function , are
convolutional with fixed coefficients , attentional with an attention mechanism of the features, and message passing with a message function of receiver and sender.
In §5.5 each node carries features and spatial coordinates . An element acts on coordinates by , "where is an orthogonal matrix modeling rotations and reflections, and is a translation vector" (p. 83). The equivariant message-passing layer (p. 84) is
with and "two distinct (learnable) functions", scalar-valued. The book's desired property (p. 83): if the spatial input is transformed by , "the spatial component of the output transforms in the same way (as ), whereas remains invariant."
For every orthogonal and , applying the layer to gives with
The statement holds for arbitrary , , and ; nothing about the learnable functions is fixed.
The equivariance of the layer is what lets a network built from it be applied to molecules and point clouds without data augmentation over rotations, reflections and translations: invariant outputs are unaffected by the placement of the input, and coordinate outputs move with it. Satorras et al. use the layer, stacked, for molecular property prediction, dynamical systems and graph autoencoders; the equivariance of the stack follows from that of each layer. The containment of the three flavours explains why the book can discuss GNN expressivity (Ch. 7, chunk IX of this series) for message passing alone.
The results are known and their proofs are short computations; none of them has a machine-checked proof on the platform. Formalizing them pins down what the claims mean exactly: that the reflections in are included, that the translation enters the coordinate update only through the leading , and under which condition on the features the containment "convolution ⊆ attention" actually holds.
The mathematics is elementary; the difficulty is in stating the claims at the generality the book uses. The coordinate update is not a function of distances alone: it is linear in the difference vectors , and equivariance rests on being scalar-valued and on the translation cancelling in every difference but surviving in the leading term. The containment "convolution ⊆ attention" fails as a literal identity when two nodes have equal features but different coefficients , since an attention mechanism sees only features; the book's look-up table needs features that identify the nodes. The two halves of the layer aggregate over different index sets ( and all ), so the layer is message passing on two different graphs.
Nodes are Fin n. Node features are a family Fin n → α (for this is the book's matrix , Matrix (Fin n) (Fin d) ℝ). The aggregator is an arbitrary function Multiset M → M' of the multiset of messages, so its permutation invariance holds by construction. A permutation acts by (PX)_u = X_{σ⁻¹(u)} and (PAPᵀ)_{uv} = A_{σ⁻¹(u)σ⁻¹(v)}. Coordinates live in EuclideanSpace ℝ (Fin 3); ranges over Matrix.orthogonalGroup (Fin 3) ℝ, the whole of including reflections, acting through Matrix.toEuclideanLin. The squared norm is kept as printed. No standing assumption of the section restricts or ; is allowed.
The layer takes the coordinates themselves as input. A formalization that fed the layer only the distance matrix would make the feature half trivially invariant and drop the coordinate half; that encoding is ruled out.
One hypothesis is added relative to the page, in milestone 3 only: the features must be pairwise distinct (Function.Injective X) for convolution to be represented by attention or by message passing. Without it the claim is false, and a two-node counterexample is checked in Lean. The inclusion of attention in message passing needs no hypothesis.
The definitions of this mission (neighbourhoods, the permutation action, the three flavours) duplicate objects of chunk II of this series; drafts cannot import drafts, and the duplicates are to be merged after the series is published. Proofs of every item are welcome; the distance lemma, the orthogonal-matrix isometry and the multiset reindexing under a permutation are reusable beyond this mission.
Max Tegmark's letter "On the dimensionality of spacetime" (Classical and Quantum Gravity 14 (1997) L69-L75) is the standard reference for the anthropic selection argument on the dimensionality of spacetime. Many superstring theories and inflationary models predict not a single classical spacetime but an ensemble of effective low-energy worlds with different numbers n of space and m of time dimensions, together with a probability distribution over the pairs (n, m). Tegmark argues that this failure to predict (n, m) = (3, 1) uniquely is a strength rather than a weakness: the selection effect arising from the fact that only some worlds contain self-aware observers collapses the distribution, so that such an ensemble theory may predict that we should find ourselves inhabiting a (3 + 1)-dimensional spacetime with 100% certainty, the Bayesian prior probabilities being completely irrelevant.
The letter's argument has three prongs, and the mission formalizes the mathematical content of each. More or less than one time dimension destroys predictability: the partial differential equations of nature have the hyperbolicity property that makes initial-value problems well posed only when m = 1; with no time dimension the equations are elliptic and an observer could not make any inferences at all about other parts of space from local data; with two or more time dimensions no hypersurface carries well-posed data. More than three space dimensions destroys stability: the Green's function of the Poisson equation scales as the (2 - n)-th power of the radius, the two-body problem has no stable orbit solutions for n > 3, and, by the quantum counterpart the letter cites (Tangherlini), no traditional atoms exist. Fewer than three space dimensions destroys complexity: the letter conjectures that such worlds are too simple and barren to contain observers, citing the absence of gravitational force in general relativity with n < 3 and the topological problems of two-dimensional organisms.
The goal statement of the mission is the Bayesian capstone: in a world ensemble whose observer worlds satisfy the three prongs, the probability of being an observer in a (3, 1)-dimensional world equals the probability of being an observer, so that conditional on observerhood the dimensionality is (3, 1) with probability one. The milestones are the classification trichotomy of the field equations, the space-time symmetry of the classification, the hyperplane obstruction behind the letter's Asgeirsson discussion, the spacelike slice of the single-time world, the predictability equivalence, the harmonicity of the Green profile, and the orbit-stability dichotomy.
The source document is the uploaded letter (tegmark1997.pdf in the mission materials).
The formalization is a three-layer development in the namespace Tegmark. The signature layer (Tegmark_sig) fixes the coordinate model: a world with n space and m time dimensions is the coordinate space over the disjoint union of the n space directions and the m time directions, carrying the quadratic form teg that counts space coordinates positively and time coordinates negatively, so that a single minus sign distinguishes space from time. The layer defines the spacelike and timelike classification of vectors and submodules, the elliptic, hyperbolic, and ultrahyperbolic classes of the field equations, the hyperplanes on which initial data can be posed, and the predictability requirement. The physics layer (Tegmark_phys) carries the Newtonian potential of a point mass in n dimensions — the Green's-function scaling of the Poisson equation — the effective potential of the two-body problem with its circular-orbit and stability criteria, and the radially reduced Laplace equation with the Green profile. The ensemble layer (Tegmark_ensemble) carries the probability space of worlds with the two dimension counts and the measurable observer event.
The following choices are disclosed explicitly.
Compile verification by CI substitution. The authoring environment has no local Lean toolchain, so the compile check demanded by the mission is performed by the continuous integration of the repository (Lean 4.33 with Mathlib): all Lean code below was compiled there before this proposal was submitted, and the code attached to the items is byte-identical to the compiled modules.
The theorem drafts carry sorry. The eight theorem statements are submitted as drafts for human review; each proof body is a single sorry marking the work the mission proposes to complete. The compilation therefore succeeds with exactly one "declaration uses 'sorry'" warning per theorem file.
The coordinate model. A world with (n, m) dimensions is the flat coordinate space over the disjoint union of the n space directions and the m time dimensions, with the signature form. This is the linear-algebra skeleton of the letter's discussion: the classification of the field equations by the eigenvalue signs of the principal symbol is a pointwise, linear matter, and the data-surface and Asgeirsson arguments take place on the hypersurfaces of the tangent space. The mission formalizes the letter's argument in this flat model, which carries it exactly; curved manifolds are not formalized (disclosure 13).
The covariant case of the letter's equation (1). The letter classifies a general second-order linear partial differential equation by the signs of the eigenvalues of the coefficient matrix A of its displayed equation (1), with A, b, and c given functions of the coordinates. The mission formalizes the covariant case, the case the letter's dimensionality argument is about: for the wave equation and the Klein-Gordon equation the principal symbol has the same eigenvalue signs as the metric, so the class of the field equations is a function pdeClass of the pair (n, m) alone. The trichotomy milestone states the three equivalences this yields. Variable-coefficient equations, lower-order terms, and the nonlinear systems the letter mentions are out of scope; the letter's remark there (that no nonlinear terms can make a locally ill-posed problem well posed) is commentary on the classification, not a formalized claim.
Well-posedness represented by the classification. The letter's predictability requirement is that the equations be hyperbolic, so that initial-value problems are well posed, and that the data can be posed on a spacelike hypersurface. The mission does not formalize the PDE theory behind this — Hadamard's well-posedness, the energy estimates, or Asgeirsson's theorem — but takes the classification as the formal content: the predicate Predictable is the conjunction of hyperbolicity of the class and the existence of a spacelike hyperplane. The milestone predictable_m1 then shows that the requirement holds exactly in the single-time worlds with at least one space dimension, which is the letter's time-dimension argument.
Hyperplanes as data surfaces. A hypersurface on which initial data is posed is modeled as a hyperplane: the kernel of a nonzero linear functional; spacelike and timelike hyperplanes are the positive- and negative-definite kernels. The letter's statement that there are no space-like and no time-like hypersurfaces in the ultrahyperbolic case is formalized as the hyperplane obstruction: with at least two time dimensions no hyperplane is spacelike, and with at least two space dimensions no hyperplane is timelike. The deeper Asgeirsson phenomenon of the letter's figure 3 — data in an effectively one-dimensional region determining the solution in a higher-dimensional region, the free-lunch symptom of ill-posedness — is out of scope; the obstruction is the part of the discussion that is linear algebra, and it is what the predictability prong needs.
The Green profile and the Newtonian potential. The potential of a point particle in n space dimensions is the Green's function of the Poisson equation, which scales as the (2 - n)-th power of the radius for n > 2 (Ehrenfest 1917, as the letter cites); the inverse-square law of electrostatics and gravity is the three-dimensional case, an inverse-cube law the four-dimensional one. The physics layer carries the Green profile and the radially reduced Laplace operator; the milestone green_harmonic verifies that the profile is harmonic away from the origin, the defining property of the fundamental solution. The Newtonian potential of the two-body problem is the coupling times the profile, up to sign. Real powers, real division, and deriv are noncomputable in the pinned Mathlib; the definitions of the physics layer that use them are marked noncomputable accordingly.
Classical stability and the quantum counterpart. The letter argues the n > 3 instability with both the classical two-body problem (no stable orbits; the figure-2 swarm either escaping to infinity or spiralling into a cataclysmic collision) and the quantum hydrogen atom (no bound states, Tangherlini 1963). The mission formalizes the classical dichotomy in the effective-potential form: for n at least 3, stable circular Newtonian orbits exist exactly when n is 3. A circular orbit is a positive critical point of the effective potential (the centrifugal barrier plus the Newtonian potential); a stable one has positive curvature there, the linear stability of the orbit. The quantum atom, and the letter's remark that the general-relativistic situation is analogous, are out of scope, as disclosed in the exclusions.
The complexity prong carried as a bound. The letter's third prong — that worlds with fewer than three space dimensions are too simple and barren to contain observers — is supported by citations the mission does not formalize (the absence of gravitational force in general relativity with n < 3; the crossing of nerves argument). The ensemble layer carries the prong as the abstract hypothesis on the observer worlds: at least three space dimensions, the complexity requirement, on a par with the stability requirement of at most three. The goal theorem quantifies over the ensembles satisfying the letter's three premises; it does not derive them, and the letter itself is explicit that it has "not attempted to rigorously demonstrate that observers are impossible for other dimensionalities".
The ensemble layer and the capstone. A world ensemble is a measurable space of worlds with a probability measure, the two effective dimension counts of each world, and the measurable event of the worlds containing observers; nothing further is assumed. The goal theorem: if the observer worlds have positive measure and satisfy the predictability, stability, and complexity requirements, then the measure of the observer worlds inside the (3, 1) region equals the measure of all observer worlds. The positive-measure hypothesis is carried so that the equality reads as the letter's conditional statement ("with 100% certainty"); the measure equality itself is the division-free form of that conditional.
Effective dimensionalities. The letter's n and m are the numbers of non-compactified space and time dimensions, or more generally the effective dimensionalities relevant to the low-energy physics; the mission's dimension counts are these effective numbers, as the letter's first footnote fixes.
Definition names and module stems. The three definition bundles are published under names equal to their module stems (Tegmark_sig, Tegmark_phys, Tegmark_ensemble), so that the platform imports Definitions.Def_Tegmark_* in the theorem preambles resolve, in dependency order sig, then phys, then ensemble.
Exclusions. Out of scope: the general variable-coefficient second-order PDE of the letter's equation (1) with arbitrary coefficient matrix; Hadamard well-posedness and Asgeirsson's theorem; curved manifolds and the general-relativistic no-gravity claim for n < 3 (Deser, Jackiw and 't Hooft, as the letter cites); the quantum hydrogen atom of Tangherlini and the letter's general-relativistic analogue; the particle-decay kinematics with m > 1 (Dorling) and the tachyon physics (Feinberg) beyond the classification symmetry; the superstring compactification and inflationary mechanisms behind the letter's ensembles; the topological nerve-crossing argument; and the null-hypersurface caveat of the letter's footnote (data posed on a light-cone hypersurface).
The mission has eleven items: three reference definitions and eight theorem drafts, in the following order.
Reference definitions (the formalization fragment):
Tegmark_sig: the signature layer. The point space of an (n, m) world, the quadratic form with its spacelike and timelike classifications of vectors and submodules, the three PDE classes with the classifier read off the pair (n, m), the spacelike and timelike hyperplanes (the kernels of nonzero linear functionals on which the form is definite), and the predictability requirement: hyperbolic field equations together with a spacelike hyperplane.Tegmark_phys: the physics layer. The Newtonian potential of a point mass in n dimensions, the effective two-body potential with its circular-orbit and stability criteria, the existence predicate for stable circular orbits, the radially reduced Laplace operator, and the radial Green profile.Tegmark_ensemble: the ensemble layer. The probability space of worlds with a probability measure, the two effective dimension counts, and the measurable observer event.Theorem drafts (milestones in attack order, then the goal):
Tegmark.pde_trichotomy: the class of the field equations of an (n, m) world is elliptic exactly when there are no space or no time dimensions, hyperbolic exactly when there is at least one dimension of each kind and exactly one of one kind, and ultrahyperbolic exactly when there are at least two of each (pages L72-L73).Tegmark.tachyon_symmetry: the class is symmetric under exchanging the numbers of space and time dimensions (page L74).Tegmark.no_spacelike_hyperplane: with at least two time dimensions no hyperplane of the point space is spacelike, and with at least two space dimensions no hyperplane is timelike (page L74).Tegmark.spacelike_slice: every world with exactly one time dimension has a spacelike hyperplane, the spatial slice (pages L73-L74).Tegmark.predictable_m1: for a world with at least one space dimension, the predictability requirement holds exactly when the number of time dimensions is one (pages L72-L74).Tegmark.green_harmonic: for n at least 3, the radial Green profile satisfies the radially reduced Laplace equation at every positive radius (page L70).Tegmark.orbit_stability_31: for n at least 3, the Newtonian two-body problem admits stable circular orbits exactly when n is 3 (pages L70-L71).Tegmark.selection_31 (the goal): in a world ensemble whose observer worlds have positive measure and satisfy the predictability, stability, and complexity requirements, the measure of the observer worlds in the (3, 1) region equals the measure of all observer worlds (pages L69-L70).Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.
The letter is the canonical modern statement of the argument that the dimensionality of spacetime is an anthropic prediction, and the standard citation for its three mathematical prongs: Ehrenfest's 1917 observation on the instability of worlds with more than three space dimensions, the Green's-function scaling behind the dimension-dependence of the force laws, and the hyperbolicity classification behind the predictability of worlds with exactly one time dimension. These prongs rest on classical results — Ehrenfest 1917, Tangherlini 1963, Asgeirsson 1936, the Courant-Hilbert classification — which exist in the physics and PDE literature but have not been formalized together in a proof assistant. The mission packages them as one Lean development with a shared coordinate model, and its capstone is a precise, checkable statement of the letter's Bayesian conclusion: the selection argument is exactly the measure-theoretic fact that a positive-measure event contained in a region carries the region's conditional probability. A formal account also disciplines the argument's edges: the mission's theorems hold exactly where the letter's prose is exact, and the letter's conjectural steps (the complexity prong, the barrenness of n < 3) enter the capstone as explicit hypotheses rather than as unexamined facts.
The trichotomy and symmetry milestones are definitional: the unfolding of the classifier and its symmetry, verifying that the mission's encoding matches the letter's three signature examples. The hyperplane milestones are genuine linear algebra: the obstruction argument must, for every nonzero functional on a space whose time block has at least two dimensions, exhibit a nonzero vector of its kernel inside the time block — a case split on whether the functional vanishes on the block — and the slice milestone evaluates the form on the projection's kernel. The physics milestones are calculus with real powers: harmonicity differentiates the (2 - n)-th power twice and cancels against the (n - 1)/r correction, and the orbit dichotomy reduces the curvature at a circular orbit to the factor (n - 2)(4 - n), whose sign is the three-case analysis n = 3, n = 4, n at least 5. The capstone is measure-theoretic bookkeeping over the ensemble: the collation of the predictability equivalence (which forces one time dimension), the stability bound (at most three space dimensions), and the complexity bound (at least three), pinning every observer world into the (3, 1) region.
Included: the letter's pages L69-L75 at the statement level — the coordinate model of an (n, m) world and its signature form; the covariant PDE classification by the numbers of space and time dimensions; the hyperplane obstruction for multi-time worlds and the spacelike slice of single-time worlds; the predictability equivalence; the harmonicity of the Green profile in n at least 3 dimensions; the effective-potential orbit-stability dichotomy for n at least 3; and the Bayesian capstone over world ensembles.
Excluded, as disclosed in item 13 of section 2: the general second-order PDE of the letter's equation (1) with variable coefficients; the well-posedness theory (Hadamard, the energy estimates, Asgeirsson's theorem) behind the classification; curved spacetimes and the general-relativistic claims; the quantum atom and its general-relativistic analogue; the m > 1 decay kinematics and the tachyon physics beyond the classification symmetry; the compactification mechanisms of the superstring and inflationary ensembles; the topological nerve-crossing argument; and the null-hypersurface caveat.
We show that the following five categories are equivalent: (1) the opposite category of commutative von Neumann algebras; (2) compact strictly localizable enhanced measurable spaces; (3) measurable locales; (4) hyperstonean locales; (5) hyperstonean spaces. This result can be seen as a measure-theoretic counterpart of the Gelfand duality between commutative unital C*-algebras and compact Hausdorff topological spaces.
This mission is the statement-level formalization of Gelfand-type duality for commutative von Neumann algebras (arXiv:2005.05284v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Continuous and completely additive finite valuations (Lemma 2.21, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
51 results of the paper are not stated yet, because the library lacks an interface they need:
This paper develops an abstract framework for constructing ``seminormal forms'' for cellular algebras. That is, given a cellular R-algebra A which is equipped with a family of JM-elements we give a general technique for constructing orthogonal bases for A, and for all of its irreducible representations, when the JM-elements separate A. The seminormal forms for A are defined over the field of fractions of R. Significantly, we show that the Gram determinant of each irreducible A-module is equal to a product of certain structure constants coming from the seminormal basis of A. In the non-separated case we use our seminormal forms to give an explicit basis for a block decomposition of A. The appendix, by Marcos Soriano, gives a general construction of a complete set of orthogonal idempotents for an algera starting from a set of elements which act on the algebra in an upper triangular fashion. The appendix shows that constructions with "Jucys-Murphy elements"depend, ultimately, on the Cayley-Hamilton theorem.
This mission is the statement-level formalization of Seminormal forms and Gram determinants for cellular algebras (arXiv:math/0604108v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gram determinants are products of seminormal structure coefficients (Abstract; Theorem 3.12 determinant consequence, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The cyclotomic Birman-Wenzl-Murakami algebras are quotients of the affine BMW algebras in which the affine generator satisfies a polynomial relation. We study admissibility conditions on the ground ring for these algebras, and show that the algebras defined over an admissible integral ground ring are free --modules and isomorphic to cyclotomic Kauffman tangle algebras. We also determine the representation theory in the generic semisimple case, obtain a recursive formula for the weights of the Markov trace, and give a sufficient condition for semisimplicity.
This mission is the statement-level formalization of Cyclotomic Birman--Wenzl--Murakami algebras, II: Admissibility Relations and Freeness (arXiv:math/0612065v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional expectation of a canonical path idempotent (Lemma 2.19: expectation of a path idempotent, PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
19 results of the paper are not stated yet, because the library lacks an interface they need:
Surfaces of three-dimensional objects are stored in computer graphics, vision and geometry processing as triangular meshes: finitely many points glued together by triangles. Geometric deep learning on such data needs a discretisation of the Laplace–Beltrami operator, because spectral filters, diffusion and many graph neural network layers on meshes are built from a Laplacian. The standard choice is the cotangent Laplacian, whose edge weights are cotangents of the angles of the mesh. It goes back to MacNeal's 1949 thesis and was popularised by Pinkall and Polthier (1993) and Meyer, Desbrun, Schröder and Barr (2003).
Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2), §4.6, pp. 61–63, introduces this operator and states that, although it is defined through angles, it can be written entirely in terms of edge lengths. This is what makes it intrinsic: invariant under every deformation of the surface that preserves the lengths of the edges. This mission formalizes that claim. The book numbers no theorems, lemmas or definitions, so every item is cited by section, equation and printed page.
A mesh on the nodes is a finite set of ordered triplets of distinct nodes, the faces; the order of a triplet is the orientation of the face, and each triangle occurs once. As assumed in §4.6, each edge belongs to two faces and the faces incident to each node form a single loop. The nodes are placed at points of a Euclidean space (the book's ). The mesh carries the metric
A quantity is intrinsic if it can be expressed through alone.
For a face with vertices , the angle is the angle at between the directions to and ; it is the angle opposite the edge . The area of the face is . The face is non-degenerate when its three vertices are affinely independent, that is, not collinear.
The local area element of a node is , one third of the total area of the faces incident to . For an interior edge shared by exactly two faces and , the cotangent weight of equation (25) is
In general, sums the cotangents of the angles opposite over the faces containing that edge. The Laplacian of equation (24) is the matrix , where holds the weights off the diagonal and with .
Heron's expression of three lengths, with semiperimeter , is
For an interior edge whose two faces and are non-degenerate, with and given by Heron's expression,
and the weight of (25) is this right-hand side divided by .
The printed display sets the right-hand side equal to itself. That omits the factor of (25), so the goal states the corrected identity.
The Laplacian with the unnormalised weights is symmetric and positive semidefinite for every manifold mesh of non-degenerate triangles (p. 63, after Wardetzky et al. 2007).
The intrinsic form of the cotangent weights is what makes the cotangent Laplacian, and everything derived from it, invariant under isometric deformations of a mesh. This includes its eigenvalues and eigenvectors, and hence spectral descriptors, heat kernels and spectral convolutions. A bent or articulated shape and its rest pose then give the same operator, which is the reason for the operator's use in shape analysis and in geometric deep learning on meshes.
The individual facts (the law of cosines, Heron's formula, the Dirichlet-energy form of the cotangent Laplacian) are classical and proved in the literature. None of them is stated on the platform for meshes. Mathlib has the law of cosines (EuclideanGeometry.law_cos) but Heron's formula only in its non-importable Archive, and it has no mesh Laplacian. This mission adds a mesh layer to the platform: triangulated faces, edge lengths, face areas, local area elements, the cotangent weights (25) and the Laplacian (24). It also corrects two slips on p. 63: the normalisation in the intrinsic display, and the symmetry claim for (25)'s weights.
The per-face identities are classical trigonometry. The difficulty is not the trigonometry but connecting an extrinsic quantity, an angle between vectors of the ambient space, to a square root of a polynomial in lengths, with the sign under the square root controlled for every triangle, degenerate ones included.
The mesh-level statements need bookkeeping that the page leaves implicit. A face is stored with one orientation, so an edge can appear as inside it, and the angle opposite must be found at whichever vertex is left. The sum defining ranges over all faces, and the hypothesis that is interior has to reduce it to exactly two terms. Isometry invariance must also cover degenerate faces, where Lean assigns junk values to angles. Positive semidefiniteness is the hardest item: obtuse angles have negative cotangents, so the weights can be negative and the usual argument for graph Laplacians with nonnegative weights does not apply.
Nodes are Fin n. The embedding x : Fin n → P takes values in an arbitrary Euclidean affine space P (a real inner product space torsor), of which is an instance. A mesh (TriMesh n) is a Finset of ordered triplets with three distinct nodes per face and no triangle listed twice. The mesh-level theorems assume IsManifoldMesh: a nonempty face set, two faces per edge, and a connected loop of incident faces at each node. Angles are Mathlib's EuclideanGeometry.angle, with the vertex in the middle argument, and is Real.cot. The face area is defined geometrically as and not by Heron's formula; with the latter, Heron's formula and the intrinsic claim would hold by definition and lose their content. The local area element sums the areas of the faces incident to , each counted once. This is the book's formula read over unoriented faces.
The book assumes non-degenerate triangles throughout. Lean's returns the junk value at the angles and , and the Heron area of a degenerate triangle is . So the cotangent identities assume that the triangles in their denominators are non-degenerate (affinely independent vertices). The goal assumes this for the two faces of the edge, and the companion for every face. Heron's formula and isometry invariance also hold for degenerate triples. Every mesh-level theorem carries the standing manifold-mesh condition of pp. 61–62; the goal additionally identifies the two faces of its chosen interior edge.
Contributions welcome: proofs of Heron's formula for points of a Euclidean space, of the per-face cotangent identity, and of the per-face positive semidefinite form. These three are reusable for any discrete differential geometry on the platform.
Geometric deep learning is the programme, set out by Bronstein, Bruna, Cohen and Veličković in Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), of deriving neural network architectures from the symmetries of the domain on which the data live. Convolutional networks on images, permutation-invariant networks on sets, graph neural networks and equivariant networks for molecules are presented there as instances of one template. Chapter 3 of the book, Geometric Priors, gives that template: it fixes what a symmetry of a signal is, what it means for a function to respect it, and how invariant functions are assembled from simpler blocks. This mission formalizes the definitions and the elementary claims of Chapter 3. Its goal is the observation the book uses to explain why such networks must be non-linear.
The book numbers no theorem, lemma or definition. Its only labels are the sections, the equations (1)–(53) and the figures. Every item of this mission is therefore cited by section, equation number (where there is one) and printed page of the arXiv v2 text; a margin note is cited as "side-note, p. n".
A domain is a set . A signal on with values in a set of channels is a function ; the signals form the space (equation (1)), written when .
A group acts on through a map with . It then acts on signals by equation (3):
On real signals this action is linear, so defines a representation of on .
A function is -invariant if for all and . A map between signal spaces on which acts is -equivariant if . A map acts on signals element-wise, .
For a measure on with , the -average of a real signal is
The book takes to be the Haar measure of the group.
The metric distortion of a map between metric spaces is (§4.4, p. 51). A self-map with distortion at most is an -isometry.
The Geometric Deep Learning Blueprint (§3.5, p. 29) builds functions
from equivariant linear layers , element-wise nonlinearities , poolings onto coarser domains, and an invariant global pooling .
For a finite domain , a finite nonzero measure on , and a linear -invariant map from into a real Banach space, for every signal ,
A linear invariant therefore depends on only through .
With and , , so .
The goal is the book's reason for non-linearity. Linear invariant models collapse to functions of the group average, so they cannot tell apart two images with the same mean colour. Expressive invariant models must interleave equivariant linear layers with non-linear maps. Milestones 5–7 are the positive half of the same argument: element-wise nonlinearities keep equivariance, the average turns equivariance into invariance, and stacking such blocks gives the blueprint that the later chapters instantiate on grids, groups, graphs and manifolds. Milestone 4 is the book's reason for leaving exact symmetry behind: small deformations do not form a group, so it replaces invariance to deformations by stability to them.
Each claim of the chapter is proved in one or two lines on the page, and none is new mathematics. What a formalization adds is the precise setting in which they hold. The book names the Haar measure but its identity needs no invariance of ; the average's invariance needs right invariance, which the page does not state; and the printed blueprint is invariant only if the poolings are equivariant. As far as a search of the platform and Mathlib shows, none of these statements has a machine-checked proof. The definitions here (the action on signals, invariance, equivariance, the average, the blueprint) are reusable by every later mission of this series.
The obvious argument for the goal pulls through the integral, which uses linearity in the form "a continuous linear map commutes with the Bochner integral". That needs continuity of and integrability of , and neither is stated on the page. On a finite domain both follow from the setting, finite dimension for continuity and boundedness with measurability for integrability. The measurability of has to be assumed of the group and the action.
For the average's invariance, the substitution is valid only for a right-invariant measure. For the blueprint, the composite's invariance fails for a non-equivariant pooling, so the box's claim is false as printed. For the -isometries, the subtle half is the negative one: exhibiting a deformation that is an -isometry while its square is not.
Ω → C. The goal and the average use real signals on a finite domain ([Fintype Ω]), following the book's side-note on p. 15 that one must always discretise to a finite grid in practice; the other milestones allow any domain and any channel types.act g x := fun u => x (g⁻¹ • u) for [MulAction G Ω], not a MulAction instance on Ω → C.μ with [IsFiniteMeasure μ] and μ ≠ 0. Without those hypotheses Lean's (μ univ).toReal⁻¹ would be and the goal false. The goal assumes no invariance of μ. Milestone 6 adds [μ.IsMulRightInvariant], which the Haar measure of a compact group satisfies.[MeasurableInv G], [MeasurableSMul G Ω] and the discrete σ-algebra on Ω; integrability of g ↦ g.x is a consequence, not a hypothesis. A finite group with the counting measure and a compact group with its Haar measure both fit.The goal cannot be satisfied trivially. groupAverage is defined from μ and the action alone, the goal quantifies over every linear invariant f, and the measure hypotheses exclude the degenerate case in which the average is . Proofs, finite-sum encodings of the average, and versions for complex or vector-valued channels are welcome.
Many learning problems take an unordered collection as input: the points of a point cloud, the particles of a physical system, the atoms of a molecule, the nodes of a graph. Storing such data in memory fixes an order of the elements, but the order carries no information, and a model whose output changes when the rows of its input are shuffled is answering a different question from the one posed. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), §4.1, make this the first instance of their blueprint: the domain is a set (or a graph) of nodes, and the symmetry group is the symmetric group of all reorderings.
Two architectures used in practice follow this pattern. Deep Sets (Zaheer et al., NeurIPS 2017) and PointNets (Qi et al., CVPR 2017) process sets; message-passing graph neural networks process graphs. The design question in both cases is which layers respect the symmetry. For linear layers the question has a complete answer, and the answer determines the layer used by Deep Sets. For graphs, Maron, Ben-Hamu, Shamir and Lipman (2018) counted the linear layers acting on adjacency matrices.
A set of nodes carries node features , stacked as the rows of a matrix . A graph adds an adjacency matrix , eq. (8), whose nonzero entries are the edges.
A permutation acts through its permutation matrix by reordering rows: row of is row of . On adjacency matrices it acts by , reordering rows and columns together.
A function is permutation invariant if for every permutation matrix , and a matrix-valued function is permutation equivariant if . On graphs the book's definitions (9) and (10) are
for any permutation matrix .
The section's constructions are the sum readout (6); the shared node-wise linear map (7); the neighbourhood (11) and the multiset of neighbourhood features (12); and the local layer whose -th row is (13). For one feature channel the two linear generators are the identity and the average , every entry of which is the mean .
The book numbers no theorems, lemmas or definitions; every item of this mission is cited by section, equation number and printed page.
For and a linear map ,
This is the book's sentence on p. 33: any linear equivariant "can be written as a linear combination of two generators, the identity … and the average". Both directions are stated; the content is the "only if" direction.
The result. The goal classifies the linear layers of a set network. Any equivariant linear layer on scalar node features mixes each node's own value with the mean of all values, and nothing else; with several channels the two scalars become two weight matrices, which is exactly the Deep Sets layer. Read the other way, the theorem says that the commutant of the permutation representation of on is two-dimensional (for ), the algebraic fact behind the decomposition into two irreducible pieces. The Maron et al. count does the same for layers acting on adjacency matrices and fixes the size of the parameter space of invariant graph networks. The milestones give the elementary invariance and equivariance facts on which the graph-network chapter rests, including the constant aggregate on a complete graph.
Formalizing it. All results here are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no statement about the commutant of the permutation representation or about equivariant layers on sets. The mission produces a vocabulary of permutation actions on feature and adjacency matrices, and the invariance and equivariance definitions (9)–(10), that later missions of this series (the WL comparison, the E(3)-equivariant layer) also use. Two of the book's printed claims need correction to be true, and the formal statements record the corrected versions.
The milestones are short reindexing arguments; the work is in choosing encodings that keep them faithful. The goal's "if" direction is a one-line computation. The "only if" direction is where an argument is needed: equivariance under all of must force the matrix of to have one value on the diagonal and one value off it. Equivariance under a smaller group does not suffice: commuting with the cyclic shift alone gives all circulant matrices, an -dimensional space, so the argument must use permutations beyond the shifts. The channel version adds a tensor-product layer to the same argument. The Maron et al. count is a dimension statement, so it needs both a spanning family and its independence, and the count is sensitive to : for the dimension is strictly smaller than 15, so any argument must use somewhere.
Node features are Matrix (Fin n) (Fin d) ℝ (rows are nodes); a single channel is Fin n → ℝ. A permutation is σ : Equiv.Perm (Fin n), acting by X.submatrix σ.symm id (row of is row ) and on adjacency matrices by A.submatrix σ.symm σ.symm; this one convention is used in every statement. Adjacency matrices are real; the edge set is the set of nonzero entries, which for the book's 0/1 matrix (8) is its edge set and also admits weighted graphs. The function of (13) and the aggregator of §5.4 take a Multiset, so their invariance to the order of the neighbours holds by construction. The average is written with , and the goal and channel version assume . Equivariance quantifies over every permutation of , never a generating subset. The complete-graph item states the identical-aggregate clause of §5.4. The page's later claim of equal expressive power across inputs is false: with , , , and , changing changes while stays fixed, which no node-only map can reproduce.
A trivializing formalization is ruled out: "equivariant" is the commutation property itself, never defined as "of the form ".
Two printed claims are corrected. On p. 33 the two-generator form is stated for matrices with channels; it is false for (the map of (7) is a counterexample), so the goal is single-channel and the multi-channel statement uses weight matrices. On p. 34 the fifteen generators are said to be independent of ; the dimension is 1, 8 and 14 for , so that item assumes , and it is stated for adjacency-to-adjacency maps as the side-note on p. 33 specifies.
The development needs Mathlib's Equiv.Perm, Matrix.submatrix, Finset sums and reindexing (Equiv.sum_comp), Multiset.map, and Module.finrank. Proofs of the commutant statements, of the multi-channel version and of the dimension count are welcome; the permutation-action and invariance lemmas proved along the way are reusable by any later development on graph networks.
Convolutional networks use the same filter at many locations. A shift of the input then shifts the output in a predictable way, allowing one set of filter coefficients to serve every location. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, §4.3, pp. 40–43 ask how this idea extends when the transformations form a group and the signal domain need not be the group itself. A grid and its cyclic shifts are one example; a sphere and its rotation group are another. In the latter example, a rotation is an output index even though it is not a point of the sphere. This distinction matters when a second convolutional layer processes the first layer's output.
The chapter places this construction within its general account of geometric deep learning: symmetries specify how inputs transform, and a compatible map should transform its outputs in a corresponding way. Here the concrete question is whether the integral defining group convolution has that compatibility. The source calls this property equivariance and gives it immediately after equation (14). The book numbers equations but no theorems, lemmas, propositions, or definitions, so the items below are cited by section, equation, and printed page.
Let be a group acting transitively on a domain ; write for the image of . The section makes this homogeneous-domain assumption explicit on p. 43. A signal is a scalar function , and a filter is another such function . The group acts on signals by the inverse action on their arguments:
This convention makes a left group representation on functions. Let be a measure on invariant under the action of every element of . The book states this measure convention beside its pairing formula on p. 41. The pairing and group convolution are
The convolution is indexed by , so it is a signal on , even when and are different spaces. Signals use the regular action . On the cyclic grid , the source uses for the action of a shift on an index . These conventions are the ones used throughout this mission. Equation (14) and the surrounding definitions, §4.3, pp. 41–43.
For every and scalar signals on , the main target is
The theorem keeps the domain action and the output regular action distinct. The invariant measure and transitive action are part of the source's setting. §4.3, equation (14) and the following displayed identity, p. 41; homogeneous-domain assumption, p. 43.
The milestone list records three claims from the same section. First, the pairing matches a transformed filter to the inversely transformed signal: . Second, the signal action satisfies . Third, for on the cyclic grid, the finite-sum instance of group convolution has the form . The source's side-note calls the last expression cross-correlation. §4.3, pp. 41–42.
The equality specifies what happens to every output coordinate after a group transformation of the input. Its output is a function on , so the statement also fixes which action later layers must use. In the sphere example, the first convolution produces a function on the rotation group rather than a function on the sphere; the book then describes applying a second group convolution on that output. §4.3, pp. 42–43.
The result is proved in the source. The remaining work here is to make the invariant measure, the two actions, and the real integral into separately inspectable Lean definitions and to supply machine-checked proofs of the open theorem statements. The cyclic example checks the sign convention at a concrete boundary: using for the group action yields after applying the inverse shift. Those definitions can also support later formalizations of group-indexed layers. This mission does not assert results for learned networks or approximation power; its target is the mathematical convolution identity displayed in the book.
The two occurrences of in the printed identity act on different function spaces. On the left, transforms a signal on ; on the right, the regular action transforms a function on . Treating both as a single action obscures the type and can silently reverse the group multiplication order. The group need not be commutative, so this order matters. The measure must also be invariant: a Dirac measure concentrated at a point that moves under the group generally changes the pairing and breaks the claimed equivariance. In the cyclic example, an inverse shift changes the sign again, which is why the output has rather than .
Lean represents a signal as a function , the group action using MulAction, and the measure as a measure on . The action on signals, the pairing, group convolution, and the output regular action are explicit functions. The integral theorems require a transitive action, as the section specifies on p. 43, plus measurable spaces on and , a measurable group action, and an invariant measure. These are the conditions under which the source's change of variables is meaningful. The cyclic example applies the same group convolution to the counting measure on ZMod n, , with the shift group acting by . It does not identify a cyclic convolution with a planar convolution or assume the group and domain coincide in the general theorem.
The source describes as a Hilbert space. The Lean theorem states the integral identity for arbitrary real functions; on integrable products the pairing has its ordinary meaning, while Lean assigns zero to a nonintegrable integral. The identity remains valid at those totalized inputs because the same measure-preserving transformation relates the two integrands. No integrability hypothesis is used to reduce the stated range. The zero measure is included, but the theorem is universal over invariant measures, including nonzero counting measure on finite group actions; it cannot be proved by choosing a zero measure or an empty domain. Reusable contributions include properties of the signal action, invariant integration under actions, and finite cyclic examples. The transform-and-convolve equation (32) and the second-layer composition on are outside this chunk's milestone list.
A pseudoholomorphic map from a planar domain into an almost complex manifold solves the nonlinear Cauchy–Riemann equation
These maps are the basic objects of Gromov's theory of holomorphic curves, of Floer homology and of symplectic field theory. Two analytic facts about them are used everywhere: solutions of low regularity are automatically smooth, and families with a uniform bound on the first derivative are precompact in . A third fact, unique continuation, says that a solution is determined near a point by its derivatives there.
This mission formalizes these results locally, for maps from discs into a finite-dimensional real vector space with an almost complex structure defined on an open subset, following C. Wendl, Lectures on Symplectic Field Theory, Lecture 2 (§ 2.4–2.5) and Proposition 9.1. Mathlib has no Sobolev spaces of weakly differentiable maps, no almost complex structures and no pseudoholomorphic maps. The definitions build on the norm of the DbarRegularity mission.
Let in be smooth almost complex structures on and let be compact. Every sequence of -holomorphic maps with has a subsequence converging in on to a smooth -holomorphic map (Wendl, Proposition 9.1).
The results. Regularity and compactness are the local half of Gromov compactness: once a moduli space of holomorphic curves has a uniform bound, it is precompact in the smooth topology. Unique continuation is the local input for the structure theory of holomorphic curves, such as the decomposition of a curve into a simple curve and a branched cover.
Formalizing them. The mission introduces almost complex structures, pseudoholomorphic maps, weak derivatives and solutions of a nonlinear first-order system, in a form that applies to any finite-dimensional target and to structures defined on an open subset. These are foundations for finite-energy holomorphic curves in symplectizations, the next stage of this series. Milestones 4 and 5 are statements about linear first-order elliptic equations in the plane, and milestone 6 is a normal form for real-linear Cauchy–Riemann equations; all three are of independent use in complex analysis.
The equation is nonlinear in and the structures vary with ; the statements about sequences are uniform in , with all constants chosen before the index. The weak formulation involves maps that are not assumed differentiable, and the conclusion of milestone 1 is classical smoothness of the given continuous map, not of a representative. The almost complex structure is only defined on an open subset of the target, so every statement keeps track of where the maps take their values. In milestone 6 the complex structure on the target varies with the point of the domain.
JHolomorphic. The definition module JHolomorphic_Setting defines IsAlmostComplexOn, dbarJ, IsJHolomorphicOn, HasWeakPartialsOn, IsWeakJHolomorphicOn and TendstoCInftyLocOn. It imports the DbarRegularity setting for sobolevNorm (the norm ).[FiniteDimensional ℝ E], without an inner product. is EuclideanSpace ℂ (Fin n). Almost complex structures have type E → E →L[ℝ] E.ENNReal.ofReal p.ContDiffOn ℝ ∞ (, not analytic); derivatives of order are iteratedFDeriv ℝ m.Contributions welcome: general lemmas on weak derivatives and on spaces over planar domains.
We consider group-covariant positive operator valued measures (POVMs) on a finite dimensional quantum system. Following Neumark's theorem a POVM can be implemented by an orthogonal measurement on a larger system. Accordingly, our goal is to find an implementation of a given group-covariant POVM by a quantum circuit using its symmetry. Based on representation theory of the symmetry group we develop a general approach for the implementation of group-covariant POVMs which consist of rank-one operators. The construction relies on a method to decompose matrices that intertwine two representations of a finite group. We give several examples for which the resulting quantum circuits are efficient. In particular, we obtain efficient quantum circuits for a class of POVMs generated by Weyl-Heisenberg groups. These circuits allow to implement an approximative simultaneous measurement of the position and crystal momentum of a particle moving on a cyclic chain.
This mission is the statement-level formalization of Implementation of group-covariant POVMs by orthogonal measurements (arXiv:quant-ph/0407054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetry-preserving orthogonal dilation (Paper main result: symmetry-preserving orthogonal dilation, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Within the abstract framework of dynamical system theory we describe a general approach to the Transient (or Evans-Searles) and Steady State (or Gallavotti-Cohen) Fluctuation Theorems of non-equilibrium statistical mechanics. Our main objective is to display the minimal, model independent mathematical structure at work behind fluctuation theorems. Besides its conceptual simplicity, another advantage of our approach is its natural extension to quantum statistical mechanics which will be presented in a companion paper. We shall discuss several examples including thermostated systems, open Hamiltonian systems, chaotic homeomorphisms of compact metric spaces and Anosov diffeomorphisms.
This mission is the statement-level formalization of Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems (arXiv:1009.3248v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-time Evans–Searles theorem (Proposition 3.3, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
79 results of the paper are not stated yet, because the library lacks an interface they need:
We point out a general argument leading from the formula for currents through an open mesoscopic system given by the theory of non-equilibrium steady states (NESS) to the Landauer-Büttiker formula.
This mission is the statement-level formalization of A general proof of Landauer-Büttiker formula (arXiv:math-ph/0603030v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-channel optical theorem with the Landauer–Büttiker transition normalization (Equations (15)–(17), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We establish a framework for cellularity of algebras related to the Jones basic construction. Our framework allows a uniform proof of cellularity of Brauer algebras, ordinary and cyclotomic BMW algebras, walled Brauer algebras, partition algebras, and others. Our cellular bases are labeled by paths on certain branching diagrams rather than by tangles. Moreover, for the class of algebras that we study, we show that the cellular structures are compatible with restriction and induction of modules. Applied to cyclotomic BMW algebras, our method allows a new a shorter proof of the finite spanning result and isomorphism with cyclotomic Kauffman tangle algebras.
This mission is the statement-level formalization of Cellularity and the Jones basic construction (arXiv:0906.1496v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Free modules embed into their fraction-field scalar extension (Lemma 2.20, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
70 results of the paper are not stated yet, because the library lacks an interface they need:
We propose a unified framework in which the different constructions of cohomology groups for topological and Lie groups can all be treated on equal footings. In particular, we show that the cohomology of "locally continuous" cochains (respectively "locally smooth" in the case of Lie groups) fits into this framework, which provides an easily accessible cocycle model for topological and Lie group cohomology. We illustrate the use of this unified framework and the relation between the different models in various applications. This includes the construction of cohomology classes characterizing the string group and a direct connection to Lie algebra cohomology.
This mission is the statement-level formalization of A Cocycle Model for Topological and Lie Group Cohomology (arXiv:1110.3304v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem VI.2: delta-functor comparison principle (Theorem VI.2: delta-functor comparison principle, PDF p. 25). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
63 results of the paper are not stated yet, because the library lacks an interface they need:
We present an axiomatic approach to finite- and infinite-dimensional differential calculus over arbitrary infinite fields (and, more generally, suitable rings). The corresponding basic theory of manifolds and Lie groups is developed. Special attention is paid to the case of mappings between topological vector spaces over non-discrete topological fields, in particular ultrametric fields or the fields of real and complex numbers. In the latter case, a theory of differentiable mappings between general, not necessarily locally convex spaces is obtained, which in the locally convex case is equivalent to Keller's C^k_c-theory.
This mission is the statement-level formalization of Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite Fields (arXiv:math/0303300v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularity of a co-restriction to a subspace (Lemma 10.1, PDF p. 48). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
65 results of the paper are not stated yet, because the library lacks an interface they need:
We generalize the classical construction principles of infinite-dimensional real (and complex) Lie groups to the case of Lie groups over non-discrete topological fields. In particular, we discuss linear Lie groups, mapping groups, test function groups, diffeomorphism groups, and weak direct products of Lie groups. The specific tools of differential calculus required for the Lie group constructions are developed. Notably, we establish differentiability properties of composition and evaluation, as well as exponential laws for function spaces. We also present techniques to deal with the subtle differentiability and continuity properties of non-linear mappings between spaces of test functions. Most of the results are independent of any specific properties of the topological vector spaces involved; in particular, we can deal with real and complex Lie groups modeled on non-locally convex spaces.
This mission is the statement-level formalization of Lie groups over non-discrete topological fields (arXiv:math/0408008v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The ordinary difference quotient and its continuous extension (Numbered assertion 1.8, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
111 results of the paper are not stated yet, because the library lacks an interface they need:
This article presents an isomorphism between two operator algebras and where is the set of operators on a space of Hilbert-Schmidt operators and is the set of operators on a tensor product space. We next compare our isomorphism to a well-known result called Choi's isomorphism theorem. The advantage of Choi's isomorphism is that it takes completely positive maps to positive operators. One advantage of our isomorphism is that it applies to infinite dimensional Hilbert spaces, while Choi's isomorphism only holds for finite dimensions. Also, our isomorphism preserves operator products while Choi's does not. We close with a brief discussion on some uses of our isomorphism.
This mission is the statement-level formalization of Operator Isomorphisms on Hilbert Space Tensor Products (arXiv:2010.15901v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.3: formula for a basis conjugation (Lemma 1.3, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
19 results of the paper are not stated yet, because the library lacks an interface they need:
A moving dielectric appears to light as an effective gravitational field. At low flow velocities the dielectric acts on light in the same way as a magnetic field acts on a charged matter wave. We develop in detail the geometrical optics of moving dispersionless media. We derive a Hamiltonian and a Lagrangian to describe ray propagation. We elucidate how the gravitational and the magnetic model of light propagation are related to each other. Finally, we study light propagation around a vortex flow. The vortex shows an optical Aharonov--Bohm effect at large distances from the core, and, at shorter ranges, the vortex may resemble an optical black hole.
This mission is the statement-level formalization of Optics of Nonuniformly Moving Media (arXiv:physics/9906038v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Ray Hamiltonian, comoving speed, and wave-number independence (§III B, (30)–(38): ray Hamiltonian, comoving speed and independence of wave number, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We study optimal teleportation based on the Bell measurements. An explicit expression for the quantum channel associated with the optimal teleportation with an arbitrary mixed state resource is presented. The optimal transmission fidelity of the corresponding quantum channel is calculated and shown to be related to the fully entangled fraction of the quantum resource, rather than the singlet fraction as in the standard teleportation protocol.
This mission is the statement-level formalization of Optimal Teleportation Based on Bell Measurement (arXiv:quant-ph/0208015v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal Bell-measurement teleportation channel and attained mean fidelity (Theorem 3, Eqs.(14)-(15): optimal Bell-measurement channel and maximal mean fidelity (abstract seed), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We construct classes of von Neumann algebra modules by considering ``column sums" of noncommutative L^p spaces. Our abstract characterization is based on an L^{p/2}-valued inner product, thereby generalizing Hilbert C*-modules and representations on Hilbert space. While the (single) representation theory is similar to the L^2 case, the concept of L^p bimodule (p not 2) turns out to be nearly trivial.
This mission is the statement-level formalization of Noncommutative Lp modules (arXiv:math/0301044v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compatible bounded operator nets have a strong limit (corrected infinite endpoint) (unnumbered-infinite-exponent-compatible-net, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
37 results of the paper are not stated yet, because the library lacks an interface they need:
We generalize the universally composable definition of Canetti to the Quantum World. The basic idea is the same as in the classical world. The main contribution is that we unfold the result in a new model which is well adapted to quantum protocols. We also simplify some aspects of the classical case. In particular, the case of protocols with an arbitrary number of layers of sub-protocols is naturally covered in the proposed model.
This mission is the statement-level formalization of General Security Definition and Composability for Quantum & Classical Protocols (arXiv:quant-ph/0409062v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is All parity-bit biases control the Euclidean distance of string laws (§2.4, unnumbered parity bound, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need: