Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Families

OpenAI groups related papers into 372 families. Each row links to the papers, their Lean statements and independent assessments.

The papers cited most within the release are listed on their own page.

No family has an explanation written for the atlas yet. An explanation for mathematicians outside a family’s area is one of the most useful things to add, and each family page has a button to offer one. The contributing guide sets out what to include and how the work is reviewed. Read CONTRIBUTING.md

Every family

Search all text

372 of 372 families shown

MathVet and cert-machine assessed whether each family’s Lean statements express the whole result OpenAI describes in its catalogue. Each column gives Atlas’s description first, followed by the group’s own term in quotation marks. Menu counts are for the whole release.

Every family in the release, one per row, in the release’s order.
FamilyLean statementsMathVetcert-machineProofs reported acceptedOther proof or calculation reportsExplanation
001Milne’s rationality conjecture and algebraic specializationNumber theoryOne earlier editionNumber theory1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
002The full BSD formula from low Selmer corankNumber theoryThree earlier editionsNumber theory3No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
003The quasi-Riemann hypothesisNumber theoryNumber theory344All of itTheir term: “full”All of itTheir term: “MATCHES”4 of 4None recordedNine explanations by others
004Hilbert’s tenth problem over ℚNumber theoryTwo earlier editionsNumber theory2No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
005Irrationality of Catalan’s constantNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Exact calculations for finite claimsOne problem reported, not judged by the atlas
006Goldfeld’s conjecture: densities and mean analytic rankNumber theoryTwo earlier editionsNumber theory2No Lean statement5No Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by othersOne problem reported, not judged by the atlas
007Ordinary two-point correlations and the corrected Elliott conjectureNumber theoryNumber theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
008The Deligne–Drinfeld conjectureNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
009Function-field reconstruction from Milnor K-theory and Galois dataNumber theoryNumber theory31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
010Unrestricted pro-modularity at the prime twoNumber theoryTwo earlier editionsNumber theory3No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
011Prime-factor statistics of \(p-1\)Number theoryNumber theory3No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
012Independent largest prime factors of consecutive integersNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
013Ostmann’s inverse Goldbach conjectureNumber theoryNumber theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
014Restricted geometric Langlands, global Arthur enhancements, and generic RamanujanNumber theoryNumber theory8No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
015Torus-packet equidistribution in prime, quartic, and sextic degreesNumber theoryNumber theory31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
016Zilber–Pink in abelian varieties and the Siegel threefoldNumber theoryNumber theory4No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
017The irrationality exponent of π is 2Number theoryThe two readers disagreeNumber theory11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1Proofs of selected steps in HOL LightTwo explanations by others
018The Margulis–Platonov conjecture over global fieldsNumber theoryNumber theory2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
019The local p-adic section conjecture and global consequencesNumber theoryOne earlier editionNumber theory2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
020Squarefree quartics and power-free polynomial valuesNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Exact calculations for finite claimsNo explanation yet
021A quadratic bound for Jacobsthal’s functionNumber theoryNumber theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedOne explanation by others
022The weak inhomogeneous Duffin–Schaeffer conjectureNumber theoryNumber theory1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
023Patterson’s first moment for cubic Gauss sumsNumber theoryNumber theory111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
024An asymptotic formula for the number of totientsNumber theoryNumber theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
025Short Egyptian fractionsNumber theoryNumber theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedOne explanation by others
026Positive lower density of large prime gapsNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
027Potential integral density on curve character varietiesNumber theoryNumber theory11Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “SUPPORT-ONLY”1 of 1None recordedNo explanation yet
028Uniformly bounded components of Gaussian-prime graphsNumber theoryNumber theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Proofs of selected steps in HOL LightNo explanation yet
029Primitive roots for every admissible integer baseNumber theoryNumber theory2No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
030Modularity of elliptic curves over imaginary quadratic fieldsNumber theoryNumber theory1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
031Uchida’s conjecture for open homomorphisms of Galois groupsNumber theoryNumber theory1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
032The rational Hodge conjecture for CM abelian varietiesAlgebraic and complex geometryThree earlier editions, three withdrawnAlgebraic and complex geometry5No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by othersNine problems reported, not judged by the atlas
033Iitaka subadditivity, variation, and logarithmic additivityAlgebraic and complex geometryAlgebraic and complex geometry515A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
034Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivityAlgebraic and complex geometryTwo earlier editionsAlgebraic and complex geometry14No Lean statement8No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
035Log-canonical threefold abundance in numerical dimension oneAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
036Numerical semiampleness and generalized minimal modelsAlgebraic and complex geometryOne earlier editionAlgebraic and complex geometry4No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
037The ordinary-double-point volume gapAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
038Fujita’s freeness conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
039Nagata’s conjecture and maximal Seshadri constantsAlgebraic and complex geometryAlgebraic and complex geometry42Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
040Bloch’s conjecture for complex surfacesAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
041Hyperkähler SYZ and projective-space basesAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
042Oka classification for minimal compact complex surfaces: Kodaira dimension zero and class VIIAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
043P = W for fixed-determinant SLn moduli spacesAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
044The equivariant cohomological Hikita conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
046Shafarevich counterexamples in dimension two and with large fundamental groupAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
047Zariski cancellation and affine fibrations over the complex numbersAlgebraic and complex geometryAlgebraic and complex geometry111Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
048A characteristic-zero counterexample to Lipman–ZariskiAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
049A stable-coordinate counterexample in four variablesAlgebraic and complex geometryAlgebraic and complex geometry23Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3Proofs of selected steps in HOL Light, exact calculations for finite claimsNo explanation yet
050A counterexample to Griffiths’ positivity conjectureAlgebraic and complex geometryAlgebraic and complex geometry11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
051Kobayashi’s canonical-ampleness conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
052Tangent splittings and product decompositionsAlgebraic and complex geometryThe two readers disagreeAlgebraic and complex geometry22Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”2 of 2None recordedNo explanation yet
053A counterexample to Pixton completeness in ChowAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
054Irrational cubic fourfolds with Hodge-theoretic and categorical K3 associationsAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
055Gepner symmetry and large-volume stability on threefoldsAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
056Termination of projective and Kähler fourfold minimal model programsAlgebraic and complex geometryThree earlier editionsAlgebraic and complex geometry5No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
057Fundamental groups of special complex varieties and root orbifoldsAlgebraic and complex geometryAlgebraic and complex geometry3No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
058Semialgebraic universal covers and bounded domainsAlgebraic and complex geometryAlgebraic and complex geometry212A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
059Counterexamples to Zariski’s multiplicity conjectureAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
060The Global Spherical Shell conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
062Projective contact classification and the LeBrun–Salamon conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
063The generalized Mukai conjectureAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
064Topological triviality of μ-constant surface singularitiesAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
065Virasoro constraints for complete intersections and projective-bundle towersAlgebraic and complex geometryAlgebraic and complex geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
066Bounded klt complements for Fano contractionsAlgebraic and complex geometryAlgebraic and complex geometry211A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “SUPPORT-ONLY”1 of 1None recordedNo explanation yet
067The Campana–Peternell conjecture in dimension sixAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
068Anticanonical nonvanishing in every dimensionAlgebraic and complex geometryAlgebraic and complex geometry7No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
069Global quantum geometric Langlands at irrational levelAlgebraic and complex geometryAlgebraic and complex geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
071Koebe’s circle-domain conjectureReal and complex analysisReal and complex analysis21Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
072Brennan’s conjecture and the integral-means spectrumReal and complex analysisThe two readers disagreeReal and complex analysis23Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”3 of 3None recordedNo explanation yet
073The Falconer distance conjectureReal and complex analysisReal and complex analysis12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
074Kakeya in three and four dimensionsReal and complex analysisReal and complex analysis2No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
075The \(L\log L\) Fourier-convergence conjectureReal and complex analysisReal and complex analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
076Real ultraflat Littlewood polynomials and unbounded binary merit factorsReal and complex analysisReal and complex analysis32Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
077Fourier restriction for positively curved surfacesReal and complex analysisReal and complex analysis2No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
078The three-dimensional Bochner–Riesz conjectureReal and complex analysisReal and complex analysis1No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
079Local smoothing in three dimensionsReal and complex analysisReal and complex analysis1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
080The exact Sobolev endpoint for Schrödinger convergenceReal and complex analysisReal and complex analysis2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
081Riesz transforms and rectifiability in higher codimensionReal and complex analysisReal and complex analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
082Annular variation and dyadic absolute bounds for the triangular Hilbert transformReal and complex analysisReal and complex analysis31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
083Hilbert transforms along Lipschitz directionsReal and complex analysisReal and complex analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
084The geometric case of the Erdős similarity conjectureReal and complex analysisReal and complex analysis21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
085Endpoint Sobolev regularity of centered disk averagesReal and complex analysisReal and complex analysis12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
086An L3 bound for the trilinear Hilbert transformReal and complex analysisReal and complex analysis1No Lean statement3No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
087The Mahler conjectures, functional inequalities and polar-product symplectic widthConvex and metric geometryThe two readers disagreeConvex and metric geometry34Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”4 of 4Exact calculations for finite claimsFive explanations by others
088Sharp projection-body inequalities and a counterexample to simplex maximizationConvex and metric geometryConvex and metric geometry23Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”3 of 3Exact calculations for finite claimsNo explanation yet
089Bounded-distortion L1 embeddings of planar and bounded-treewidth graphsConvex and metric geometryThe two readers disagreeConvex and metric geometry22Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2None recordedNo explanation yet
090Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energyConvex and metric geometryConvex and metric geometry44Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”3 of 4Exact calculations for finite claimsNo explanation yet
091Logarithmic and Lp Brunn–Minkowski inequalities and the B-conjectureConvex and metric geometryConvex and metric geometry11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
092The optimal order of convex-body covering densityConvex and metric geometryConvex and metric geometry22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
093Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measuresConvex and metric geometryConvex and metric geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
094Subpolynomial dimension reduction in LpConvex and metric geometryThe two readers disagreeConvex and metric geometry111All of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
095Hyperbolicity cones without semidefinite liftsConvex and metric geometryConvex and metric geometry31Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
096The Gaussian propeller conjecture in every dimensionConvex and metric geometryThe two readers disagreeConvex and metric geometry111All of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
097The Euclidean Steinitz–Bergström boundConvex and metric geometryThe two readers disagreeConvex and metric geometry11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
098Compact counterexamples to bi-Lipschitz dimension reductionConvex and metric geometryConvex and metric geometry121All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
099The sharp exponential scale of edit-distance distortionConvex and metric geometryConvex and metric geometry341All of itTheir term: “full”All of itTheir term: “MATCHES”4 of 4None recordedNo explanation yet
100Cylinder coverings below the half-area boundConvex and metric geometryConvex and metric geometry43Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3Exact calculations for finite claimsNo explanation yet
101The sharp simplex conjecture for isotropic constantsConvex and metric geometryConvex and metric geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
102The Unique Games Conjecture and optimal approximation thresholdsTheoretical computer scienceTheoretical computer science552All of itTheir term: “full”All of itTheir term: “MATCHES”3 of 5None recordedFour explanations by others
103Exact derandomization of logarithmic space: \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\)Theoretical computer scienceThe two readers disagreeTheoretical computer science11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedOne problem reported, not judged by the atlas
104Quasipolynomial algorithms for mean-payoff, stochastic and parity gamesTheoretical computer scienceTheoretical computer science42Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2Exact calculations for finite claimsNo explanation yet
105Perfect completeness for 2-to-1 gamesTheoretical computer scienceTheoretical computer science112All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
106Hardness of coloring three-colorable graphsTheoretical computer scienceTheoretical computer science111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
107Matrix multiplication with exponent at most 9/4Theoretical computer scienceThe two readers disagreeTheoretical computer science32Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2Exact calculations for finite claimsTwo explanations by othersOne problem reported, not judged by the atlas
108A cubic permanent–determinant lower boundTheoretical computer scienceTheoretical computer science12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
109Integer multiplication below \(n\log n\)Theoretical computer scienceTheoretical computer science1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
110Optimal-order randomized k-server on arbitrary metricsTheoretical computer scienceTheoretical computer science22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedOne problem reported, not judged by the atlas
111One-sample matroid prophet inequalities against an almighty adversaryTheoretical computer scienceTheoretical computer science12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
112Beyond the square-root exponent for depth-three circuitsTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
113Approximate counting and entropy of perfect matchingsTheoretical computer scienceTheoretical computer science261All of itTheir term: “full”All of itTheir term: “MATCHES”6 of 6None recordedNo explanation yet
114Approximate counting of common integer polymatroid basesTheoretical computer scienceTheoretical computer science211Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
115Sampling and counting contingency tables with arbitrary marginsTheoretical computer scienceTheoretical computer science212All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
116Uniform black-box noncommutative identity testing across characteristicsTheoretical computer scienceTheoretical computer science32Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
117Uniform sparsest cut: hardness and semidefinite gapsTheoretical computer scienceTheoretical computer science211Part of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
118Bin packing and unbounded configuration-LP gapsTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Exact calculations for finite claimsNo explanation yet
119The Courtade–Kumar and Hellinger conjecturesTheoretical computer scienceTheoretical computer science22Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2Exact calculations for finite claimsNo explanation yet
120Almost-linear-time exact matching and prescribed-degree factors in general graphsTheoretical computer scienceTheoretical computer science1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
121Almost-linear approximation of edit distanceTheoretical computer scienceTheoretical computer science111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
122Quantitative trace-reconstruction bounds with a uniform decoderTheoretical computer scienceTheoretical computer science31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedOne explanation by others
124Polynomial-time scheduling on three identical machinesTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
125The metric k-median approximation threshold and recoveryTheoretical computer scienceTheoretical computer science24Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”4 of 4None recordedNo explanation yet
126Exponential semidefinite complexity of perfect matchingTheoretical computer scienceTheoretical computer science12Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — DECLARED”2 of 2None recordedNo explanation yet
127Average sensitivity of polynomial threshold functionsTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
128A factor-two approximation for shortest common superstringTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
129Exponential state costs for two-way automataTheoretical computer scienceTheoretical computer science23Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3None recordedNo explanation yet
130Exact Fourier transforms below \(n\log n\)Theoretical computer scienceTheoretical computer science22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2Exact calculations for finite claimsTwo explanations by others
131Rapid mixing of graph switches for every degree sequenceTheoretical computer scienceThe two readers disagreeTheoretical computer science11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
132A superquadratic separation of sensitivity and block sensitivityTheoretical computer scienceTheoretical computer science11Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
133The computational complexity of Weisfeiler–Leman refinementTheoretical computer scienceTheoretical computer science44Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”4 of 4None recordedNo explanation yet
134Generalized star height at most threeTheoretical computer scienceTheoretical computer science31Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
135Homogeneous depth-five lower bounds for iterated matrix multiplicationTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
136A quasilinear PCP theorem for PPADTheoretical computer scienceTheoretical computer science1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
137One-tape time simulation in two-fifths-power spaceTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
138Subset Sum in \(O(2^{0.49n})\) timeTheoretical computer scienceTheoretical computer science2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
139Subpolynomial query complexity for log-concave samplingTheoretical computer scienceTheoretical computer science11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
140Memory–sample lower bounds for noiseless Gaussian regressionTheoretical computer scienceTheoretical computer science68Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”8 of 8None recordedNo explanation yet
141Existential–universal real sentences in the counting hierarchyTheoretical computer scienceTheoretical computer science1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
142Deterministic polynomial factorization over prime fieldsTheoretical computer scienceTheoretical computer science1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
143Hilbert’s sixteenth problem: uniform bounds for limit cyclesDynamical systems and ergodic theoryDynamical systems and ergodic theory21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedOne problem reported, not judged by the atlas
144Banach’s simple Lebesgue-spectrum problemDynamical systems and ergodic theoryDynamical systems and ergodic theory111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
145Rokhlin’s multiple-mixing problemDynamical systems and ergodic theoryDynamical systems and ergodic theory113All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne problem reported, not judged by the atlas
146Positive metric entropy for the standard mapDynamical systems and ergodic theoryDynamical systems and ergodic theory13Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3None recordedNo explanation yet
147The near-boundary Birkhoff conjectureDynamical systems and ergodic theoryDynamical systems and ergodic theory2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
148The entropy-rate dimension formula for self-similar measuresDynamical systems and ergodic theoryDynamical systems and ergodic theory12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
149Classwise permanence for weakly reversible mass-action systemsDynamical systems and ergodic theoryDynamical systems and ergodic theory21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
150Weak mixing of triangular billiards with an irrational angleDynamical systems and ergodic theoryDynamical systems and ergodic theory21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1Proofs of selected steps in HOL LightNo explanation yet
151A C1 counterexample to the entropy conjectureDynamical systems and ergodic theoryDynamical systems and ergodic theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
152Zero entropy does not guarantee a smooth positive-volume modelDynamical systems and ergodic theoryDynamical systems and ergodic theory11Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
153Arithmetic classification and non-Pisot singularity for Bernoulli convolutionsDynamical systems and ergodic theoryDynamical systems and ergodic theory1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
154Pointwise multiple ergodic averages for mixing transformationsDynamical systems and ergodic theoryDynamical systems and ergodic theory4No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
155A counterexample to periodic tiling in dimension threeCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
156Borsuk’s conjecture fails in dimension nineCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne explanation by others
157Graph coloring, clique minors, and Colin de Verdière invariantsCombinatoricsCombinatorics32Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”2 of 2Exact calculations for finite claimsNo explanation yet
158The Euclidean plane cannot be colored with five colorsCombinatoricsCombinatorics12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2Proofs of selected steps in HOL Light, exact calculations for finite claimsTwo explanations by othersFour problems reported, not judged by the atlas
159Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi boundsCombinatoricsCombinatorics111Part of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedOne explanation by others
160Superexponential van der Waerden numbersCombinatoricsCombinatorics111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
161Counterexamples to Sidorenko’s conjecture and the forcing conjectureCombinatoricsCombinatorics11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
162Counterexamples to Ryser’s covering conjectureCombinatoricsCombinatorics23Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”3 of 3Exact calculations for finite claimsNo explanation yet
164Hindman’s finite sums and products conjectureCombinatoricsCombinatorics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
165The Harary–Hill and Zarankiewicz crossing-number formulasCombinatoricsCombinatorics22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
166The higher-dimensional Erdős distinct-distances conjectureCombinatoricsCombinatorics1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
167Planar distinct distances and unit-distance boundsCombinatoricsCombinatorics22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
168Combinatorial invariance of Kazhdan–Lusztig polynomialsCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
169Shareshian–Wachs elementary positivityCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedTwo problems reported, not judged by the atlas
170Sharp logarithmic exponents for off-diagonal Ramsey numbersCombinatoricsCombinatorics221All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
171The hypercube Ramsey conjectureCombinatoricsCombinatorics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
172Classification of finite Euclidean Ramsey configurationsCombinatoricsCombinatorics17Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”7 of 7None recordedNo explanation yet
173Seymour’s second-neighborhood conjectureCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
174Deterministic construction of strong thin spanning treesCombinatoricsCombinatorics22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
175Talagrand’s expectation thresholds, discrete convexity, and graph decompositionsCombinatoricsCombinatorics322Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
176The second Kahn–Kalai conjecture with an edge-count boundCombinatoricsCombinatorics111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
177Bounded-degree coboundary expandersCombinatoricsThe two readers disagreeCombinatorics11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
178Deterministic nonbipartite Ramanujan graphs in every fixed degreeCombinatoricsCombinatorics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
179The circulant Hadamard and Barker-sequence conjecturesCombinatoricsThe two readers disagreeCombinatorics12Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”2 of 2None recordedNo explanation yet
180Barnette’s Hamiltonian-cycle conjectureCombinatoricsThe two readers disagreeCombinatorics11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
181The Erdős–Gallai cycle-decomposition conjectureCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
182Power savings for intersective polynomial differences and prime argumentsCombinatoricsCombinatorics31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
183Power savings for planar halving lines and k-setsCombinatoricsCombinatorics11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
184Correspondence coloring with a fixed forbidden subgraphCombinatoricsCombinatorics21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
185Counterexamples to infinite matroid intersection and packing/coveringCombinatoricsCombinatorics12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
186Uniform influence and sharp thresholds for graph and hypergraph propertiesCombinatoricsCombinatorics21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
187Snaky in 21 Maker movesCombinatoricsCombinatorics13Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3Exact calculations for finite claimsNo explanation yet
188The sharp terminal leave in random triangle removalCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Proofs of selected steps in HOL LightNo explanation yet
189Cycle–clique Ramsey numbersCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”0 of 1Exact calculations for finite claimsNo explanation yet
190Polynomial removal fails for ordered binary matricesCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Exact calculations for finite claimsNo explanation yet
191A power improvement in the Heilbronn triangle lower boundCombinatoricsCombinatorics11Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
192Boolean functions violate the square-root degree bound by arbitrary factorsCombinatoricsCombinatorics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
193Serre’s intersection-multiplicity conjectureAlgebraAlgebra1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
194Lech’s multiplicity conjectureAlgebraAlgebra111A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
195A counterexample to the small Cohen–Macaulay module conjectureAlgebraAlgebra111A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “SUPPORT-ONLY”1 of 1None recordedOne explanation by others
196A counterexample to Kaplansky’s zero-divisor conjectureAlgebraAlgebra111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Proofs of selected steps in HOL Light, exact calculations for finite claimsNo explanation yet
197A torsion-free group algebra that is not directly finiteAlgebraAlgebra44Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”4 of 4Exact calculations for finite claimsNo explanation yet
198A counterexample to finitistic-dimension finitenessAlgebraAlgebra121All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
199Counterexamples to Auslander–Reiten, Tachikawa and related homological conjecturesAlgebraAlgebra221Part of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”2 of 2Exact calculations for finite claimsNo explanation yet
200Eisenbud–Green–Harris and lex-plus-powersAlgebraAlgebra2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
201A counterexample to Kurosh’s division-ring problemAlgebraAlgebra1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
202The blockwise Alperin weight conjectureAlgebraAlgebra1No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
203Donovan’s conjecture over fields and complete mixed-characteristic DVRsAlgebraAlgebra2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
204Tensor saturation for even spin groupsAlgebraAlgebra1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
205Saxl’s conjecture and universal tensor squaresAlgebraAlgebra22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 2Exact calculations for finite claimsNo explanation yet
206Finite lattice representation and undecidabilityAlgebraAlgebra21Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
207The ℓ¹-Bass conjecture for all discrete groupsAlgebraAlgebra221Part of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2None recordedNo explanation yet
208Finite symmetric tensor categories and the Verlinde towerAlgebraAlgebra1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
209Integral counterexamples to Gersten’s conjectureAlgebraAlgebra2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
210Foulkes' conjecture for sixth powers and quadratic stabilizationAlgebraAlgebra21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
211The geometric phase diagram, diffusion, and spectra of random planar mapsProbability and statistical mechanicsProbability and statistical mechanics71Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
212Planar first-passage geometry and the absence of bigeodesicsProbability and statistical mechanicsProbability and statistical mechanics22Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
213Critical percolation on every quasi-transitive graphProbability and statistical mechanicsProbability and statistical mechanics22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedOne explanation by others
214The Benjamini–Schramm nonuniqueness conjectureProbability and statistical mechanicsProbability and statistical mechanics121All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
215Canonical \(O(3)\) continuum limit and exact \(O(4)\) mass asymptoticsProbability and statistical mechanicsProbability and statistical mechanics51Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
216Critical and near-critical XY scaling and BKT universalityProbability and statistical mechanicsProbability and statistical mechanics6No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
217The low-temperature Sherrington–Kirkpatrick fluctuation lawProbability and statistical mechanicsProbability and statistical mechanics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
218Conformal universality for weakly interacting and random-bond Ising modelsProbability and statistical mechanicsProbability and statistical mechanics611A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedOne explanation by others
219GOE bulk universality for regular graphs with weak Anderson disorderProbability and statistical mechanicsProbability and statistical mechanics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
220Directional zero–one laws beyond iid environments and iid ballisticityProbability and statistical mechanicsProbability and statistical mechanics33Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”3 of 3None recordedNo explanation yet
221The Mézard–Parisi formula for diluted spin glassesProbability and statistical mechanicsProbability and statistical mechanics111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne explanation by others
222Perceptron free energies and microscopic jamming exponentsProbability and statistical mechanicsProbability and statistical mechanics431Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”3 of 3Exact calculations for finite claimsNo explanation yet
223Random-cluster interfaces: critical, disordered, thermal, and natural-time scalingProbability and statistical mechanicsProbability and statistical mechanics6No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
224Critical and quenched near-critical universality for Poisson–Voronoi percolationProbability and statistical mechanicsProbability and statistical mechanics3No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
225Gaussian free field limits throughout the balanced six-vertex regimeProbability and statistical mechanicsProbability and statistical mechanics1No Lean statement4No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
226The double-dimer loop ensemble converges to CLE4Probability and statistical mechanicsProbability and statistical mechanics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
227Critical SK autocorrelation processes and dynamics across the temperature transitionProbability and statistical mechanicsProbability and statistical mechanics85Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”5 of 5Exact calculations for finite claimsNo explanation yet
228Continuum phase transitions for radial pair potentialsProbability and statistical mechanicsProbability and statistical mechanics23Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3None recordedNo explanation yet
229Exact three- and four-state reconstruction thresholds and four-state tree capacityProbability and statistical mechanicsProbability and statistical mechanics32Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”2 of 2Exact calculations for finite claimsNo explanation yet
230Exact Hausdorff gauges for SLEProbability and statistical mechanicsProbability and statistical mechanics21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
231The free uniform spanning forest is a factor of IIDProbability and statistical mechanicsProbability and statistical mechanics121All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
232Gaussian fields and interfaces for triangular-lattice Lipschitz heightsProbability and statistical mechanicsThree earlier editionsProbability and statistical mechanics3No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
233The joint critical Ashkin–Teller current limitProbability and statistical mechanicsOne earlier editionProbability and statistical mechanics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
234All-temperature pressure of orthogonally invariant Ising spin glassesProbability and statistical mechanicsProbability and statistical mechanics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
235Limiting random SAT thresholds, sharp variance and computabilityProbability and statistical mechanicsProbability and statistical mechanics441Part of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”4 of 4None recordedNo explanation yet
236The exact factor-of-IID threshold for free Ising spins on treesProbability and statistical mechanicsProbability and statistical mechanics111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
237The three-quarter exponent for honeycomb self-avoiding walkProbability and statistical mechanicsProbability and statistical mechanics134Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”4 of 4None recordedNo explanation yet
238Optimal logarithmic mixing of the Thorp shuffleProbability and statistical mechanicsProbability and statistical mechanics1213Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”13 of 13Exact calculations for finite claimsFour problems reported, not judged by the atlas
239Sharp singularity rates for symmetric random sign matricesProbability and statistical mechanicsProbability and statistical mechanics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
240Shelah’s eventual categoricity and the prescribed-threshold obstructionMathematical logicMathematical logic21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
241Rigidity of the Turing degreesMathematical logicMathematical logic11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
242Single-fold Diophantine representations and undecidability under an at-most-one-solution promiseMathematical logicThe two readers disagreeMathematical logic11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
243Separating choiceless counting from polynomial time and witnessed choiceMathematical logicMathematical logic22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
244The Partition Principle does not imply ChoiceMathematical logicMathematical logic12Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”2 of 2None recordedNo explanation yet
245Weak normalization implies strong normalization in pure type systemsMathematical logicMathematical logic11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
246Cannon’s conjectureGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
247An infinite finitely presented residually finite 2-group and a finitely presented nil algebraGroup theoryGroup theory21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
248Thompson’s group F is nonamenableGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
249A finitely generated Eilenberg–Ganea counterexampleGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
250Boone–Higman embeddings with higher finitenessGroup theoryGroup theory331All of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3None recordedNo explanation yet
251Amenability, unitarizability, and strong Ulam stabilityGroup theoryGroup theory222Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
252A torsion-free hyperbolic group that is neither residually finite nor linear over any fieldGroup theoryThe two readers disagreeGroup theory11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
253An infinite finitely presented simple amenable groupGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
254Classifying spaces and geometric obstructions for Artin groupsGroup theoryGroup theory33Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”3 of 3None recordedNo explanation yet
255Quasi-isometric recognition of virtually polycyclic groupsGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
256Nonsingular systems of equations over arbitrary groupsGroup theoryGroup theory21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
257A hyperbolic group without a geometric CAT(0) actionGroup theoryGroup theory11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
258Gersten’s conjecture and virtual compact specialness of one-relator groupsGroup theoryGroup theory2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
259A group without fixed priceGroup theoryGroup theory1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
260Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensionsMathematical physicsMathematical physics131Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedTwo explanations by others
261Localization and delocalization in the Anderson modelMathematical physicsMathematical physics21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedOne explanation by others
262Sharp finite-matrix Lieb–Thirring inequalities and all equality casesMathematical physicsMathematical physics31Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedOne explanation by others
263The ionization and generalized ionization conjecturesMathematical physicsMathematical physics322Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedOne explanation by others
264Strong cosmic censorship near two-ended Kerr dataMathematical physicsMathematical physics3No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
265Area laws and tensor networks for two-dimensional gapped systemsMathematical physicsMathematical physics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
266Exactly three mutually unbiased bases in dimension sixMathematical physicsMathematical physics22Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — DECLARED”2 of 2Exact calculations for finite claimsTwo explanations by othersOne problem reported, not judged by the atlas
267Positive-temperature Bose–Einstein condensation and exact quantum depletionMathematical physicsMathematical physics51Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedOne explanation by others
268The spin-one Haldane gapMathematical physicsMathematical physics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsTwo explanations by others
269Uniform Laughlin gap and stability under bounded scalar disorderMathematical physicsMathematical physics24Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”4 of 4Exact calculations for finite claimsTwo explanations by others
270Threshold and positive-energy bound states of the BFSS matrix modelMathematical physicsMathematical physics2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
271Bloch’s law, its lattice correction, and the spherical magnetization lawMathematical physicsMathematical physics41Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedTwo explanations by others
272Entanglement without distillable secret keyMathematical physicsMathematical physics12Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”2 of 2Exact calculations for finite claimsTwo explanations by others
273The entropy photon-number inequalityMathematical physicsThe two readers disagreeMathematical physics11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedOne explanation by others
274Parity is not in QAC0Mathematical physicsThe two readers disagreeMathematical physics22Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2None recordedTwo explanations by others
275QMA-hardness of continuum Coulomb energyMathematical physicsMathematical physics21Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”0 of 1None recordedTwo explanations by others
276Classical capacity of generalized amplitude dampingMathematical physicsMathematical physics11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedTwo explanations by others
277Threshold repetition for entangled gamesMathematical physicsMathematical physics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne explanation by others
278Failure of Kohn–Sham ensemble representationMathematical physicsMathematical physics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
279Exact quantum factoring over a fixed finite gate setMathematical physicsMathematical physics11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedTwo explanations by others
280Unitary vertex operator algebras and conformal netsMathematical physicsMathematical physics11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedOne explanation by others
281QAOA attains the SK optimum in the thermodynamic-first limitMathematical physicsMathematical physics22Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”2 of 2Exact calculations for finite claimsTwo explanations by others
282From scale symmetry to local conformal symmetry in four-dimensional QFTMathematical physicsMathematical physics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
283Polynomial-time unitary synthesis from a Boolean oracleMathematical physicsMathematical physics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
284The optimal quartic separation between randomized and quantum queriesMathematical physicsMathematical physics1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
285Counterexamples to Baum–Connes and Kadison–KaplanskyOperator algebrasOperator algebras3No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
286Rigidity and arithmetic of lattice von Neumann algebrasOperator algebrasOperator algebras2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
287Isomorphism of the free group factorsOperator algebrasThe two readers disagreeOperator algebras113All of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedOne explanation by others
288Kadison’s similarity conjectureOperator algebrasOperator algebras122All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
289Strong Kadison–Kastler stability and its spatial boundariesOperator algebrasOperator algebras31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
290Relative bicentralizers and modular spectral recoveryOperator algebrasOperator algebras21Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
291Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stabilityOperator algebrasOperator algebras412A supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
292Kirchberg’s \(\mathcal O_2\) norm-ultrapower embedding problemOperator algebrasOperator algebras11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
293Invariant projections, hyperinvariant subspaces, and transitive algebrasOperator algebrasOperator algebras26Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”6 of 6None recordedNo explanation yet
294Kaplansky’s quasitrace conjecture and failure of tensor-product stable finitenessOperator algebrasOperator algebras12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
295The Kadison–Ringrose cohomology conjectureOperator algebrasOperator algebras11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
296The generator problem for finite factorsOperator algebrasOperator algebras12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
297A ZFC counterexample to Naimark’s problemOperator algebrasOperator algebras11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne explanation by othersTwo problems reported, not judged by the atlas
298Two notions of free entropy differ even when both are finiteOperator algebrasOperator algebras11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
299The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stabilityOperator algebrasOperator algebras111Part of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
300Approximation and quadratic strong-operator pavingOperator algebrasOperator algebras2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
301Trace cones and Razak–Jacelon stabilizationOperator algebrasOperator algebras11Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “SUPPORT-ONLY”1 of 1None recordedNo explanation yet
302Radius of comparison equals half the mean dimensionOperator algebrasOperator algebras2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
303Weak pure infiniteness and Cuntz-algebra absorptionOperator algebrasThe two readers disagreeOperator algebras12Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”2 of 2None recordedNo explanation yet
304The Hilbert–Smith conjecture in every dimensionTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedTwo explanations by others
305Four-dimensional disk embedding and Wall’s conjectureTopologyTopology3No Lean statement2No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
306The purely cosmetic surgery conjectureTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
307Failure of rational injectivity for maximal coarse assemblyTopologyTopology21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”0 of 1None recordedNo explanation yet
308Finite Smith–Toda complexes at every heightTopologyTopology2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
309The Kervaire invariant problem at the prime threeTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
310Quillen’s conjecture in rational homologyTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
311The Hovey–Strickland and Chai conjecturesTopologyTopology1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
312The Grothendieck homotopy hypothesisTopologyTopology111A supporting or different resultTheir term: “supporting-only”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedOne explanation by othersOne problem reported, not judged by the atlas
313Finite generation for the \(K(n)\)-local sphereTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
314Cyclic length and chromatic fixed-point lossTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
315The four-dimensional Singer conjectureTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
316Curtis’s conjectureTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
317Thomason model structures in all strict higher dimensionsTopologyTopology11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
318Chromatic splitting: filtrations and counterexamplesTopologyTopology5No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
319Counterexamples to finite generation at chromatic height twoTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
320Nonhomeomorphic closed aspherical four-manifoldsTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
321A counterexample to Wall’s finite D(2) problemTopologyTopology1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
322Tingley’s sphere-isometry problemFunctional analysisFunctional analysis111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
323Independence of the separable quotient problemFunctional analysisFunctional analysis11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
324Lipschitz equivalent Banach spaces need not be linearly isomorphicFunctional analysisFunctional analysis22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
325The complete Crouzeix conjectureFunctional analysisFunctional analysis25Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”5 of 5Proofs of selected steps in HOL LightOne explanation by othersOne problem reported, not judged by the atlas
326The cotype–cotype conjecture under the approximation propertyFunctional analysisThe two readers disagreeFunctional analysis11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — UNDECLARED”1 of 1None recordedNo explanation yet
327Markov type characterizes superreflexivityFunctional analysisFunctional analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
328Nonexpansive fixed points in reflexive Banach spacesFunctional analysisFunctional analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
329A counterexample to metric-entropy dualityFunctional analysisFunctional analysis11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
330A uniformly discrete counterexample to bounded approximation in Lipschitz-free spacesFunctional analysisFunctional analysis12Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
331Reflexive midpoint convexity and diamond distortionFunctional analysisFunctional analysis77Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”7 of 7None recordedNo explanation yet
332Metric Markov cotype of ℓ1 and Hilbert-space Lipschitz extensionFunctional analysisFunctional analysis1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
333Smooth isometric immersions of surfaces into ℝ4Differential geometryDifferential geometry11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
334A smooth surface metric with no local isometric immersion in ℝ3Differential geometryDifferential geometry111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
335Gromov’s integral scalar-curvature bound for simplicial volumeDifferential geometryDifferential geometry2No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedOne problem reported, not judged by the atlas
336Spectral scalar curvature, Urysohn width, and macroscopic dimensionDifferential geometryDifferential geometry3No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne problem reported, not judged by the atlas
337Sharp Cartan–Hadamard isoperimetry and rigidityDifferential geometryDifferential geometry22Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”2 of 2None recordedNo explanation yet
338Yau’s uniformization conjectureDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
339Katok’s entropy rigidity conjectureDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
340A counterexample to the nearby Lagrangian conjectureDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
341Donaldson’s hypersymplectic deformation conjectureDifferential geometryOne earlier editionDifferential geometry1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
342Donaldson’s tamed-to-compatible conjectureDifferential geometryOne earlier editionDifferential geometry111All of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
343Symplectic ball packing in higher dimensionsDifferential geometryDifferential geometry121All of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
344The metric Blaschke conjectureDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
345Infinitely many closed geodesics on Riemannian spheres and closed three-manifoldsDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
346Sharp singular-set bounds for stationary integral varifoldsDifferential geometryDifferential geometry2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
347Counterexamples to stable-Morse and strong Arnold fixed-point boundsDifferential geometryDifferential geometry51Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
348Nonnegative-curvature Einstein classification and an L2 topological gapDifferential geometryDifferential geometry31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1Exact calculations for finite claimsNo explanation yet
349The Solomon–Yau least-volume conjectureDifferential geometryDifferential geometry1No Lean statement1No Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
350Yau’s nodal bounds: surfaces and higher dimensionsDifferential geometryDifferential geometry33Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNDECLARED”3 of 3None recordedNo explanation yet
351Scalar curvature and finite-time Ricci-flow singularitiesDifferential geometryDifferential geometry3No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
352A finite-time singularity of Calabi flowDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementExact calculations for finite claimsNo explanation yet
353Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexampleDifferential geometryDifferential geometry21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1Proofs of selected steps in HOL LightNo explanation yet
354The isoperimetric profile of the cubic three-torusDifferential geometryDifferential geometry11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Proofs of selected steps in HOL Light, exact calculations for finite claimsNo explanation yet
355Unique tangent flows at the first surface singularityDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
356Gigli’s characterization of Alexandrov curvatureDifferential geometryDifferential geometry21Not citedA supporting or different resultTheir term: “supporting-only”A supporting or different resultTheir term: “DIFFERENT”1 of 1None recordedNo explanation yet
357Bi-Lipschitz coordinates at every regular RCD pointDifferential geometryDifferential geometry1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
358A three-manifold without conjugate points or nonpositive curvatureDifferential geometryDifferential geometry11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
359Negative Kähler curvature without bounded holomorphic coordinatesDifferential geometryDifferential geometry21Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
360Weak MTW curvature gives convexity and regular optimal transportDifferential geometryDifferential geometry22Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”2 of 2None recordedNo explanation yet
361Failure of integer-degree harmonic dimension comparisonDifferential geometryDifferential geometry21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — UNLINKED”1 of 1Exact calculations for finite claimsNo explanation yet
362Global smoothness for relativistic Vlasov–MaxwellPartial differential equationsPartial differential equations11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne explanation by others
363Nonuniqueness with local conservation for the hard-sphere Boltzmann equationPartial differential equationsPartial differential equations21Not citedPart of itTheir term: “weaker-statement”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
364Kinetic limits and fluctuations over the Boltzmann lifespanPartial differential equationsPartial differential equations2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
365Joint metric and connection recovery from one boundary patchPartial differential equationsPartial differential equations31Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — UNLINKED”1 of 1None recordedNo explanation yet
366The planar Mumford–Shah regularity conjecture and local weak-L4 gradient boundsPartial differential equationsPartial differential equations1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
367The critical dimension for the one-phase Bernoulli problemPartial differential equationsPartial differential equations11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsNo explanation yet
368The three-dimensional Ball–Evans approximation problemPartial differential equationsPartial differential equations2No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet
369The hot spots conjecture for simply connected planar domainsPartial differential equationsPartial differential equations11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1Proofs of selected steps in HOL LightNo explanation yet
370The Lane–Emden and Hénon–Lane–Emden conjecturesPartial differential equationsPartial differential equations11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
371Stable blowup for the defocusing Schrödinger equationPartial differential equationsThe two readers disagreePartial differential equations11Not citedAll of itTheir term: “full”Part of itTheir term: “NARROWER — DECLARED”1 of 1Exact calculations for finite claimsOne problem reported, not judged by the atlas
372Global uniqueness in smooth isotropic elasticityPartial differential equationsPartial differential equations11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedNo explanation yet
373Nonattainment of the three-marginal Coulomb Monge problemPartial differential equationsPartial differential equations11Not citedPart of itTheir term: “partial”Part of itTheir term: “NARROWER — DECLARED”1 of 1None recordedNo explanation yet
374Sharp one-third stability of Brenier mapsPartial differential equationsPartial differential equations11Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”1 of 1None recordedOne problem reported, not judged by the atlas
375De Giorgi’s conjecture in dimension eightPartial differential equationsPartial differential equations1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedOne explanation by others
376Universal computation in forced Navier–Stokes flowsPartial differential equationsOne earlier editionPartial differential equations96Not citedAll of itTheir term: “full”All of itTheir term: “MATCHES”6 of 6None recordedOne explanation by others
377Interior \(C^{1,\alpha}\) regularity for infinity-harmonic functionsPartial differential equationsPartial differential equations1No Lean statementNot citedNo Lean statementNo Lean statementNo Lean statementNone recordedNo explanation yet

