Lean statements

Lean is a language for mathematical statements and proofs that a computer can verify. The release supplies 416 statement files, listing 189 as main results. Each row links a Lean statement to its possible paper counterpart and shows independent assessments and reports of proof verification.

Every Lean statement

Sort by

Discipline

Pairing

MathVet

cert-machine

Words

416 of 416 shown

The independent groups, MathVet; Carlos Toledo’s cert-machine, assess whether each family’s Lean statements express the whole result OpenAI describes in its catalogue. Each row shows that family-level assessment. A possible match selected from shared wording has no recorded review of whether the statements mean the same thing.

Lean statements, possible paper matches, independent assessments of each family and reports of accepted Comparator runs
Lean statement	Family		Paired paper statement	MathVet on the family	cert-machine on the family	Reports of acceptance		Local definitions
Noncoordinate polynomial in every dimension at least four`AbhyankarSathaye`Algebraic and complex geometry	A stable-coordinate counterexample in four variables	Algebraic and complex geometry	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	0	7
Affine Bernstein classification for complete graphs in dimensions three through nine`AffineBernstein`Differential geometry	Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexample	Differential geometry	Theorem 1.1The affine Bernstein theorem in dimensions three through ninepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	11	51
Polynomial-time construction of strong thin trees`AlgorithmicThinTrees`Combinatorics	Deterministic construction of strong thin spanning trees	Combinatorics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	37	131
Additivity and capacity for generalized amplitude damping`AmplitudeDamping`Mathematical physics	Classical capacity of generalized amplitude damping	Mathematical physics	Theorem 1.1Classical capacity and entropy inequalities for generalized amplitude dampingpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	22	77
Three-fixed-point Arnold counterexample`ArnoldCounterexample`Differential geometry	Counterexamples to stable-Morse and strong Arnold fixed-point bounds	Differential geometry	Theorem 1.1Three fixed points on the symplectic quadric threefoldpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	19	74
Artin group with no geometric $\mathrm{CAT}(0)$ action`ArtinCAT0`Group theory	Classifying spaces and geometric obstructions for Artin groups	Group theory	Theorem 1.1An Artin group with no geometric CAT(0) actionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	13	51
Parabolic intersections, closures, and structural consequences`ArtinParabolicIntersections`Group theory	Classifying spaces and geometric obstructions for Artin groups	Group theory	Corollary 1.4Parabolic intersections in Artin groupspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	16	64
Asymptotically minimal Littlewood maximum`AsymptoticallyMinimalLittlewood`Real and complex analysis	Real ultraflat Littlewood polynomials and unbounded binary merit factors	Real and complex analysis	Theorem 1.1Asymptotically minimal maxima of real Littlewood polynomialspossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	3	10
Sharp Gaussian minorants from an atomic certificate`AtomicGaussian`Convex and metric geometry	Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy	Convex and metric geometry	Theorem 1.2An atomic certificate for triangular-lattice universal optimalitypossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	68	147
Auslander–Reiten counterexample`AuslanderReiten`Algebra	Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures	Algebra	Theorem 1.1An explicit counterexample to the Auslander-Reiten conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	6	49
Quasinilpotent operator with transitive commutant`BackwardIntertwiners`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	Corollary 1.2Backward intertwiners and a transitive commutantpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	4	18
Incompressible transport of solid boxes`BalancedBoxRouting`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	24	64
Balanced Ryser counterexamples at prime orders`BalancedRyser`Combinatorics	Counterexamples to Ryser’s covering conjecture	Combinatorics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	No	8	19
Finite computation in a balanced zero-data fluid flow`BalancedThreeStack`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	Theorem 1.1Velocity-Field Detection of Computation in Forced Navier–Stokes Flowspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	51	172
Exact criterion for higher-dimensional symplectic ball packings`BallPacking`Differential geometry	Symplectic ball packing in higher dimensions	Differential geometry	Theorem 1.1Symplectic Ball Packings in Higher Dimensionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	8	24
Necessity of the volume and pairwise capacity inequalities`BallPackingNecessity`Differential geometry	Symplectic ball packing in higher dimensions	Differential geometry	Theorem 1.1Symplectic Ball Packings in Higher Dimensionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	8	24
Barnette’s Hamiltonian-cycle conjecture`BarnetteHamiltonian`Combinatorics	Barnette’s Hamiltonian-cycle conjecture	Combinatorics	Theorem 1.1Paired states and Hamiltonian cycles in cubic bipartite planar graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	5	31
Trace rank and characteristic-zero Kaplansky idempotents for torsion-free groups`BassTorsionFree`Algebra	The ℓ¹-Bass conjecture for all discrete groups	Algebra	Corollary 1.2The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	2	No	18	194
Complex Bass trace vanishing and support`BassTrace`Algebra	The ℓ¹-Bass conjecture for all discrete groups	Algebra	Corollary 1.2The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecturepossible match from catalogue wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	31	387
Nonuniqueness phase and critical laws on quasi-transitive graphs`BenjaminiSchramm`Probability and statistical mechanics	The Benjamini–Schramm nonuniqueness conjecture	Probability and statistical mechanics	Corollary 1Nonuniqueness of percolation on nonamenable quasi-transitive graphspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	42	137
A nonflat one-homogeneous Bernoulli minimizer in dimension seven`BernoulliNonflatInSeven`Partial differential equations	The critical dimension for the one-phase Bernoulli problem	Partial differential equations	Theorem 1.1The critical dimension for one-phase Bernoulli minimizerspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	12	45
Uniform bi-Hölder optimal transport`BiholderTransport`Differential geometry	Weak MTW curvature gives convexity and regular optimal transport	Differential geometry	Theorem 1.1Uniform Bi-Holder Transport from Weak MTWpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	13	68
Unbounded configuration gaps and additive hardness`BinPackingGap`Theoretical computer science	Bin packing and unbounded configuration-LP gaps	Theoretical computer science	Theorem 1.2Additive hardness and unbounded configuration gaps in bin packingpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	68	229
Binary edit-distance distortion lower bound`BinaryEditLower`Convex and metric geometry	The sharp exponential scale of edit-distance distortion	Convex and metric geometry	Theorem 1.1Tree Constructions for the l1 Distortion of Binary Edit Distancecited in the Lean source; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	9	28
Deterministic approximate matching count`BinaryMatching`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	Theorem 1.1A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	14	45
Binary sweep contraction and mixing`BinarySweep`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Conditional coordinate sweeps and analytic transferpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	18	58
Crossing number of complete bipartite graphs`BipartiteCrossing`Combinatorics	The Harary–Hill and Zarankiewicz crossing-number formulas	Combinatorics	Theorem 1.1The crossing number of complete bipartite graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	11	35
Injectivity of Bogomolov–Pop reconstruction modulo the stated ambiguities`BogomolovPopInjectivity`Number theory	Function-field reconstruction from Milnor K-theory and Galois data	Number theory	Theorem 1.1The Bogomolov-Pop reconstruction theorempossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	24	92
Two periodic hard-sphere Boltzmann solutions with the same data`BoltzmannNonuniqueness`Partial differential equations	Nonuniqueness with local conservation for the hard-sphere Boltzmann equation	Partial differential equations	Theorem 1.1Nonuniqueness for the periodic hard-sphere Boltzmann equationpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	1	No	38	143
Boone–Higman equivalence`BooneHigman`Group theory	Boone–Higman embeddings with higher finiteness	Group theory	Theorem 1.1Finite algebraic envelopes and the Boone–Higman conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	4	16
Nine-dimensional Borsuk counterexample`BorsukNine`Combinatorics	Borsuk’s conjecture fails in dimension nine	Combinatorics	Theorem 1.1A nine-dimensional counterexample to Borsuk’s covering assertionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	6	19
Bounded recovery from modular spectral averages`BoundedRecovery`Operator algebras	Relative bicentralizers and modular spectral recovery	Operator algebras	Theorem 4.1Bounded recovery for modular spectral averagespossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	Yes	12	59
Tree-potential midpoint convexity and renorming obstruction`BoundedTreePotentials`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	27	295
Bounded-treewidth graph metrics in $L_1$`BoundedTreewidthL1`Convex and metric geometry	Bounded-distortion L₁ embeddings of planar and bounded-treewidth graphs	Convex and metric geometry	Theorem 1.1L1 Embeddings of Graphs of Bounded Treewidthpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	5	25
One-third stability of Brenier maps and sharpness`Brenier`Partial differential equations	Sharp one-third stability of Brenier maps	Partial differential equations	Theorem 1.1Sharp One-Third Stability of Brenier Mapspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	12	78	12 definitions checked by name and type only
Brennan and inverse-square integral-means bounds`Brennan`Real and complex analysis	Brennan’s conjecture and the integral-means spectrum	Real and complex analysis	Theorem 1.1Brennan’s conjecture and sharp inverse-square integral meansCorollary 1.2Brennan’s conjecture and sharp inverse-square integral meanspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	8	31
Sharp endpoint divergence`BrennanSharp`Real and complex analysis	Brennan’s conjecture and the integral-means spectrum	Real and complex analysis	Theorem 1.1Brennan’s conjecture and sharp inverse-square integral meanspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	8	18
Finite-graph buffered Ising likelihood comparison`BufferedIsing`Probability and statistical mechanics	Conformal universality for weakly interacting and random-bond Ising models	Probability and statistical mechanics	Theorem 1.1Buffered comparison and stopping-band resolution in critical Isingpossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	No	16	66
Bi-Lipschitz absorption of $c_0$`C0Absorption`Functional analysis	Lipschitz equivalent Banach spaces need not be linearly isomorphic	Functional analysis	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	5	16
A $C^1$ counterexample to the entropy conjecture`C1EntropyCounterexample`Dynamical systems and ergodic theory	A C¹ counterexample to the entropy conjecture	Dynamical systems and ergodic theory	Theorem 1.1A C^1 Counterexample to the Entropy Conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	12	45
CH categoricity-threshold obstruction`CHObstruction`Mathematical logic	Shelah’s eventual categoricity and the prescribed-threshold obstruction	Mathematical logic	Theorem 1.1A CH obstruction to a prescribed categoricity thresholdpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	14	63
Area-controlled end replacement and Schwarzschild equality examples`CKSBondiPenrose`Mathematical physics	Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions	Mathematical physics	Theorem 1.1Area-controlled end replacement and the Bondi Penrose inequality in the CKS classpossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	No	310	1,857
Cannon’s geometric-action conclusion`CannonGeometricAction`Group theory	Cannon’s conjecture	Group theory	Theorem 1.1A Modulus Proof of Cannon’s Conjecturepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	16	64
Compactness of normalized chart-field retractions`CartierChartCompactnessSupport`Algebraic and complex geometry	Bounded klt complements for Fano contractions	Algebraic and complex geometry	Theorem 1Uniform Cartier sections for Fano type contractionspossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “SUPPORT-ONLY”	3	Yes	1	17	Imports outside Mathlib: OAI.AlgebraicGeometry.CartierSections.FieldTopology, OAI.AlgebraicGeometry.CartierSections.FieldRetraction
Irrationality of Catalan’s constant`Catalan`Number theory	Irrationality of Catalan’s constant	Number theory	Theorem 1.1Catalan’s constant is irrationalpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	0	3
Nonuniqueness for every nonamenable Cayley graph`CayleyPercolation`Probability and statistical mechanics	The Benjamini–Schramm nonuniqueness conjecture	Probability and statistical mechanics	Corollary 1Nonuniqueness of percolation on nonamenable quasi-transitive graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	17	50
Kirchberg–Rørdam character criterion`CharacterCriterion`Operator algebras	The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability	Operator algebras	Theorem 1.1The Kirchberg–Rørdam character criterionpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	146	1,804
Compatibility of the produced marked solution with every seam equation`CharacterVarietiesAllSeamsSupport`Number theory	Potential integral density on curve character varieties	Number theory	Theorem 1.1Integral points on character varieties of curvespossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “SUPPORT-ONLY”	2	Yes	0	9	Imports outside Mathlib: OAI.AlgebraicGeometry.CharacterVarieties.Seams.ProducedEquations
Polynomial-time query outside choiceless polynomial time`ChoicelessPolynomialTime`Mathematical logic	Separating choiceless counting from polynomial time and witnessed choice	Mathematical logic	Theorem 1Choiceless polynomial time with counting does not capture polynomial timepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	83	337
Classification of circulant Hadamard orders`CirculantHadamard`Combinatorics	The circulant Hadamard and Barker-sequence conjectures	Combinatorics	Theorem 1.1The circulant Hadamard conjecturepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	5	13
Exponential correlation decay for classical $O(n)$ models`ClassicalON`Probability and statistical mechanics	Canonical $O(3)$ continuum limit and exact $O(4)$ mass asymptotics	Probability and statistical mechanics	Theorem 1.1Exponential decay in two-dimensional classical O(n) modelspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	12	33
Logarithmic independence bound for clique-free graphs`CliqueFreeLog`Combinatorics	Correspondence coloring with a fixed forbidden subgraph	Combinatorics	Theorem 1.1A logarithmic independence bound for clique-free graphspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	1	10
Failure of rational injectivity for ordinary coarse assembly`CoarseAssembly`Topology	Failure of rational injectivity for maximal coarse assembly	Topology	Theorem 1.1A counterexample to the coarse Novikov conjecturepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	0	No	216	4,469
Bounded-degree coboundary expanders in dimensions at least three`CoboundaryExpanders`Combinatorics	Bounded-degree coboundary expanders	Combinatorics	Theorem 1.1Bounded-degree coboundary expanders in every dimensionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	No	15	46
FPRAS for common matroid bases`CommonBasesFPRAS`Theoretical computer science	Approximate counting of common integer polymatroid bases	Theoretical computer science	Theorem 1.1Approximate counting of common bases of two matroidspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	15	106
Commuting locally nilpotent derivations`CommutingDerivations`Algebraic and complex geometry	A stable-coordinate counterexample in four variables	Algebraic and complex geometry	Corollary 1.2An explicit noncoordinate polynomial with affine three-space zero fibrepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	17	39
Compact counterexamples in infinite-dimensional Banach spaces`CompactBanach`Convex and metric geometry	Compact counterexamples to bi-Lipschitz dimension reduction	Convex and metric geometry	Theorem 1A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	2	15
Crossing number of complete graphs`CompleteCrossing`Combinatorics	The Harary–Hill and Zarankiewicz crossing-number formulas	Combinatorics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	12	55
Complete polynomial inequality and sharpness`CompleteCrouzeix`Functional analysis	The complete Crouzeix conjecture	Functional analysis	Theorem 3.2A direct proof of the complete Crouzeix inequalitypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	5	20
Complex affine-space cancellation counterexample`ComplexCancellation`Algebraic and complex geometry	Zariski cancellation and affine fibrations over the complex numbers	Algebraic and complex geometry	Theorem 1.1An explicit failure of complex affine-space cancellationpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	10	15
Scalar conductivity nonuniqueness`Conductivity`Partial differential equations	Joint metric and connection recovery from one boundary patch	Partial differential equations	Corollary 1.2Nonuniqueness for bounded measurable scalar conductivities in three dimensionspossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	23	52
No conjugate points without a nonpositively curved metric`ConjugatePoints`Differential geometry	A three-manifold without conjugate points or nonpositive curvature	Differential geometry	Theorem 1.1A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metricpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	18	79
Exact and bounded-time sampling of contingency tables`ContingencyTables`Theoretical computer science	Sampling and counting contingency tables with arbitrary margins	Theoretical computer science	Theorem 1.1An FPRAS for Cell-Bounded Contingency Tablespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	32	139
Continuous-weight invariant-projection counterexample`ContinuousCircleWeight`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	Theorem 1.1Invariant-projection counterexamples for every irrational rotationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	10	34
QMA-hardness of continuum Coulomb energy with binary charges`ContinuumCoulombHardness`Mathematical physics	QMA-hardness of continuum Coulomb energy	Mathematical physics	Theorem 1QMA-hardness of continuum Coulomb energy with unit nuclear chargespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	0	No	90	416
Temperature singularity over a density interval`ContinuumTransition`Probability and statistical mechanics	Continuum phase transitions for radial pair potentials	Probability and statistical mechanics	Theorem 1.1A continuum temperature singularity for a radial pair potentialpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	9	42
Conditional coordinate-sweep moment estimate`CoordinateSweeps`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 3.1Conditional coordinate sweeps and analytic transfercited in the Lean source; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	59	190
Regular trace smoothing and full-permutation mixing`CoordinateTrace`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Random-subspace tests and trace smoothing for coordinate sweepspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	52	227
Cotype–cotype equivalence with approximation property`Cotype`Functional analysis	The cotype–cotype conjecture under the approximation property	Functional analysis	Theorem 1.1The cotype–cotype conjecture under the approximation propertypossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	12	27
Coulomb Monge nonattainment with equality of infima`CoulombCounterexample`Partial differential equations	Nonattainment of the three-marginal Coulomb Monge problem	Partial differential equations	Theorem 1.1A counterexample to the Monge ansatz for the three-marginal Coulomb costpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	19	66
Generalized Coulomb ionization-energy asymptotics`CoulombIonization`Mathematical physics	The ionization and generalized ionization conjectures	Mathematical physics	Theorem 1.1Generalized ionization energies for full Coulomb atomspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	19	66
Asymptotic outer-electron radii of neutral atoms`CoulombRadii`Mathematical physics	The ionization and generalized ionization conjectures	Mathematical physics	Theorem 1.1Generalized outer-electron radii of neutral Coulomb atomspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	20	57
Courtade–Kumar inequality and attainment`CourtadeKumar`Theoretical computer science	The Courtade–Kumar and Hellinger conjectures	Theoretical computer science	Corollary 1.2Sharp binary-information contraction on the discrete cubepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	16	38
Optimal order for translative and lattice covering-density suprema`CoveringDensity`Convex and metric geometry	The optimal order of convex-body covering density	Convex and metric geometry	Theorem 1.1Translative covering densities of order n log npossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	22	63
No infinite cluster at the critical probability`CriticalPercolation`Probability and statistical mechanics	Critical percolation on every quasi-transitive graph	Probability and statistical mechanics	Theorem 1.1Critical bond and site percolation on the cubic latticepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	10	25
Equilibrium starts, covariance, and mixing lower bounds`CriticalSK`Probability and statistical mechanics	Critical SK autocorrelation processes and dynamics across the temperature transition	Probability and statistical mechanics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	28	84
Critical SK mixing bounds`CriticalSKMixing`Probability and statistical mechanics	Critical SK autocorrelation processes and dynamics across the temperature transition	Probability and statistical mechanics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	19	45
Critical honeycomb strip mass and displacement moment`CriticalStripMass`Probability and statistical mechanics	The three-quarter exponent for honeycomb self-avoiding walk	Probability and statistical mechanics	Theorem 1.1Critical strip-crossing mass on the honeycomb latticepossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	No	22	45
No infinite critical clusters on $\mathbb Z^3$`CriticalZ3`Probability and statistical mechanics	Critical percolation on every quasi-transitive graph	Probability and statistical mechanics	Theorem 1.1Critical bond and site percolation on the cubic latticepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	19	36
Complete sharp Crouzeix theorem on arbitrary Hilbert spaces`CrouzeixHilbert`Functional analysis	The complete Crouzeix conjecture	Functional analysis	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	24	106
Isoperimetric profile and all minimizers in the cubic flat three-torus`CubicTorus`Differential geometry	The isoperimetric profile of the cubic three-torus	Differential geometry	Theorem 1.1The Isoperimetric Conjecture for the Cubic Flat Three-Toruspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	18	47
Exact cycle–clique Ramsey numbers`CycleCliqueRamsey`Combinatorics	Cycle–clique Ramsey numbers	Combinatorics	Theorem 1.1Cycle–clique Ramsey numberspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	0	No	2	10
Linear cycle-and-edge decomposition`CycleDecomposition`Combinatorics	The Erdős–Gallai cycle-decomposition conjecture	Combinatorics	Theorem 1.1A linear cycle-and-edge decomposition of every graphpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	3	14
Cylinder-covering counterexamples and companion approximations`CylinderCovering`Convex and metric geometry	Cylinder coverings below the half-area bound	Convex and metric geometry	Theorem 1.1Finite triangular approximation of radial sweepsCorollary 1.2Finite triangular approximation of radial sweepspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	108	327
Exact asymptotic moduli and a Daugavet example`DaugavetModuli`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 1.1Exact asymptotic moduli in a Daugavet subspace of L1possible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	14	61
Stable self-similar blowup and positive-probability Gaussian blowup`DefocusingNLS`Partial differential equations	Stable blowup for the defocusing Schrödinger equation	Partial differential equations	Corollary 1.2Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the toruspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	No	37	216	3 definitions checked by name and type only
Rigidity of the Turing degrees`DegreeRigidity`Mathematical logic	Rigidity of the Turing degrees	Mathematical logic	Theorem 1.1Rigidity of the Turing degreespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	8	23
Deligne–Drinfeld main statement`DeligneDrinfeld`Number theory	The Deligne–Drinfeld conjecture	Number theory	Theorem 1.1The Deligne-Drinfeld conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	38	157
Homogeneous depth-five bounds for iterated matrix multiplication`DepthFive`Theoretical computer science	Homogeneous depth-five lower bounds for iterated matrix multiplication	Theoretical computer science	Theorem 1.1Homogeneous depth-five lower bounds for iterated matrix multiplicationpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	15	104
Depth-three circuit lower bound beyond every square-root constant`DepthThree`Theoretical computer science	Beyond the square-root exponent for depth-three circuits	Theoretical computer science	Theorem 1.1Beyond the Square-Root Exponent for Depth-Three Boolean Circuitspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	24	87
All-pairs diamond distortion bound`DiamondDistortion`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 1.1Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree spacepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	37	224
Mézard–Parisi variational equality for diluted even-arity spin glasses`DilutedSpin`Probability and statistical mechanics	The Mézard–Parisi formula for diluted spin glasses	Probability and statistical mechanics	Theorem 2.1The Mézard–Parisi formula for diluted spin glassespossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	23	98
PPT channel on dimension 21 whose square is not entanglement breaking`DimensionTenChannel`Mathematical physics	Entanglement without distillable secret key	Mathematical physics	Theorem 1.3Entanglement with zero distillable secret key in local dimension tenpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	9	24
Dimension-ten PPT pair with non-entanglement-breaking composition`DimensionTenPair`Mathematical physics	Entanglement without distillable secret key	Mathematical physics	Theorem 1.2Entanglement with zero distillable secret key in local dimension tenpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	25	86
Complete Crouzeix inequality and sharpness`DirectCrouzeix`Functional analysis	The complete Crouzeix conjecture	Functional analysis	Theorem 3.2A direct proof of the complete Crouzeix inequalitypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	5	22
Constant-factor hardness of directed feedback vertex set`DirectedFeedback`Theoretical computer science	The Unique Games Conjecture and optimal approximation thresholds	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	0	No	15	52
Directional transience implies ballisticity`DirectionalBallisticity`Probability and statistical mechanics	Directional zero–one laws beyond iid environments and iid ballisticity	Probability and statistical mechanics	Theorem 1.1Directional transience implies ballisticitypossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	21	69
Directional zero–one law under strict ellipticity`DirectionalWalk`Probability and statistical mechanics	Directional zero–one laws beyond iid environments and iid ballisticity	Probability and statistical mechanics	Theorem 1.1A directional zero–one law under strict ellipticitypossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	17	65
Dirichlet $L$-function $7/8$ bound`DirichletSevenEighths`Number theory	The quasi-Riemann hypothesis	Number theory	Theorem 1.1The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane $\Re s\gt 7/8$possible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	0	5
Uniformly discrete Lipschitz-free space with AP but no BAP`DiscreteLipschitzFree`Functional analysis	A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces	Functional analysis	Theorem 1.1A uniformly discrete counterexample to bounded approximation in Lipschitz-free spacespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	19	118
Endpoint gradient bound for the centered disk maximal operator`DiskMaximal`Real and complex analysis	Endpoint Sobolev regularity of centered disk averages	Real and complex analysis	Theorem 1.1An Endpoint Gradient Bound for the Centered Disk Maximal Operatorpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	9	27
Separable nonunitarizable witnesses for countable nonamenable groups`Dixmier`Group theory	Amenability, unitarizability, and strong Ulam stability	Group theory	Theorem 1.1Unitarizability implies amenability for discrete groupspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	5	24
Unitarizability for all discrete groups`DixmierAllDiscrete`Group theory	Amenability, unitarizability, and strong Ulam stability	Group theory	Theorem 1.1Unitarizability implies amenability for discrete groupspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	5	28
Doubling Hilbert subset without finite-dimensional embedding`DoublingHilbert`Convex and metric geometry	Compact counterexamples to bi-Lipschitz dimension reduction	Convex and metric geometry	Theorem 1A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	3	14
Equidistribution of prime-degree torus packets`DukePrimeDegree`Number theory	Torus-packet equidistribution in prime, quartic, and sextic degrees	Number theory	Theorem 1.1Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Typepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	1	No	32	164
Complete-domain Dutta multiplicity comparison`DuttaDomain`Algebra	Lech’s multiplicity conjecture	Algebra	Corollary 5.4Lech’s multiplicity conjecturepossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	No	10	39
Positive-measure avoidance of every affine dyadic sequence`DyadicAvoidance`Real and complex analysis	The geometric case of the Erdős similarity conjecture	Real and complex analysis	Theorem 1.1The dyadic case of the Erdős similarity conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	1	9
Almost-linear randomized approximation of edit distance`EditApproximation`Theoretical computer science	Almost-linear approximation of edit distance	Theoretical computer science	Theorem 1.1An Almost-Linear Approximation Scheme for Edit Distancepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	1,212	16,221
Matching exponential-scale bounds for edit-distance distortion`EditDistance`Convex and metric geometry	The sharp exponential scale of edit-distance distortion	Convex and metric geometry	Theorem 1.1Edit Distance in l1: Matching Bounds up to Constants in the Exponentpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	12	36
Short expansions, counting, and prescribed denominators`EgyptianFractions`Number theory	Short Egyptian fractions	Number theory	Corollary 1.3Short Egyptian fractionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	11	89
Counterexample to the Eilenberg–Ganea conjecture`EilenbergGanea`Group theory	A finitely generated Eilenberg–Ganea counterexample	Group theory	Theorem 1.1A finitely generated counterexample to the Eilenberg–Ganea conjecturepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	25	82
Classification of positively curved Einstein four-manifolds`EinsteinFour`Differential geometry	Nonnegative-curvature Einstein classification and an L² topological gap	Differential geometry	Theorem 1.1Positively curved Einstein four-manifoldspossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	1	No	32	128
Global uniqueness of smooth isotropic Lamé moduli`ElasticityUniqueness`Partial differential equations	Global uniqueness in smooth isotropic elasticity	Partial differential equations	Theorem 1.1Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problempossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	23	64
Elementary positivity for natural unit interval graphs`ElementaryPositivity`Combinatorics	Shareshian–Wachs elementary positivity	Combinatorics	Theorem 1.1Elementary positivity of chromatic quasisymmetric functionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	12	37	One definition checked by name and type only
Threshold parallel repetition for entangled games`EntangledGames`Mathematical physics	Threshold repetition for entangled games	Mathematical physics	Theorem 1.1Threshold parallel repetition for finite-dimensional entangled gamespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	10	55
Entropy photon-number inequality for finite-energy bosonic inputs`EntropyPhotonNumber`Mathematical physics	The entropy photon-number inequality	Mathematical physics	Theorem 1.1The entropy photon-number inequalitypossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	17	50
Erdős’s reciprocal-sum arithmetic-progression conjecture`ErdosReciprocal`Combinatorics	Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds	Combinatorics	Corollary 1.2Quasipolynomial Bounds for Arithmetic Progressionspossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	3	9
No proper five-coloring`EuclideanFiveColor`Combinatorics	The Euclidean plane cannot be colored with five colors	Combinatorics	Theorem 1.1The Euclidean plane is not five-colorablepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	1	4	One definition checked by name and type only
Tensor-field classification of Ramsey configurations`EuclideanRamsey`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Theorem 1.1A classification of finite Euclidean Ramsey configurationspossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	10	29
Ramsey property for at most five circle points`EuclideanRamseyCircle`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Corollary 7.4A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	3	11
Nine-point non-Ramsey circle configuration`EuclideanRamseyNine`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Proposition 7.6A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	4	16
Quadratic-independence criterion for spherical configurations`EuclideanRamseyQuadratic`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Proposition 7.3A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	7	23
Cosphericity of Ramsey configurations`EuclideanRamseySpherical`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Proposition 2.4A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	3	11
Ramsey property for subsets of finite transitive configurations`EuclideanRamseyTransitive`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Corollary 7.2A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	3	14
Classification of positive even Barker lengths`EvenBarker`Combinatorics	The circulant Hadamard and Barker-sequence conjectures	Combinatorics	Corollary 1.2The circulant Hadamard conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	No	3	9
Subsequential savings for exact Fourier circuits`ExactFourier`Theoretical computer science	Exact Fourier transforms below $n\log n$	Theoretical computer science	Proposition 3.4Finite tensor savings and exact Fourier circuitspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	10	34
Fixed-amplification pure infiniteness for exact algebras`ExactInfiniteness`Operator algebras	Weak pure infiniteness and Cuntz-algebra absorption	Operator algebras	Theorem 1.2Weak pure infiniteness and O-infinity absorptionpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	1	No	23	116
Exact quantum factoring over a fixed finite gate set`ExactQuantumFactoring`Mathematical physics	Exact quantum factoring over a fixed finite gate set	Mathematical physics	Theorem 1.1Exact quantum factoring over a fixed finite gate setcited in the Lean source; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	27	93
Brownian continuum-random-tree limit for finite FK maps`FKCRT`Probability and statistical mechanics	The geometric phase diagram, diffusion, and spectra of random planar maps	Probability and statistical mechanics	Theorem 1.1Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above fourpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	34	116
Single generation of separable-predual $\mathrm{II}_1$ factors`FactorGeneration`Operator algebras	The generator problem for finite factors	Operator algebras	Theorem 1.1Relative generation and the generator problem for finite factorspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	5	23
Falconer distance theorem in every dimension`FalconerAllDimensions`Real and complex analysis	The Falconer distance conjecture	Real and complex analysis	Theorem 1.1The Falconer distance conjecture in all dimensionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	0	5
Optimality of the Euclidean filling coefficient`FillingCoefficient`Differential geometry	Sharp Cartan–Hadamard isoperimetry and rigidity	Differential geometry	Theorem 1.1Sharp integral fillings in CAT(0) spacespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	23	83
Finite-circle obstructions and histogram embeddings for edit distance`FiniteCircle`Convex and metric geometry	The sharp exponential scale of edit-distance distortion	Convex and metric geometry	Theorem 1.1Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distancepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	42	173
Colored-graph criterion for finite congruence lattices`FiniteCongruenceGraph`Algebra	Finite lattice representation and undecidability	Algebra	Theorem 1.1Finite congruence lattices: characterization and undecidabilitypossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	No	10	38
Finite separation of microstates and nonmicrostates free entropy`FiniteEntropySeparation`Operator algebras	Two notions of free entropy differ even when both are finite	Operator algebras	Theorem 1.1A finite-entropy separation of microstates and nonmicrostates free entropypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	19	85
Finite-factor invariant-projection counterexample`FiniteFactor`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	Theorem A.1Invariant-projection counterexamples for every irrational rotationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	5	21
Left/right finitistic-dimension asymmetry`FinitisticAsymmetry`Algebra	A counterexample to finitistic-dimension finiteness	Algebra	Corollary 1.2An algebra of infinite little finitistic dimensionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	3	21
Limiting satisfiability threshold for every fixed $k\ge3$`FixedClauseThreshold`Probability and statistical mechanics	Limiting random SAT thresholds, sharp variance and computability	Probability and statistical mechanics	Theorem 1.1A Limiting Satisfiability Threshold for Every Fixed Clause Sizepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	8	24
Effective finite computation detected by a fixed particle`ForcedNavierStokesComputation`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	Theorem 5.1Computation under Rapidly Vanishing Navier–Stokes Forcingpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	50	170
Reflexive tree space, midpoint modulus, and diamond distortion`ForestSpace`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 1.1Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree spacepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	43	324
One rational matrix tuple hitting all bounded-size noncommutative formulas`FormulaHitting`Theoretical computer science	Uniform black-box noncommutative identity testing across characteristics	Theoretical computer science	Theorem 1.1One Rational Matrix Hitting Point for Noncommutative Formulaspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	10	40
Quadratic stabilization of the canonical Foulkes–Howe map`FoulkesHowe`Algebra	Foulkes' conjecture for sixth powers and quadratic stabilization	Algebra	Theorem 1Quadratic stabilization of the canonical Foulkes–Howe mappossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	6	27
Strict four-row permanent inequality near the uniform law`FourRowPermanent`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1A strict four-row permanent inequality and permutation momentspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	9	21
Almost-everywhere convergence of full symmetric Fourier partial sums`FourierLLogL`Real and complex analysis	The $L\log L$ Fourier-convergence conjecture	Real and complex analysis	Theorem 1.1Almost-everywhere Fourier convergence in L log Lpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	1	13
Factor-of-IID threshold for the free Ising model`FreeIsing`Probability and statistical mechanics	The exact factor-of-IID threshold for free Ising spins on trees	Probability and statistical mechanics	Theorem 1.1The sharp factor-of-IID threshold for the free Ising model on regular treespossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	16	61
A universal IID factor for the free uniform spanning forest`FreeUniformSpanningForest`Probability and statistical mechanics	The free uniform spanning forest is a factor of IID	Probability and statistical mechanics	Theorem 1.1The free uniform spanning forest is a factor of IIDpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	26	106
Differentiability for every positive Gamma edge-weight law`GammaPassage`Probability and statistical mechanics	Planar first-passage geometry and the absence of bigeodesics	Probability and statistical mechanics	Theorem 1.1Strict convexity and differentiability of the planar exponential first-passage limit shapepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	17	62
Finite-entropy localization and regularization bounds`GaussianFiniteEntropy`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	50	144
Information growth under repeated exact Gaussian observations`GaussianInformation`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	Theorem 3.2Localization costs and information growth for exact Gaussian observationspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	53	144
Uniform bounds for bounded-step Gaussian-prime walks`GaussianMoat`Number theory	Uniformly bounded components of Gaussian-prime graphs	Number theory	Theorem 1.1Bounded-Step Walks on Gaussian Primespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	5	26
Gaussian propeller bound and attainment`GaussianPropeller`Convex and metric geometry	The Gaussian propeller conjecture in every dimension	Convex and metric geometry	Theorem 1.1The Gaussian propeller bound in every dimensionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	8	22
Gaussian replacement and information bounds`GaussianReplacement`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	64	428
General Mahler inequality and simplex equality cases`GeneralMahler`Convex and metric geometry	The Mahler conjectures, functional inequalities and polar-product symplectic width	Convex and metric geometry	Corollary 6.2The symmetric Mahler conjecture and its equality casespossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	No	3	15
Uniform generalized star-height bound of three`GeneralizedStarHeight`Theoretical computer science	Generalized star height at most three	Theoretical computer science	Theorem 1.1Finite Monoid Computations and a Uniform Generalized Star-Height Boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	4	26
Average sensitivity of polynomial threshold functions`GotsmanLinial`Theoretical computer science	Average sensitivity of polynomial threshold functions	Theoretical computer science	Theorem 1Average sensitivity of polynomial threshold functionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	10	28
Twelve-point spherical non-Ramsey example`GrahamSpherical`Combinatorics	Classification of finite Euclidean Ramsey configurations	Combinatorics	Proposition 7.6A classification of finite Euclidean Ramsey configurationspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	12	28
Elementary-expansion weak equivalence`GrothendieckElementaryExpansion`Topology	The Grothendieck homotopy hypothesis	Topology	Theorem 1.1The Grothendieck homotopy hypothesis via elementary expansionspossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	76	344
Group-ring determinant counterexample`GroupRingDeterminant`Algebra	A torsion-free group algebra that is not directly finite	Algebra	Theorem 1.1A Counterexample to the Group-Ring Determinant Conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	7	29
Cube-fiber cancellation for order-six Hadamard row ratios`HadamardCubeFiber`Mathematical physics	Exactly three mutually unbiased bases in dimension six	Mathematical physics	Proposition 4.1Exact Fourier certificates for complex Hadamard matrices of order sixpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	3	No	7	17
Arbitrarily large counterexamples to Hadwiger’s conjecture`HadwigerCounterexample`Combinatorics	Graph coloring, clique minors, and Colin de Verdière invariants	Combinatorics	Corollary 1.2A counterexample to Hadwiger’s conjectureTheorem 1.1A counterexample to Hadwiger’s conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	4	28
Power-saving bounds for halving pairs and level switches`HalvingLines`Combinatorics	Power savings for planar halving lines and k-sets	Combinatorics	Theorem 1.1A power saving for planar halving linespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	9	37
Uniform ground-state condensation in the dilute hard-sphere gas`HardSphere`Mathematical physics	Positive-temperature Bose–Einstein condensation and exact quantum depletion	Mathematical physics	Theorem 1.1Ground-state condensation in the dilute hard-sphere gaspossible match from catalogue wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	31	301
Contractibility of the Salvetti cover`HarmonicArtin`Group theory	Classifying spaces and geometric obstructions for Artin groups	Group theory	Corollary 1.3Parabolic intersections in Artin groupspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	13	36
Counterexample to harmonic dimension comparison`HarmonicGrowth`Differential geometry	Failure of integer-degree harmonic dimension comparison	Differential geometry	Theorem 1.1A counterexample to integer-degree harmonic dimension comparisonpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	19	58	Declares an axiom
Finite-order Hecke $L$-function $7/8$ bound`HeckeSevenEighths`Number theory	The quasi-Riemann hypothesis	Number theory	Theorem 1.1The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane $\Re s\gt 7/8$possible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	23	185
Power improvement for the smallest Heilbronn triangle`HeilbronnTriangle`Combinatorics	A power improvement in the Heilbronn triangle lower bound	Combinatorics	Theorem 1.1A power improvement in the Heilbronn triangle lower boundpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	2	No	12	40
Low-temperature spontaneous magnetization for every positive spin`Heisenberg`Mathematical physics	Bloch’s law, its lattice correction, and the spherical magnetization law	Mathematical physics	Theorem 1.1Spontaneous magnetization in the quantum Heisenberg ferromagnetpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	31	169
Subcritical Hénon–Lane–Emden nonexistence`HenonEmden`Partial differential equations	The Lane–Emden and Hénon–Lane–Emden conjectures	Partial differential equations	Corollary 1.2The Subcritical Hénon–Lane–Emden Conjecturepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	3	18
Numerical-range geometry and finite-compression support`HilbertCrouzeix`Functional analysis	The complete Crouzeix conjecture	Functional analysis	Corollary 6.3The complete Crouzeix theorem: optimal similarity and a common positive boundary representationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	26	92
Finiteness of critical bridge mass and first length moments`HoneycombBridgeFiniteness`Probability and statistical mechanics	The three-quarter exponent for honeycomb self-avoiding walk	Probability and statistical mechanics	Theorem 1.1Polynomial vacuum representations and bridge mass for honeycomb walkspossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	No	13	44
Strict honeycomb bridge mass of order $(1+h)^{-1/4}$`HoneycombBridgeMassSupport`Probability and statistical mechanics	The three-quarter exponent for honeycomb self-avoiding walk	Probability and statistical mechanics	no confident match	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	Yes	15	46
Existence of the honeycomb free-energy limit`HoneycombFreeEnergy`Probability and statistical mechanics	The three-quarter exponent for honeycomb self-avoiding walk	Probability and statistical mechanics	Theorem 1.1Critical honeycomb chords with prescribed boundary endpointspossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	No	15	39
Strict hot spots and absence of interior critical points`HotSpots`Partial differential equations	The hot spots conjecture for simply connected planar domains	Partial differential equations	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	8	34
Nonspectrahedral hyperbolicity cone`HyperbolicCones`Convex and metric geometry	Hyperbolicity cones without semidefinite lifts	Convex and metric geometry	Proposition 4.1A nonspectrahedral hyperbolicity conepossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	15	48
Hyperbolic group with no geometric CAT(0) action`HyperbolicObstruction`Group theory	A hyperbolic group without a geometric CAT(0) action	Group theory	Theorem 1.1A hyperbolic group with no geometric CAT(0) actionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	23	87
Quasinilpotent operator with a transitive commutant`HyperinvariantSubspaces`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	Corollary 1.2Backward intertwiners and a transitive commutantpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	4	16
Independent-product spaces and positive midpoint moduli`IndependentProducts`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 1.1Independent products in real L1: asymptotic midpoint convexity without AUC renormingspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	17	66
Independent-set hardness in three-colorable graphs`IndependentSets`Theoretical computer science	Hardness of coloring three-colorable graphs	Theoretical computer science	Theorem 1.1Hardness of finding large independent sets in three-colorable graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	15	50
Individual proper infiniteness implies strong pure infiniteness`IndividualStrongInfiniteness`Operator algebras	Weak pure infiniteness and Cuntz-algebra absorption	Operator algebras	Theorem 1.2Weak pure infiniteness and O-infinity absorptionpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	42	248
Infinite matroid packing/covering counterexample`InfiniteMatroid`Combinatorics	Counterexamples to infinite matroid intersection and packing/covering	Combinatorics	Theorem 1.1A Counterexample to the Infinite Matroid Packing/Covering Conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	4	20
Partitional intersection, covering, and packing counterexamples`InfiniteMatroidCorollaries`Combinatorics	Counterexamples to infinite matroid intersection and packing/covering	Combinatorics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	19	98
Isomorphism of all interpolated free group factors`InterpolatedFactors`Operator algebras	Isomorphism of the free group factors	Operator algebras	Corollary 7.1An isomorphism of the free group factorspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	No	41	139
Pressure and ground-state limits for invariant Ising models`InvariantIsing`Probability and statistical mechanics	All-temperature pressure of orthogonally invariant Ising spin glasses	Probability and statistical mechanics	Theorem 1.1All-temperature pressure for orthogonally invariant Ising spin glassespossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	66	389
Invariant-projection counterexamples for every irrational rotation`IrrationalRotation`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	Theorem A.1Invariant-projection counterexamples for every irrational rotationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	114	551
Ergodicity of triangular billiards with an irrational angle`IrrationalTriangleBilliard`Dynamical systems and ergodic theory	Weak mixing of triangular billiards with an irrational angle	Dynamical systems and ergodic theory	Theorem 1Ergodicity of triangular billiards with an irrational anglepossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	16	62
Finiteness of the Ising-perceptron variational value`IsingFiniteness`Probability and statistical mechanics	Perceptron free energies and microscopic jamming exponents	Probability and statistical mechanics	Theorem 2.3The free energy of the Ising random perceptronpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	13	54
Smooth local isometric-immersion obstruction`IsometricImmersion`Differential geometry	A smooth surface metric with no local isometric immersion in ℝ³	Differential geometry	Theorem A (unnumbered)A Smooth Metric with No Local Isometric Immersion into Three-Spacepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	5	27
Quadratic Jacobsthal bound`Jacobsthal`Number theory	A quadratic bound for Jacobsthal’s function	Number theory	Theorem 1.1A quadratic bound for Jacobsthal’s functionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	2	8
Jacobsthal bound with an iterated-logarithm saving`JacobsthalImproved`Number theory	A quadratic bound for Jacobsthal’s function	Number theory	Theorem 1.1A quadratic bound for Jacobsthal’s functionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	2	9
Joint Dickman law and equal ordering densities for consecutive integers`JointDickman`Number theory	Independent largest prime factors of consecutive integers	Number theory	Theorem 1.1The joint Dickman law for consecutive integerspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	6	25
Combinatorial invariance of Kazhdan–Lusztig polynomials`KLInvariance`Combinatorics	Combinatorial invariance of Kazhdan–Lusztig polynomials	Combinatorics	Theorem 1.1Combinatorial invariance of Kazhdan–Lusztig polynomialspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	9	56
Randomized metric $k$-median approximation below two`KMedianRecovery`Theoretical computer science	The metric k-median approximation threshold and recovery	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	18	70
Exact-budget recovery from accurate distinct cluster proxies`KMedianRefinedRecovery`Theoretical computer science	The metric k-median approximation threshold and recovery	Theoretical computer science	Theorem 1.1Single-exponential recovery and bounded-price strictness for metric k-medianpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	27	112
Exact approximation threshold under $P\ne NP$`KMedianThreshold`Theoretical computer science	The metric k-median approximation threshold and recovery	Theoretical computer science	Corollary 1.2The approximation threshold for metric k-medianpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	19	63
Squared-logarithmic randomized $k$-server on arbitrary metrics`KServer`Theoretical computer science	Optimal-order randomized k-server on arbitrary metrics	Theoretical computer science	Theorem 1.1Squared-logarithmic randomized k-server on arbitrary metricspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	9	42	9 definitions checked by name and type only
Bounded primitives for all Hochschild cocycles of degree at least two`KadisonRingrose`Operator algebras	The Kadison–Ringrose cohomology conjecture	Operator algebras	Proposition 1.2Vanishing of higher bounded Hochschild cohomologypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	3	18
Kadison’s similarity theorem and uniform hyperreflexivity`KadisonSimilarity`Operator algebras	Kadison’s similarity conjecture	Operator algebras	Theorem 1.1Kadison’s similarity theorem through uniform derivation estimatescited in the Lean source; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	20	62
Universal-cover product splitting`KahlerSplitting`Algebraic and complex geometry	Tangent splittings and product decompositions	Algebraic and complex geometry	Theorem 1.1Universal-cover splitting for compact Kähler manifoldspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	17	98
Characteristic-two direct-finiteness counterexample`KaplanskyDirectFiniteness`Algebra	A torsion-free group algebra that is not directly finite	Algebra	Theorem 1.1A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Characteristic Twopossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	1	6
Finitely presented characteristic-two counterexample`KaplanskyFinitelyPresented`Algebra	A torsion-free group algebra that is not directly finite	Algebra	Theorem 1.1A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Characteristic Twopossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	0	6
Nonadditive normalized $2$-quasitraces`KaplanskyQuasitrace`Operator algebras	Kaplansky’s quasitrace conjecture and failure of tensor-product stable finiteness	Operator algebras	Theorem 1.1A counterexample to Kaplansky’s quasitrace conjecture and failure of tensor-product stable finitenesspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	7	27
Tensor-product failure of stable finiteness and quasitrace consequences`KaplanskyStableFiniteness`Operator algebras	Kaplansky’s quasitrace conjecture and failure of tensor-product stable finiteness	Operator algebras	Corollary 1.2A counterexample to Kaplansky’s quasitrace conjecture and failure of tensor-product stable finitenesspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	26	125
Coefficient-group injectivity for unimodular one-relator quotients`Kervaire`Group theory	Nonsingular systems of equations over arbitrary groups	Group theory	Theorem 1.1The Kervaire theorem for groupspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	7	16
Removable-boundary rigidity and the circle-domain theorem`KoebeCircleDomains`Real and complex analysis	Koebe’s circle-domain conjecture	Real and complex analysis	Theorem 1.1Removable Boundaries and Rigidity of Circle Domainspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	13	42
Uniform Laughlin $V_1$ spectral gap`Laughlin`Mathematical physics	Uniform Laughlin gap and stability under bounded scalar disorder	Mathematical physics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	13	43
Uniform Fock-space spectral-gap inequality`LaughlinFock`Mathematical physics	Uniform Laughlin gap and stability under bounded scalar disorder	Mathematical physics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	1	No	11	34
Uniform unperturbed spherical Laughlin gap inequality`LaughlinGap`Mathematical physics	Uniform Laughlin gap and stability under bounded scalar disorder	Mathematical physics	Theorem 1.1Uniform Stability of the Spherical Laughlin Gappossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	13	44
Planar spectral-gap inequality`LaughlinPlanar`Mathematical physics	Uniform Laughlin gap and stability under bounded scalar disorder	Mathematical physics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	17	44
Sharp one-dimensional Lieb–Thirring inequality`LiebThirring`Mathematical physics	Sharp finite-matrix Lieb–Thirring inequalities and all equality cases	Mathematical physics	Theorem 1.1Sharp one-dimensional Lieb–Thirring constantspossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	15	51
Bi-Lipschitz equivalent nonisomorphic Banach spaces`LipschitzEquivalence`Functional analysis	Lipschitz equivalent Banach spaces need not be linearly isomorphic	Functional analysis	Theorem 1.1Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphicpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	5	25
Uniform short Hilbert-transform bounds for Lipschitz directions`LipschitzHilbert`Real and complex analysis	Hilbert transforms along Lipschitz directions	Real and complex analysis	Theorem 1.1A uniform Hilbert transform estimate for Lipschitz directionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	8	46
Linear list-coloring bound in the Hadwiger number`ListHadwiger`Combinatorics	Graph coloring, clique minors, and Colin de Verdière invariants	Combinatorics	Theorem 1.1A linear list-coloring bound in terms of the Hadwiger numberpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	6	19
Infinite little finitistic dimension`LittleFinitistic`Algebra	A counterexample to finitistic-dimension finiteness	Algebra	Corollary 1.2An algebra of infinite little finitistic dimensionpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	1	10
Finite-exponent flatness of one all-length Littlewood family`LittlewoodFiniteFlatness`Real and complex analysis	Real ultraflat Littlewood polynomials and unbounded binary merit factors	Real and complex analysis	Theorem 1.1Asymptotically minimal maxima of real Littlewood polynomialspossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	3	19
Logarithmic Brunn–Minkowski inequality`LogBrunnMinkowski`Convex and metric geometry	Logarithmic and L_p Brunn–Minkowski inequalities and the B-conjecture	Convex and metric geometry	Theorem 1.1The logarithmic Brunn–Minkowski conjecturepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	6	18
Subpolynomial query complexity for log-concave sampling`LogConcaveQuery`Theoretical computer science	Subpolynomial query complexity for log-concave sampling	Theoretical computer science	Theorem 1.1Subpolynomial query complexity for well-conditioned log-concave samplingpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	16	55
Logarithmic Kodaira additivity in the negative-fiber branch`LogKodairaFiberNegative`Algebraic and complex geometry	Iitaka subadditivity, variation, and logarithmic additivity	Algebraic and complex geometry	Corollary 1.2The reverse logarithmic Kodaira inequality and additivitypossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	No	34	149
Exact equality of deterministic and randomized logarithmic space`LogspaceEquality`Theoretical computer science	Exact derandomization of logarithmic space: $\mathsf L=\mathsf{RL}=\mathsf{BPL}$	Theoretical computer science	Theorem 1.2Exact derandomization of logarithmic space: L = RL = BPLpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	25	100	20 definitions checked by name and type only
Order-six Hadamard Fourier vanishing and a five-basis upper bound`MUBSix`Mathematical physics	Exactly three mutually unbiased bases in dimension six	Mathematical physics	Theorem 1.1Exact Fourier certificates for complex Hadamard matrices of order sixpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	1	No	16	35
Symmetric Mahler inequality`MahlerConjecture`Convex and metric geometry	The Mahler conjectures, functional inequalities and polar-product symplectic width	Convex and metric geometry	no confident match	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	1	8
Nontrivial Markov type and superreflexivity`MarkovType`Functional analysis	Markov type characterizes superreflexivity	Functional analysis	Theorem 1.1Nontrivial Markov Type Forces Superreflexivitypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	10	41
Global boundedness and persistence for weakly reversible mass-action systems`MassAction`Dynamical systems and ergodic theory	Classwise permanence for weakly reversible mass-action systems	Dynamical systems and ergodic theory	Theorem 1.1Boundedness and persistence of weakly reversible mass-action systemspossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	8	38
Superpolynomial lower bound for affine semidefinite lifts`MatchingAffineLift`Theoretical computer science	Exponential semidefinite complexity of perfect matching	Theoretical computer science	Corollary 1.2Exponential PSD rank of positively shifted matching matricespossible match from catalogue wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	2	No	6	19
Perfect-matching entropy bound`MatchingEntropy`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	Proposition 5.2Entropy and Face Dimension of the Perfect-Matching Polytopepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	13	32
Refined pointwise perfect-matching entropy bounds`MatchingEntropyBounds`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	Theorem 1.1Entropy and Face Dimension of the Perfect-Matching Polytopepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	14	35
Randomized approximation of the perfect-matching count`MatchingFPRAS`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	Theorem 1.1A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	18	64
Superpolynomial PSD rank for the perfect-matching slack matrix`MatchingPSD`Theoretical computer science	Exponential semidefinite complexity of perfect matching	Theoretical computer science	Corollary A.4Exponential PSD rank of positively shifted matching matricespossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	3	No	11	30
Matrix-multiplication exponent over every field`MatrixFields`Theoretical computer science	Matrix multiplication with exponent at most 9/4	Theoretical computer science	Theorem 1.1Staggered extraction for exact matrix multiplication over every fieldpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	14	55
Complex square, dual, and rectangular exponent bounds`MatrixMultiplication`Theoretical computer science	Matrix multiplication with exponent at most 9/4	Theoretical computer science	Theorem 1.1Complex Matrix Multiplication Below 2.258 and Rectangular Boundspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	18	69
Failure of polynomial removal for ordered binary matrices`MatrixRemoval`Combinatorics	Polynomial removal fails for ordered binary matrices	Combinatorics	Theorem 1.1Polynomial removal fails for ordered binary matricespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	11	52
One-sample matroid prophet inequality against an almighty adversary`MatroidProphet`Theoretical computer science	One-sample matroid prophet inequalities against an almighty adversary	Theoretical computer science	Theorem 1.1One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversarypossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	16	58
Hidden-vector matroid selection with worst-order guarantee`MatroidSecretary`Theoretical computer science	One-sample matroid prophet inequalities against an almighty adversary	Theoretical computer science	Theorem 1.1One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversarypossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	31	134
Eventual maximal Seshadri constants`MaximalSeshadriConstants`Algebraic and complex geometry	Nagata’s conjecture and maximal Seshadri constants	Algebraic and complex geometry	Theorem 1.1Maximal Seshadri constants on arbitrary polarized surfacespossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	44	223
Projection estimates and memory–precision bounds`MemoryPrecision`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	66	688
Counterexample to metric-entropy duality`MetricEntropyDuality`Functional analysis	A counterexample to metric-entropy duality	Functional analysis	Theorem 1.1Counterexamples to the duality conjecture for metric entropypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	8	29
Deterministic metric $k$-median approximation at the threshold`MetricKMedian`Theoretical computer science	The metric k-median approximation threshold and recovery	Theoretical computer science	Theorem 1.1The approximation threshold for metric k-medianpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	9	42
Midpoint-lens tail estimate`MidpointLenses`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 1.1Midpoint lenses in segment spacespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	35	275
Arbitrary constant-factor hardness of Min-UnCut`MinUncut`Theoretical computer science	The Unique Games Conjecture and optimal approximation thresholds	Theoretical computer science	Theorem 1.1Constant-factor hardness of Min-UnCutpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	0	No	18	65
Nagata’s conjecture`Nagata`Algebraic and complex geometry	Nagata’s conjecture and maximal Seshadri constants	Algebraic and complex geometry	Theorem 1.1Nagata’s conjecture for plane curvespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	29	233
Counterexample to Naimark’s problem in ZFC`Naimark`Operator algebras	A ZFC counterexample to Naimark’s problem	Operator algebras	Theorem 1.1A counterexample to Naimark’s problem in ZFCpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	7	34	7 definitions checked by name and type only
Rapidly decaying alternating-coordinate memory`NavierStokesAlternating`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	Theorem 1.1Velocity-Field Detection of Computation in Forced Navier–Stokes Flowspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	56	173
Pointwise and integral velocity-field detection of halting`NavierStokesVelocity`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	Theorem 1.1Velocity-Field Detection of Computation in Forced Navier–Stokes Flowspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	196	607
Sharp upper bound for nodal length on smooth surfaces`NodalLength`Differential geometry	Yau’s nodal bounds: surfaces and higher dimensions	Differential geometry	Theorem 1.1Sharp nodal length on smooth surfacespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	No	8	35
Subquadratic and fixed-quadratic memory–precision lower bounds`NoiselessRegression`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	Proposition 7.1Subsphere methods for memory-sample lower bounds in noiseless Gaussian regressionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	19	82
Obstruction to nuclear norm-ultrapower embeddings`NuclearUltrapower`Operator algebras	Kirchberg’s $\mathcal O_2$ norm-ultrapower embedding problem	Operator algebras	Theorem 1.1An explicit obstruction to nuclear norm-ultrapower embeddingspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	29	133
Row–column overlap on occupied boards`OccupiedOverlap`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 5.1Row–column symmetry and contraction of coordinate sweepscited in the Lean source; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	33	160	5 definitions checked by name and type only
Prescribed odd-characteristic counterexample`OddKaplansky`Algebra	A torsion-free group algebra that is not directly finite	Algebra	Theorem 1.1A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Odd Characteristicpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	4	16
Time-capped and unknown-time one-tape simulation in two-fifths-power space`OneTapeSpace`Theoretical computer science	One-tape time simulation in two-fifths-power space	Theoretical computer science	Theorem 1Simulating One-Tape Time in Two-Fifths-Power Spacepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	53	167
Exponential deterministic state lower bound for liveness`OneWayLiveness`Theoretical computer science	Exponential state costs for two-way automata	Theoretical computer science	Theorem 1.1An exponential two-way deterministic state lower bound for one-way livenesspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	22	70
Optimal Max-Cut hardness gap`OptimalMaxCut`Theoretical computer science	The Unique Games Conjecture and optimal approximation thresholds	Theoretical computer science	Theorem 1.1A Direct Proof of Optimal Max-Cut Hardnesspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	24	94
Ordinary Elliott cancellation under uniform nonpretentiousness`OrdinaryElliott`Number theory	Ordinary two-point correlations and the corrected Elliott conjecture	Number theory	Theorem 1.2Ordinary two-point correlations of multiplicative functionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	6	23
Ordinary Liouville and multiplicative two-point correlations`OrdinaryTwoPointCorrelations`Number theory	Ordinary two-point correlations and the corrected Elliott conjecture	Number theory	Theorem 1.1Ordinary two-point correlations of multiplicative functionspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	9	39
Ostmann’s inverse Goldbach theorem and the infinite-summands case`OstmannComplete`Number theory	Ostmann’s inverse Goldbach conjecture	Number theory	Theorem 2.3The additive indecomposability of the primespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	5	20
Additive indecomposability of the primes up to finite changes`OstmannPrimes`Number theory	Ostmann’s inverse Goldbach conjecture	Number theory	Theorem 1.1The additive indecomposability of the primespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	0	3
Parity-lift characterization of Weisfeiler–Leman equivalence`ParityLifts`Theoretical computer science	The computational complexity of Weisfeiler–Leman refinement	Theoretical computer science	Theorem 1.2Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalencepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	37	154
Fourier bounds from complementary coset caps`PartialPermutation`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	17	70
Relative consistency of the Partition Principle with ordinal Choice and failure of Choice`PartitionConsistency`Mathematical logic	The Partition Principle does not imply Choice	Mathematical logic	Theorem 1.2The Partition Principle does not imply Choicepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	47	200
Partition Principle without Choice from a ground model`PartitionPrinciple`Mathematical logic	The Partition Principle does not imply Choice	Mathematical logic	Theorem 3.3The Partition Principle does not imply Choicepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	1	Yes	50	155
Patterson first moment and angular cancellation`PattersonFirstMoment`Number theory	Patterson’s first moment for cubic Gauss sums	Number theory	Theorem 1.1An unconditional first moment for cubic Gauss sumspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	21	54
Variational formula for spherical-perceptron pressure`PerceptronFreeEnergy`Probability and statistical mechanics	Perceptron free energies and microscopic jamming exponents	Probability and statistical mechanics	Theorem 8.5The free energy of the Ising random perceptronpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	27	71
Perfect-completeness reduction for 2-to-1 games`PerfectCompleteness`Theoretical computer science	Perfect completeness for 2-to-1 games	Theoretical computer science	Theorem 1.1Perfect completeness for 2-to-1 gamespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	30	101
Infinite finitely presented periodic group`PeriodicGroup`Group theory	An infinite finitely presented residually finite 2-group and a finitely presented nil algebra	Group theory	Theorem 1.1An infinite finitely presented periodic grouppossible match from catalogue wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	9	31
Aperiodic translational tile in dimension three`PeriodicTilingThree`Combinatorics	A counterexample to periodic tiling in dimension three	Combinatorics	Theorem 1.1A translational tile with no fully periodic tiling in dimension threepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	12	34
Cubic lower bounds for permanent determinantal complexity`PermanentCubic`Theoretical computer science	A cubic permanent–determinant lower bound	Theoretical computer science	Theorem 1.1A cubic lower bound for border determinantal complexity of the permanentpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	6	24
Petty’s projection-volume inequality`PettyProjectionVolume`Convex and metric geometry	Sharp projection-body inequalities and a counterexample to simplex maximization	Convex and metric geometry	Theorem 1.1Petty’s projection-volume conjecture in dimensions at least fourpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	10	24
The irrationality exponent of $\pi$ equals two`PiExponent`Number theory	The irrationality exponent of π is 2	Number theory	Theorem 1.1The irrationality exponent of pi is 2possible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	No	0	9
Negatively pinched Kähler threefold without bounded coordinates`PinchedKahler`Differential geometry	Negative Kähler curvature without bounded holomorphic coordinates	Differential geometry	Theorem 1.1A negatively pinched Kähler threefold without bounded holomorphic coordinatespossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	37	105
Weak pinned planar distance theorem`PinnedDistances`Combinatorics	Planar distinct distances and unit-distance bounds	Combinatorics	Corollary 1.2The weak pinned planar distance theorempossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	6	15
Almost-sure spectrum of the planar Anderson operator`PlanarAndersonSpectrum`Mathematical physics	Localization and delocalization in the Anderson model	Mathematical physics	Theorem 1.1Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorderpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	6	15
Planar Falconer distance theorem`PlanarFalconer`Real and complex analysis	The Falconer distance conjecture	Real and complex analysis	Proposition 5.10The Falconer distance conjecture in all dimensionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	3	7
Differentiability of the exponential first-passage limit shape`PlanarFirstPassage`Probability and statistical mechanics	Planar first-passage geometry and the absence of bigeodesics	Probability and statistical mechanics	Theorem 1.1Strict convexity and differentiability of the planar exponential first-passage limit shapepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	17	64
Planar graph metrics in $L_1$`PlanarL1`Convex and metric geometry	Bounded-distortion L₁ embeddings of planar and bounded-treewidth graphs	Convex and metric geometry	Theorem 1.1Planar Graph Metrics Embed into L1 with Constant Distortionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	4	31
Sharp Fourier certificate for planar circle packing`PlanarPacking`Convex and metric geometry	Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy	Convex and metric geometry	Theorem 1.1A sharp Fourier certificate for planar circle packingpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	0	No	4	13
Power saving for planar unit distances`PlanarUnitDistances`Combinatorics	Planar distinct distances and unit-distance bounds	Combinatorics	Theorem 1.1A power saving for planar unit distancespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	4	11
Proper seven-coloring`PlaneColoring`Combinatorics	The Euclidean plane cannot be colored with five colors	Combinatorics	Theorem 1.1The Euclidean plane is not five-colorablepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	2	5
Quasi-isometric recognition of virtually polycyclic groups and solvable lattices`PolycyclicRecognition`Group theory	Quasi-isometric recognition of virtually polycyclic groups	Group theory	Theorem 1.4Quasi-isometric recognition of virtually polycyclic groupspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	20	136
Posterior-replica comparisons and sample lower bound`PosteriorReplicas`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	Proposition 7.1Subsphere methods for memory-sample lower bounds in noiseless Gaussian regressionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	75	323
Positive density of power-free polynomial values`PowerFreeValues`Number theory	Squarefree quartics and power-free polynomial values	Number theory	Corollary 1.3Squarefree values of quartics and power-free values of polynomialspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	7	24
Positive lower density of prime-ratio increases`PrimeGaps`Number theory	Positive lower density of large prime gaps	Number theory	Theorem 1.1Positive lower density of large prime gapsCorollary 1.2Positive lower density of large prime gapspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	6	23
Brown measure of the selected product weighted shift`ProductBrown`Operator algebras	Invariant projections, hyperinvariant subspaces, and transitive algebras	Operator algebras	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	62	541
Failure of the simplex upper bound in dimension 20`ProjectionCounterexample`Convex and metric geometry	Sharp projection-body inequalities and a counterexample to simplex maximization	Convex and metric geometry	Theorem 1A product counterexample to the simplex maximum for projection-body volumepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	8	17
Projection, cap, and Riesz estimates with regression bounds`ProjectionMoments`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	90	425
Explicit product-of-simplices counterexample`ProjectionVolume`Convex and metric geometry	Sharp projection-body inequalities and a counterexample to simplex maximization	Convex and metric geometry	Theorem 1A product counterexample to the simplex maximum for projection-body volumepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	11	33
Constant-depth quantum parity lower bound`QACParity`Mathematical physics	Parity is not in QAC⁰	Mathematical physics	Theorem 1Product-projection localization and the QAC0 parity lower boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	16	37
Ample bundles without Griffiths-positive metrics`QuadricBundles`Algebraic and complex geometry	A counterexample to Griffiths’ positivity conjecture	Algebraic and complex geometry	Theorem 1.1Ample rank-two bundles on the quadric surface without Griffiths-positive metricspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	34	134
Uniform van der Waerden lower bound`QuantitativeVanDerWaerden`Combinatorics	Superexponential van der Waerden numbers	Combinatorics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	4	12
Riemann zeta $7/8$ bound`QuasiRiemannHypothesis`Number theory	The quasi-Riemann hypothesis	Number theory	Theorem 1.1The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane $\Re s\gt 7/8$possible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	0	3
Exact two-cycle bound for quintic Liénard systems`QuinticLienard`Dynamical systems and ergodic theory	Hilbert’s sixteenth problem: uniform bounds for limit cycles	Dynamical systems and ergodic theory	Proposition 2.5Two limit cycles for quintic Liénard systemspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	Yes	5	17
A common radial phase transition over a density interval`RadialDensityInterval`Probability and statistical mechanics	Continuum phase transitions for radial pair potentials	Probability and statistical mechanics	Theorem 1.1A radial continuum phase transition with algebraic decaypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	13	44
Fixed-density radial continuum phase transition`RadialTransition`Probability and statistical mechanics	Continuum phase transitions for radial pair potentials	Probability and statistical mechanics	Theorem 1.1A radial continuum phase transition with algebraic decaypossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	13	41
Sharp logarithmic exponent of $r(5,t)$`RamseyFive`Combinatorics	Sharp logarithmic exponents for off-diagonal Ramsey numbers	Combinatorics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	4	16
Randomized quasipolynomial mean-payoff algorithm`RandomizedMeanPayoff`Theoretical computer science	Quasipolynomial algorithms for mean-payoff, stochastic and parity games	Theoretical computer science	Theorem 1.1Randomized quasipolynomial-time mean-payoff gamespossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	23	94
Polynomial hitting lists for rational formulas`RationalHitting`Theoretical computer science	Uniform black-box noncommutative identity testing across characteristics	Theoretical computer science	Theorem 1.1Polynomial Hitting Lists for Noncommutative Rational Formulaspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	22	66
Quantitative renorming of real $\ell_1$`RealL1Renorming`Functional analysis	A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces	Functional analysis	Corollary 1.3A uniformly discrete counterexample to bounded approximation in Lipschitz-free spacespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	6	23
Recursive-potential spaces and midpoint convexity`RecursivePotentials`Functional analysis	Reflexive midpoint convexity and diamond distortion	Functional analysis	Theorem 2.1Midpoint convexity from two recursive potentialsTheorem 6.3Midpoint convexity from two recursive potentialspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	159	538
Nonexpansive fixed points in reflexive spaces`ReflexiveFixedPoints`Functional analysis	Nonexpansive fixed points in reflexive Banach spaces	Functional analysis	Theorem 1.1Fixed Points of Nonexpansive Maps in Reflexive Banach Spacespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	1	11
Polynomial-size parity specialization`RegularParity`Mathematical physics	Parity is not in QAC⁰	Mathematical physics	Theorem 1Product-projection localization and the QAC0 parity lower boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	15	36
Dense relative generators for irreducible inclusions of finite factors`RelativeGeneration`Operator algebras	The generator problem for finite factors	Operator algebras	Theorem 1.1Relative generation and the generator problem for finite factorspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	11	66
Quantitative higher-codimension Riesz rectifiability`RieszQuantitative`Real and complex analysis	Riesz transforms and rectifiability in higher codimension	Real and complex analysis	Theorem 1.3Riesz transforms and uniform rectifiability in higher codimensionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	8	34
Mixing of every finite order for one mixing transformation`Rokhlin`Dynamical systems and ergodic theory	Rokhlin’s multiple-mixing problem	Dynamical systems and ergodic theory	Theorem 1.1Rokhlin’s multiple-mixing problem for one transformationpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	4	18	4 definitions checked by name and type only
Finite cylinder approximation for the selected ruled families`RuledCovering`Convex and metric geometry	Cylinder coverings below the half-area bound	Convex and metric geometry	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	46	161
Fixed-prime Ryser counterexamples`RyserCovering`Combinatorics	Counterexamples to Ryser’s covering conjecture	Combinatorics	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	10	29
Counterexamples in odd extension degrees`RyserOddExtensions`Combinatorics	Counterexamples to Ryser’s covering conjecture	Combinatorics	Theorem 1.1A counterexample to Ryser’s covering conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	11	41
Computability of the random $3$-SAT threshold`SATComputability`Probability and statistical mechanics	Limiting random SAT thresholds, sharp variance and computability	Probability and statistical mechanics	Theorem 1.1Computing the Random 3-SAT Thresholdpossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	2	No	8	26
Sharpness of random $k$-SAT lifetime and replacement bounds`SATSharpness`Probability and statistical mechanics	Limiting random SAT thresholds, sharp variance and computability	Probability and statistical mechanics	Theorem 1.1A Limiting Satisfiability Threshold for Every Fixed Clause Sizepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	16	44
Variance bounds for the random $k$-SAT hitting time`SATVariance`Probability and statistical mechanics	Limiting random SAT thresholds, sharp variance and computability	Probability and statistical mechanics	Theorem 1.1Linear Variance of the Random 3-SAT Hitting Timepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	16	38
Stretched-exponential barriers from typical equilibrium initial states`SKBarriers`Probability and statistical mechanics	Critical SK autocorrelation processes and dynamics across the temperature transition	Probability and statistical mechanics	Theorem B.1Stretched-exponential barriers for typical SK initial statespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	19	46
Full support of zero-temperature SK minimizers`SKFullSupport`Mathematical physics	QAOA attains the SK optimum in the thermodynamic-first limit	Mathematical physics	Theorem 1.1Full support of the zero-temperature Sherrington-Kirkpatrick order parameterpossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	No	16	63
Spectral-gap bound throughout the high-temperature SK phase`SKHighTemperature`Probability and statistical mechanics	Critical SK autocorrelation processes and dynamics across the temperature transition	Probability and statistical mechanics	Theorem 1.1A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phasepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	18	42
Discrete mixing-time ratio cutoff for $\beta<1/2$`SKRatio`Probability and statistical mechanics	Critical SK autocorrelation processes and dynamics across the temperature transition	Probability and statistical mechanics	Theorem 1.1A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phasepossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	16	44
Parisi ground-state value identities and finite Gaussian approximation`SKValue`Mathematical physics	QAOA attains the SK optimum in the thermodynamic-first limit	Mathematical physics	Theorem 1.1QAOA attains the SK ground-state energy in the thermodynamic-first limitpossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	No	35	128
Positivity of the explicit gauge on every positive-time segment`SLELowerPositivity`Probability and statistical mechanics	Exact Hausdorff gauges for SLE	Probability and statistical mechanics	Theorem 1.1An explicit exact Hausdorff gauge for SLEpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	No	14	53
Saxl’s conjecture`Saxl`Algebra	Saxl’s conjecture and universal tensor squares	Algebra	Theorem 1.1A Cyclic Polytabloid Proof of Saxl’s Conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	14	72
Second Kahn–Kalai threshold bounds`SecondKahnKalai`Combinatorics	The second Kahn–Kalai conjecture with an edge-count bound	Combinatorics	Theorem 1.1The second Kahn–Kalai conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	12	37
Entropy-rate dimension formula`SelfSimilar`Dynamical systems and ergodic theory	The entropy-rate dimension formula for self-similar measures	Dynamical systems and ergodic theory	Theorem 1.1The entropy-rate dimension formula for self-similar measures on the linepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	12	39
Homogeneous-measure and self-similar-attractor dimension formulas`SelfSimilarCorollaries`Dynamical systems and ergodic theory	The entropy-rate dimension formula for self-similar measures	Dynamical systems and ergodic theory	Theorem 1.1The entropy-rate dimension formula for self-similar measures on the linepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	10	43
Superquadratic sensitivity separation`SensitivitySeparation`Theoretical computer science	A superquadratic separation of sensitivity and block sensitivity	Theoretical computer science	Theorem 1.1A superquadratic separation between sensitivity and block sensitivitypossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	5	22
Failure of the separable quotient assertion under the continuum hypothesis`SeparableQuotientNegative`Functional analysis	Independence of the separable quotient problem	Functional analysis	Proposition 2.2Relative independence of the separable quotient problempossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	3	11
Seymour’s second-neighborhood conjecture`SeymourSecondNeighborhood`Combinatorics	Seymour’s second-neighborhood conjecture	Combinatorics	Theorem 1.1A proof of Seymour’s second-neighborhood conjecturepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	4	15
Sharp integral fillings in proper $\mathrm{CAT}(0)$ spaces`SharpCAT0Filling`Differential geometry	Sharp Cartan–Hadamard isoperimetry and rigidity	Differential geometry	Theorem 1.1Sharp integral fillings in CAT(0) spacespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	24	93
Sharp logarithmic exponent for fixed off-diagonal Ramsey numbers`SharpLogRamsey`Combinatorics	Sharp logarithmic exponents for off-diagonal Ramsey numbers	Combinatorics	Theorem 1.1Sharp logarithmic exponents for fixed off-diagonal Ramsey numberspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	4	20
Sharp threshold width for monotone graph properties`SharpThreshold`Combinatorics	Uniform influence and sharp thresholds for graph and hypergraph properties	Combinatorics	Theorem 1.1A Sharp Threshold Bound for Monotone Graph Propertiespossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	12	37
Optimal order of the shortest Egyptian-fraction expansions`ShortEgyptianFractions`Number theory	Short Egyptian fractions	Number theory	Proposition 2.1Short Egyptian fractionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	3	14
Counterexample to Sidorenko’s conjecture`SidorenkoCounterexample`Combinatorics	Counterexamples to Sidorenko’s conjecture and the forcing conjecture	Combinatorics	Theorem 1.1A counterexample to Sidorenko’s conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	7	23
Uniform real-zero gap`SiegelZeros`Number theory	The quasi-Riemann hypothesis	Number theory	Theorem 1Uniform exclusion of Landau–Siegel zerospossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	0	16
Signed finite-band disk-maximal gradient bound`SignedFiniteBand`Real and complex analysis	Endpoint Sobolev regularity of centered disk averages	Real and complex analysis	Theorem 1.1An Endpoint Gradient Bound for the Centered Disk Maximal Operatorpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	7	21
Uniform signed-occurrence moment bound for coordinate sweeps`SignedSweepMoment`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Signed tensor densities and diagram budgets for the Thorp shufflepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	34	133
Infinite finitely presented simple amenable group`SimpleAmenable`Group theory	An infinite finitely presented simple amenable group	Group theory	Theorem 1.1An infinite finitely presented simple amenable grouppossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	1	8
Simple type $F_\infty$ overgroups of groups with decidable word problem`SimpleOvergroups`Group theory	Boone–Higman embeddings with higher finiteness	Group theory	Theorem 1.1Simple F∞ overgroups of groups with decidable word problempossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	3	22
Single-fold Diophantine representations`SingleFold`Mathematical logic	Single-fold Diophantine representations and undecidability under an at-most-one-solution promise	Mathematical logic	Corollary 1.2Single-fold Diophantine representationspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	3	12
Single-lattice covering bound`SingleLatticeCovering`Convex and metric geometry	The optimal order of convex-body covering density	Convex and metric geometry	Theorem 1.1A single-lattice covering bound of order n log npossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	3	11
Approximate counting with singleton loops`SingletonLoopMatching`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	Theorem 1.2Entropy and Face Dimension of the Perfect-Matching Polytopepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	24	80
Determinantal lower bound from a smooth initial form`SmoothInitialForm`Theoretical computer science	A cubic permanent–determinant lower bound	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	5	37
Finite-entropy system without a smooth positive-volume model`SmoothObstruction`Dynamical systems and ergodic theory	Zero entropy does not guarantee a smooth positive-volume model	Dynamical systems and ergodic theory	Theorem 1.1A zero-entropy system without a smooth positive-volume modelpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — DECLARED”	3	No	9	58
Nodal counterexamples in dimensions three and four`SmoothYau`Differential geometry	Yau’s nodal bounds: surfaces and higher dimensions	Differential geometry	no confident match	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	18	88
Reconstruction of the 35-move Snaky certificate`SnakyCertificate`Combinatorics	Snaky in 21 Maker moves	Combinatorics	Proposition 10Snaky in 21 Maker movespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	670	718
Conditional winning templates from finite partial positions`SnakyConditional`Combinatorics	Snaky in 21 Maker moves	Combinatorics	Proposition 10Snaky in 21 Maker movespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	9	41
Legal Snaky winning strategy within 21 Maker moves`SnakyTwentyOne`Combinatorics	Snaky in 21 Maker moves	Combinatorics	Theorem 1Snaky in 21 Maker movespossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	9	41
Sharp binary-channel contraction and entropy production`SoftChannel204`Theoretical computer science	The Courtade–Kumar and Hellinger conjectures	Theoretical computer science	Theorem 1.1Sharp binary-information contraction on the discrete cubepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	34	68
Positive diagonal programs on incompressible coding sheets`SolenoidalSheetPrograms`Partial differential equations	Universal computation in forced Navier–Stokes flows	Partial differential equations	Theorem 5.1Computation under Rapidly Vanishing Navier–Stokes Forcingpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	42	139
Spherical linear-field dual formula and approximation`SphericalField`Probability and statistical mechanics	Perceptron free energies and microscopic jamming exponents	Probability and statistical mechanics	Proposition 4The free energy of the spherical random perceptronpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	66	446
One-sided angle bound for signed spin types`SpinAngle`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Corollary 1.3Compatibility entropy and the spectrum of a Thorp sweeppossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	61	329	3 definitions checked by name and type only
Integrability of both holomorphic tangent summands`SplitTangentIntegrability`Algebraic and complex geometry	Tangent splittings and product decompositions	Algebraic and complex geometry	Theorem 1.1Integrability of split tangent bundles on rationally connected manifoldspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	No	20	86
Power saving for square-difference-free sets`SquareDifference`Combinatorics	Power savings for intersective polynomial differences and prime arguments	Combinatorics	Theorem 1.1A power saving for square-difference-free setspossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	1	No	1	7
Unbounded violations of the square-root Fourier-degree bound`SquareRootDegree`Combinatorics	Boolean functions violate the square-root degree bound by arbitrary factors	Combinatorics	Theorem 1.1Unbounded Violations of the Square-Root Degree Boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	12	29
Degree-five stable noncoordinate with nonrectifiable affine-space fibers`StableCoordinateFour`Algebraic and complex geometry	A stable-coordinate counterexample in four variables	Algebraic and complex geometry	Theorem 1.1An explicit noncoordinate polynomial with affine three-space zero fibrepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	13	28
Positive-area hyperbolic Bernoulli component`StandardMapComponents`Dynamical systems and ergodic theory	Positive metric entropy for the standard map	Dynamical systems and ergodic theory	Corollary 1.2Positive Metric Entropy for the Standard Map at Large Parameterspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	19	77
Positive metric entropy for all sufficiently large parameters`StandardMapEntropy`Dynamical systems and ergodic theory	Positive metric entropy for the standard map	Dynamical systems and ergodic theory	Theorem 1.1Positive Metric Entropy for the Standard Map at Large Parameterspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	11	29
Positive Lyapunov exponents and entropy`StandardMapLyapunov`Dynamical systems and ergodic theory	Positive metric entropy for the standard map	Dynamical systems and ergodic theory	Theorem 1.1Positive Metric Entropy for the Standard Map at Large Parameterspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	21	75
Euclidean signed and reordered prefix bounds`SteinitzBergstrom`Convex and metric geometry	The Euclidean Steinitz–Bergström bound	Convex and metric geometry	Corollary 6.1The Euclidean Steinitz–Bergström theorempossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	3	Yes	3	16
Strict inverse-first-power bound and consequences`StrictMeans`Real and complex analysis	Brennan’s conjecture and the integral-means spectrum	Real and complex analysis	Theorem 1.1A strict inverse-first-power bound for univalent functionspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	7	25
Universal near-identity unitary conjugacy for close von Neumann algebras`StrongKadisonKastler`Operator algebras	Strong Kadison–Kastler stability and its spatial boundaries	Operator algebras	Theorem 1.1Universal strong Kadison–Kastler stabilitypossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	6	17
Strong thin-tree bound`StrongThinTree`Combinatorics	Deterministic construction of strong thin spanning trees	Combinatorics	Theorem 1.1The strong thin tree conjecturepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	6	23
Strongly Rayleigh and determinantal-process IID factors`StronglyRayleighDPP`Probability and statistical mechanics	The free uniform spanning forest is a factor of IID	Probability and statistical mechanics	Corollary 1.4The free uniform spanning forest is a factor of IIDpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	21	139
Optimal similarity and boundary representation`StructuralCrouzeix`Functional analysis	The complete Crouzeix conjecture	Functional analysis	Theorem 1.2The complete Crouzeix theorem: optimal similarity and a common positive boundary representationTheorem 1.3The complete Crouzeix theorem: optimal similarity and a common positive boundary representationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	18	119
Dimension reduction in $L_p$`SubpolynomialLp`Convex and metric geometry	Subpolynomial dimension reduction in L_p	Convex and metric geometry	no confident match	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	4	25
Subsphere estimates and memory–sample lower bounds`SubsphereCurrent`Theoretical computer science	Memory–sample lower bounds for noiseless Gaussian regression	Theoretical computer science	Proposition 7.1Subsphere methods for memory-sample lower bounds in noiseless Gaussian regressionpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	61	265
Polynomial-time 2-approximation for shortest common superstring`Superstring`Theoretical computer science	A factor-two approximation for shortest common superstring	Theoretical computer science	Theorem 1.1A Polynomial-Time 2-Approximation for Shortest Common Superstringpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	10	20
Ring-theoretic properties of the completed surface-cone candidate`SurfaceConeCandidateSupport`Algebra	A counterexample to the small Cohen–Macaulay module conjecture	Algebra	Theorem 1.1A Complete Local Domain without a Small Cohen–Macaulay Modulepossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “SUPPORT-ONLY”	3	Yes	0	7
Smooth isometric immersion of every closed surface into four-space`SurfaceImmersion`Differential geometry	Smooth isometric immersions of surfaces into ℝ⁴	Differential geometry	Theorem 1.1Smooth isometric immersions of closed surfaces into Euclidean four-spacepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	6	18
Polynomial mixing and connectivity for every graphical degree sequence`SwitchChain`Theoretical computer science	Rapid mixing of graph switches for every degree sequence	Theoretical computer science	Theorem 1.1Polynomial mixing of the switch chain for every graphical degree sequencepossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	No	28	125
Symmetry of semialgebraic bounded domains`SymmetricDomains`Algebraic and complex geometry	Semialgebraic universal covers and bounded domains	Algebraic and complex geometry	Theorem 1.1Symmetry of semialgebraic bounded domains with compact quotientpossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	Yes	8	44
Symmetric Mahler equality characterization`SymmetricMahlerEquality`Convex and metric geometry	The Mahler conjectures, functional inequalities and polar-product symplectic width	Convex and metric geometry	Theorem 1.1The symmetric Mahler conjecture and its equality casespossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	2	Yes	5	26
Gromov width of symmetric polar products`SymmetricPolar`Convex and metric geometry	The Mahler conjectures, functional inequalities and polar-product symplectic width	Convex and metric geometry	Theorem 1.1Symplectic Balls in Symmetric Polar Productspossible match from Lean wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	9	28
Tachikawa counterexample`Tachikawa`Algebra	Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures	Algebra	Theorem 1.1A counterexample to Tachikawa’s second conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	3	22
Talagrand discrete convexity`TalagrandDiscreteConvexity`Combinatorics	Talagrand’s expectation thresholds, discrete convexity, and graph decompositions	Combinatorics	Theorem 1.1Talagrand’s discrete-convexity conjecturepossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	8	20
Integral–fractional expectation-threshold comparison`TalagrandExpectationThreshold`Combinatorics	Talagrand’s expectation thresholds, discrete convexity, and graph decompositions	Combinatorics	Theorem 1.1Integral and fractional expectation thresholds are equivalentpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	Yes	12	25
Taming implies compatibility`TamingCompatibility`Differential geometry	Donaldson’s tamed-to-compatible conjecture	Differential geometry	Theorem 1.1Taming implies compatibility on four-manifoldspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	13	40
Thomason model structures and nerve detection in all positive strict dimensions`ThomasonModelStructures`Topology	Thomason model structures in all strict higher dimensions	Topology	Theorem 1.1Thomason Model Structures in Every Strict Higher Dimensionpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	110	1,914
Nonamenability of Thompson’s group $F$`ThompsonNonamenability`Group theory	Thompson’s group F is nonamenable	Group theory	Theorem 1.1Thompson’s group F is nonamenablepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	12	51
Reciprocal Specht degrees and eight-block Fourier bound`ThorpFirstReciprocal`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	34	138
Frame, spectral, and density estimates for Thorp mixing`ThorpRemaining`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Optimal-order mixing of the Thorp shufflepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	87	349
Nine routing-density and representation estimates`ThorpRouting`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Proposition 5.1Routing densities and representation contraction for Thorp sweepspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	357	1,565
Weighted row–column compatibility bound`ThorpWeightedCompatibility`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Row–column symmetry and contraction of coordinate sweepspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	7	33
Optimal three-machine unit-job scheduling`ThreeMachine`Theoretical computer science	Polynomial-time scheduling on three identical machines	Theoretical computer science	Theorem 1.1A Polynomial-Time Algorithm for Three-Machine Unit-Job Schedulingpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	18	72
Supercritical reconstruction on regular and Poisson trees`ThreeStateSupercritical`Probability and statistical mechanics	Exact three- and four-state reconstruction thresholds and four-state tree capacity	Probability and statistical mechanics	Theorem 1.1The exact reconstruction threshold for the three-state symmetric channelpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	17	65
Three-state reconstruction above the Kesten–Stigum threshold`ThreeStateTreeClauses`Probability and statistical mechanics	Exact three- and four-state reconstruction thresholds and four-state tree capacity	Probability and statistical mechanics	Theorem 1.1The exact reconstruction threshold for the three-state symmetric channelpossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	14	60
Smooth simple Lebesgue spectrum on the three-torus`ThreeTorus`Dynamical systems and ergodic theory	Banach’s simple Lebesgue-spectrum problem	Dynamical systems and ergodic theory	Theorem 1.1A smooth three-torus diffeomorphism with simple Lebesgue spectrumpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	12	51
Tingley’s sphere-isometry extension`TingleySphereIsometry`Functional analysis	Tingley’s sphere-isometry problem	Functional analysis	Theorem 1.1A positive solution to Tingley’s problempossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	2	17
Torsion-free hyperbolic group that is not residually finite`TorsionFreeHyperbolic`Group theory	A torsion-free hyperbolic group that is neither residually finite nor linear over any field	Group theory	Corollary 1.2A torsion-free hyperbolic group that is not residually finitepossible match from catalogue wording; no review recorded	All of itTheir term: “full”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	4	22
Torsion-free group-algebra counterexample`TorsionFreeZeroDivisors`Algebra	A counterexample to Kaplansky’s zero-divisor conjecture	Algebra	Theorem 1.1A Torsion-Free Group Algebra with Zero Divisorspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	3	24
Totient-count asymptotics and regular variation`TotientAsymptotic`Number theory	An asymptotic formula for the number of totients	Number theory	Theorem 2.1An asymptotic formula for the number of totientspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	32	105
Exact zero case for the companion totient counts`TotientCompanionZero`Number theory	An asymptotic formula for the number of totients	Number theory	Theorem 2.1An asymptotic formula for the number of totientspossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	No	22	64
Transport of trace ideals and their additive-idempotent description`TraceIdealTransportSupport`Operator algebras	Trace cones and Razak–Jacelon stabilization	Operator algebras	Theorem 1.1The trace cone classifies Razak–Jacelon stabilizationspossible match from catalogue wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “SUPPORT-ONLY”	3	Yes	30	158
Quantitative and superpolynomial sample lower bounds for trace reconstruction`TraceReconstruction`Theoretical computer science	Quantitative trace-reconstruction bounds with a uniform decoder	Theoretical computer science	Theorem 1.1Quantitative lower bounds for trace reconstructionpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	3	No	13	49
Tree-based binary edit-distance distortion lower bound`TreeEdit`Convex and metric geometry	The sharp exponential scale of edit-distance distortion	Convex and metric geometry	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	7	25
Face correspondence under triangle expansion`TriangleFace`Theoretical computer science	Approximate counting and entropy of perfect matchings	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	24	86
Sharp terminal edge count in random triangle removal`TriangleRemoval`Combinatorics	The sharp terminal leave in random triangle removal	Combinatorics	Theorem 1.1The sharp terminal leave in random triangle removalpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	11	31
Explicit triangular-cylinder cover below half area`TriangularCovering`Convex and metric geometry	Cylinder coverings below the half-area bound	Convex and metric geometry	Theorem 1.1Finite angular cylinder covers below the half-area boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	16	40
Universal energy minimality of the triangular lattice`TriangularEnergy`Convex and metric geometry	Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy	Convex and metric geometry	Theorem 1.1An atomic certificate for triangular-lattice universal optimalitypossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	20	39
Gaussian Fourier minorants with their construction`TriangularGaussian`Convex and metric geometry	Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy	Convex and metric geometry	Theorem 1.2An atomic certificate for triangular-lattice universal optimalitypossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	73	149
Maximal triangular Hilbert transform bound`TriangularHilbert`Real and complex analysis	Annular variation and dyadic absolute bounds for the triangular Hilbert transform	Real and complex analysis	Theorem 1.1The maximal triangular Hilbert transform at the symmetric pointpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	9	28
Finite counterexample to Truffet’s optimization procedure`TruffetCounterexample`Theoretical computer science	Quasipolynomial algorithms for mean-payoff, stochastic and parity games	Theoretical computer science	Proposition 5.1Randomized quasipolynomial-time mean-payoff gamespossible match from Lean wording; no review recorded	Part of itTheir term: “weaker-statement”	Part of itTheir term: “NARROWER — UNDECLARED”	3	No	30	92
Two-way nondeterministic complementation lower bound`TwoWayComplementation`Theoretical computer science	Exponential state costs for two-way automata	Theoretical computer science	Theorem 1.1An exponential state lower bound for two-way nondeterministic complementationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	5	24
Same-family determinization lower bound`TwoWayDeterminization`Theoretical computer science	Exponential state costs for two-way automata	Theoretical computer science	Theorem 1.1An exponential state lower bound for two-way nondeterministic complementationpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	8	36
Weak normalization implies strong normalization in every pure type system`TypeSystemNormalization`Mathematical logic	Weak normalization implies strong normalization in pure type systems	Mathematical logic	Theorem 1Weak and strong normalization in pure type systemspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	18	76
Uniform amplified commutator estimate`UniformCommutator`Operator algebras	Kadison’s similarity conjecture	Operator algebras	Theorem 1.2Kadison’s similarity theorem through uniform derivation estimatespossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	3	21
Uniform exact DFT and convolution with a power saving`UniformFourier`Theoretical computer science	Exact Fourier transforms below $n\log n$	Theoretical computer science	Corollary 1.3An explicit power saving for the exact discrete Fourier transformpossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	54	198
Uniform property $\Gamma$ from tracial real rank zero`UniformGamma`Operator algebras	Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability	Operator algebras	Theorem 1.1Tracial projection methods and uniform property Gammapossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	3	Yes	67	331
Uniform bit algorithm for the squared-logarithmic $k$-server bound`UniformKServer`Theoretical computer science	Optimal-order randomized k-server on arbitrary metrics	Theoretical computer science	Theorem 1.1Uniform computation of the squared-logarithmic k-server boundpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	31	132
Uniform sparsest-cut integrality gaps`UniformSparsestCut`Theoretical computer science	Uniform sparsest cut: hardness and semidefinite gaps	Theoretical computer science	Theorem 1.1Near-square-root logarithmic integrality gaps for uniform sparsest cutpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	Yes	7	30
Unique Games gap reduction`UniqueGamesTheorem`Theoretical computer science	The Unique Games Conjecture and optimal approximation thresholds	Theoretical computer science	Theorem 1.1The Unique Games Theorempossible match from catalogue wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	31	122
Universal group of type $F_\infty$`UniversalFInfinity`Group theory	Boone–Higman embeddings with higher finiteness	Group theory	Theorem 1.1A universal group of type F∞possible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	Yes	1	13
Universal irreducible tensor squares for symmetric groups`UniversalTensorSquares`Algebra	Saxl’s conjecture and universal tensor squares	Algebra	Theorem 1.1Universal Tensor Squares for Symmetric Groupspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	0	No	12	72
EXPTIME-completeness of variable-dimension Weisfeiler–Leman equivalence`VariableWL`Theoretical computer science	The computational complexity of Weisfeiler–Leman refinement	Theoretical computer science	no confident match	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	27	93
Positive-probability transience and the velocity hemisphere`VelocityHemisphere`Probability and statistical mechanics	Directional zero–one laws beyond iid environments and iid ballisticity	Probability and statistical mechanics	Corollary 1.2Directional transience implies ballisticitypossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNLINKED”	2	No	20	74
Energy bounds, strong locality, and an irreducible conformal net`VertexAlgebraNet`Mathematical physics	Unitary vertex operator algebras and conformal nets	Mathematical physics	Theorem 1.1Strongly rational unitary vertex operator algebras and conformal netspossible match from catalogue wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — DECLARED”	3	No	89	535
Vertex Cover gap and factor-two hardness`VertexCover`Theoretical computer science	The Unique Games Conjecture and optimal approximation thresholds	Theoretical computer science	Theorem 1.1The Factor-Two Hardness Threshold for Vertex Coverpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	1	Yes	26	103
Global classical Vlasov–Maxwell solutions`VlasovMaxwell`Partial differential equations	Global smoothness for relativistic Vlasov–Maxwell	Partial differential equations	Theorem 1.1Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell systempossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	28	80
EXPTIME-completeness of Weisfeiler–Leman graph identification`WLIdentification`Theoretical computer science	The computational complexity of Weisfeiler–Leman refinement	Theoretical computer science	Theorem 1.1The complexity of identifying a graph by Weisfeiler–Leman refinementpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	No	32	93
Weak Hessian bounds along every geodesic`WeakHessian`Differential geometry	Gigli’s characterization of Alexandrov curvature	Differential geometry	Theorem 1.1Weak Hessian bounds along every geodesic in RCD spacespossible match from Lean wording; no review recorded	A supporting or different resultTheir term: “supporting-only”	A supporting or different resultTheir term: “DIFFERENT”	2	Yes	45	149
Convex injectivity domains under weak MTW`WeakMTWGlobalSupport`Differential geometry	Weak MTW curvature gives convexity and regular optimal transport	Differential geometry	Theorem 1.1Global Support and Convex Injectivity Domains under Weak MTWpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	2	Yes	10	46
Weighted Schatten moments and operator contraction for coordinate sweeps`WeightedSweepMoments`Probability and statistical mechanics	Optimal logarithmic mixing of the Thorp shuffle	Probability and statistical mechanics	Theorem 1.1Row–column symmetry and contraction of coordinate sweepspossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	42	175
Unconditional sequential time lower bounds for Weisfeiler–Leman equivalence`WeisfeilerLeman`Theoretical computer science	The computational complexity of Weisfeiler–Leman refinement	Theoretical computer science	Theorem 1.1Unconditional time lower bounds for Weisfeiler–Leman equivalencepossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	52	196
Strict expressive gain from one witnessed symmetric choice`WitnessedChoice`Mathematical logic	Separating choiceless counting from polynomial time and witnessed choice	Mathematical logic	Theorem 1.1Witnessed symmetric choice is strictly stronger than choiceless polynomial time with countingpossible match from Lean wording; no review recorded	All of itTheir term: “full”	All of itTheir term: “MATCHES”	3	No	62	357
Unbounded nodal ratio on $S^4\times S^1$`YauCounterexample`Differential geometry	Yau’s nodal bounds: surfaces and higher dimensions	Differential geometry	Theorem 1.1Smooth counterexamples to Yau’s nodal upper bound in dimensions three and fourpossible match from Lean wording; no review recorded	Part of itTheir term: “partial”	Part of itTheir term: “NARROWER — UNDECLARED”	2	Yes	12	44