Where a careful reading is most useful

The first 25 of the 172 Lean statements with a specific reason for a careful reading, each with its reasons.

  1. Elementary positivity for natural unit interval graphs Family 169: Shareshian–Wachs elementary positivity
    • The configuration names no theorem: it checks a definition whose type carries the claim, so read that definition's type and body.
    • 1 definition hole: Comparator compares it by name and type only, so a reader checks what each solution body means.
  2. Nine routing-density and representation estimates Family 238: Optimal logarithmic mixing of the Thorp shuffle
    • The AI draft scope reading could not tell from OpenAI's note how much of a paper's theorem this file states.
    • The draft scope reading depends on mathematics a specialist should settle.
    • 357 local vocabulary declarations to read.
  3. Exact equality of deterministic and randomized logarithmic space Family 103: Exact derandomization of logarithmic space: \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\)
    • 20 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  4. Stable self-similar blowup and positive-probability Gaussian blowup Family 371: Stable blowup for the defocusing Schrödinger equation
    • 3 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  5. Counterexample to harmonic dimension comparison Family 361: Failure of integer-degree harmonic dimension comparison
    • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.
    • States its claim through an axiom in the challenge file; check what the configuration compares.
  6. One-third stability of Brenier maps and sharpness Family 374: Sharp one-third stability of Brenier maps
    • 12 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  7. Squared-logarithmic randomized $k$-server on arbitrary metrics Family 110: Optimal-order randomized k-server on arbitrary metrics
    • 9 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  8. Counterexample to Naimark's problem in ZFC Family 297: A ZFC counterexample to Naimark’s problem
    • 7 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  9. Area-controlled end replacement and Schwarzschild equality examples Family 260: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions
    • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.
    • 310 local vocabulary declarations to read.
  10. Row–column overlap on occupied boards Family 238: Optimal logarithmic mixing of the Thorp shuffle
    • 5 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  11. Failure of rational injectivity for ordinary coarse assembly Family 307: Failure of rational injectivity for maximal coarse assembly
    • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.
    • 216 local vocabulary declarations to read.
  12. Mixing of every finite order for one mixing transformation Family 145: Rokhlin’s multiple-mixing problem
    • 4 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  13. Kirchberg–Rørdam character criterion Family 299: The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability
    • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.
    • 146 local vocabulary declarations to read.
  14. One-sided angle bound for signed spin types Family 238: Optimal logarithmic mixing of the Thorp shuffle
    • 3 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.
  15. No proper five-coloring Family 158: The Euclidean plane cannot be colored with five colors
    • 1 definition hole: Comparator compares it by name and type only, so a reader checks what each solution body means.
  16. Perfect-matching entropy bound Family 113: Approximate counting and entropy of perfect matchings
    • The draft scope reading depends on mathematics a specialist should settle.
  17. Projection estimates and memory–precision bounds Family 140: Memory–sample lower bounds for noiseless Gaussian regression
    • The draft scope reading depends on mathematics a specialist should settle.
  18. Barnette's Hamiltonian-cycle conjecture Family 180: Barnette’s Hamiltonian-cycle conjecture
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  19. Bounded-treewidth graph metrics in $L_1$ Family 089: Bounded-distortion L1 embeddings of planar and bounded-treewidth graphs
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  20. Brennan and inverse-square integral-means bounds Family 072: Brennan’s conjecture and the integral-means spectrum
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  21. Sharp endpoint divergence Family 072: Brennan’s conjecture and the integral-means spectrum
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  22. Classification of circulant Hadamard orders Family 179: The circulant Hadamard and Barker-sequence conjectures
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  23. Bounded-degree coboundary expanders in dimensions at least three Family 177: Bounded-degree coboundary expanders
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  24. Cotype–cotype equivalence with approximation property Family 326: The cotype–cotype conjecture under the approximation property
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.
  25. Entropy photon-number inequality for finite-energy bosonic inputs Family 273: The entropy photon-number inequality
    • Two independent readers, MathVet and cert-machine, disagree on whether this family's challenges state its headline; a specialist reading would settle it.

Points per reason, highest first: a configuration with no theorem target 100; definition holes 90 plus one per hole; unclear draft scope 85; a draft scope reading needing a specialist 80; independent readers disagreeing on the family 75; both independent readers finding less than the headline where the atlas's AI draft says the file states a paper's theorem as the paper does 72; a target theorem shared with another file 70; an axiom in the challenge 60; no local vocabulary but OpenAI imports 50; 100 or more local declarations 20 plus one per hundred (capped); a family in which the AI draft finds no statement of a paper's theorem as the paper does 5. Ties go alphabetically. The order allocates reading; it is no verdict.

The order allocates reading time and says nothing about whether any statement or proof is correct.