Learning path

Each declaration appears after its prerequisites.

OAI.AbhyankarSathaye.exists_noncoordinate_polynomial@ComparatorChallenges/AbhyankarSathaye.lean Challenge statement: Affine-space zero fibre without an ambient coordinate
OAI.AffineBernstein.hessian Coordinate Hessian
OAI.AffineBernstein.cofactorHessian The coefficient U^{ij} = det(D²u) (D²u)^{-1}_{ij}
OAI.AffineBernstein.affineWeight The classical determinant weight; in particular, this is not a generalized exponent
OAI.AffineBernstein.AffineMaximalOn
OAI.AffineBernstein.graphPathLength Length on [0,1] for g_x(v,v) = ‖v‖² + (Du_x v)², the metric induced by the Euclidean graph embedding x ↦ (x,u(x))
OAI.AffineBernstein.graphEDist The intrinsic extended distance: infimum of lengths of C¹ paths in the domain
OAI.AffineBernstein.EuclideanGraphComplete Sequential completeness for the induced Euclidean path metric
OAI.AffineBernstein.graph The graph, regarded as an affine subset of R^{n+1}
OAI.AffineBernstein.affine_bernstein@ComparatorChallenges/AffineBernstein.lean Challenge statement: Affine Bernstein theorem in dimensions 3 to 9 after OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete
OAI.StrongThinTree.MultiGraph A finite loopless multigraph with individually indexed edge copies
OAI.StrongThinTree.MultiGraph.cut The selected edges crossing a vertex cut
OAI.StrongThinTree.MultiGraph.Connected Connectivity of a chosen edge set
OAI.StrongThinTree.MultiGraph.SpanningTree A minimally connected spanning edge set
OAI.StrongThinTree.MultiGraph.EdgeConnected At least $k$ edge copies cross every nontrivial cut
OAI.CurrentKS.frame A self-delimiting Boolean-list frame
OAI.CurrentKS.encodeNat A framed bit encoding of a natural number
OAI.CurrentKS.StackAction The three permitted updates to one Boolean stack
OAI.CurrentKS.StackAction.apply Execute one action on one Boolean stack
OAI.CurrentKS.Instruction One transition of a finite multi-stack machine
OAI.CurrentKS.Instruction.halt The default halting instruction
OAI.CurrentKS.Machine A finite Boolean-stack machine with designated input and output stacks
OAI.CurrentKS.Config A machine state together with all current stacks
OAI.CurrentKS.topCode Encode a stack's visible head as one of three cases
OAI.CurrentKS.headsCode Combine all visible stack heads into one base-$3$ number
OAI.CurrentKS.Machine.step Perform one deterministic machine transition
OAI.CurrentKS.Machine.init Initialize the machine from an encoded input
OAI.CurrentKS.Machine.run Run a machine for exactly the supplied fuel
OAI.AlgorithmicThinTrees.ExplicitInput A thin-tree instance with every edge copy listed explicitly
OAI.AlgorithmicThinTrees.BinaryInput A multiplicity-compressed multigraph input
OAI.AlgorithmicThinTrees.BinaryInput.Edge One concrete edge copy in a compressed binary input
OAI.AlgorithmicThinTrees.BinaryInput.edgeEquiv Number all expanded binary-input edge copies
OAI.AlgorithmicThinTrees.BinaryInput.graph Expand compressed multiplicities into a loopless multigraph
OAI.AlgorithmicThinTrees.Input Either an explicit or multiplicity-compressed graph instance
OAI.AlgorithmicThinTrees.ExplicitInput.encode Serialize an explicitly listed multigraph
OAI.AlgorithmicThinTrees.BinaryInput.encode Serialize a multiplicity-compressed multigraph
OAI.AlgorithmicThinTrees.Input.encode Tag and serialize either input representation
OAI.AlgorithmicThinTrees.Input.length The bit length used by the polynomial runtime bound
OAI.AlgorithmicThinTrees.Input.n Read the vertex count from either input branch
OAI.AlgorithmicThinTrees.Valid The admissible $k$-edge-connected inputs
OAI.AlgorithmicThinTrees.ThinTree A spanning tree uniformly thin across every cut
OAI.AlgorithmicThinTrees.ExplicitInput.encodeEdges Serialize a list of explicit edge indices
OAI.AlgorithmicThinTrees.BinaryInput.encodeEdges Serialize selected copies from a compressed multigraph
OAI.AlgorithmicThinTrees.BinaryInput.selected Convert decoded binary-input edge copies to multigraph indices
OAI.AlgorithmicThinTrees.TreeOutput The output bits encode a duplicate-free thin spanning tree
OAI.AlgorithmicThinTrees.GoodOutput A valid tree output with a canonical one-vertex case
OAI.AlgorithmicThinTrees.AlgorithmicStrongThinTrees The complete deterministic polynomial-time strong thin-tree proposition
OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees@ComparatorChallenges/AlgorithmicThinTrees.lean Challenge statement: A deterministic polynomial-time strong thin-tree construction
OAI.GAD.entropy The spectral definition of -Tr(P log P), with 0 log 0 = 0
OAI.GAD.tensorKraus Tensor products of the single-site Kraus operators, with the full Kraus index
OAI.GAD.channel The memoryless n-fold generalized amplitude-damping channel
OAI.GAD.Ensemble All finite ensembles, without any product or purity restriction
OAI.GAD.Code An unrestricted n-use quantum code with one collective output POVM
OAI.GAD.Achievable The liminf rate condition written as its eventual lower-bound characterization
OAI.GAD.capacity Operational unassisted classical capacity, not a definition by regularization
OAI.GAD.phaseValue Holevo value of the explicit 2^n equiprobable product signals
OAI.GAD.main@ComparatorChallenges/AmplitudeDamping.lean Challenge statement: Exact unassisted classical capacity of generalized amplitude damping
OAI.ArnoldCounterexample.Q3 The literal projective quadric sum z_j^2 = 0 in CP^4
OAI.ArnoldCounterexample.Horizontal Horizontal lifts of the real tangent of Q3 at [z]
OAI.ArnoldCounterexample.omega The restricted Fubini--Study form, evaluated on horizontal lifts
OAI.ArnoldCounterexample.LocalFunctionLift A local smooth extension of the pullback of h to the unit isotropic cone
OAI.ArnoldCounterexample.IsCritical dh_q = 0, expressed using all local lifts, independent of normal extensions
OAI.ArnoldCounterexample.criticalNumber The minimum critical number, including degenerate functions (ENat allows infinity)
OAI.ArnoldCounterexample.HamiltonianPath An explicit smooth lift of a Hamiltonian isotopy, with inverse and generator
OAI.ArnoldCounterexample.HasDegenerateFixedPoint Eigenvalue 1 in the derivative on the quotient tangent, not an ambient spurious vertical eigenvector
OAI.ArnoldCounterexample.main@ComparatorChallenges/ArnoldCounterexample.lean Challenge statement: Counterexamples to stable-Morse and strong Arnold fixed-point bounds
OAI.ArtinCAT0.main@ComparatorChallenges/ArtinCAT0.lean Challenge statement: An explicit Artin group with no geometric $\mathrm{CAT}(0)$ action
OAI.HarmonicArtin.ParabolicIntersections.conjugate@ComparatorChallenges/ArtinParabolicIntersections.lean g P g⁻¹, with membership expressed without existential witnesses
OAI.HarmonicArtin.ParabolicIntersections.IsParabolic Conjugates of standard subgroups, with no spherical-type restriction
OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic An isometric non-elementary acylindrical action on a geodesic Gromov-hyperbolic metric space
OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible No nontrivial partition has every cross label equal to two
OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections@ComparatorChallenges/ArtinParabolicIntersections.lean Challenge statement: Parabolic intersections, closures, and structural consequences
OAI.HarmonicArtin.ParabolicIntersections.unconditional_arbitrary_intersections@ComparatorChallenges/ArtinParabolicIntersections.lean Challenge statement: Parabolic intersections, closures, and structural consequences
OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_closure@ComparatorChallenges/ArtinParabolicIntersections.lean Challenge statement: Parabolic intersections, closures, and structural consequences
OAI.HarmonicArtin.ParabolicIntersections.unconditional_nonclique_dynamics@ComparatorChallenges/ArtinParabolicIntersections.lean Challenge statement: Parabolic intersections, closures, and structural consequences
OAI.AsymptoticallyMinimalLittlewood.main@ComparatorChallenges/AsymptoticallyMinimalLittlewood.lean Challenge statement: Asymptotically minimal Littlewood maximum
OAI.AtomicTriangular.sharp_gaussian_minorants_atomic@ComparatorChallenges/AtomicGaussian.lean Challenge statement: Sharp Gaussian minorants from an atomic certificate
OAI.ArExplicit.Statement.main@ComparatorChallenges/AuslanderReiten.lean Challenge statement: Auslander–Reiten counterexample
OAI.BackwardIntertwiners.direct_algebra_corollary@ComparatorChallenges/BackwardIntertwiners.lean Challenge statement: Quasinilpotent operator with transitive commutant
OAI.BoxTransport.Routing.balanced_box_routing@ComparatorChallenges/BalancedBoxRouting.lean Challenge statement: Incompressible transport of solid boxes
OAI.Balanced.main_result@ComparatorChallenges/BalancedRyser.lean Challenge statement: Balanced Ryser counterexamples at prime orders
OAI.BalancedTransport.balanced_three_stack_realization@ComparatorChallenges/BalancedThreeStack.lean Challenge statement: Finite computation in a balanced zero-data fluid flow
OAI.HigherDimensionalBallPacking.main_theorem@ComparatorChallenges/BallPacking.lean Challenge statement: Exact criterion for higher-dimensional symplectic ball packings
OAI.HigherDimensionalBallPacking.packing_necessity@ComparatorChallenges/BallPackingNecessity.lean Challenge statement: Necessity of the volume and pairwise capacity inequalities
OAI.Barnette.PlaneEmbedding A topological plane drawing of a simple graph, with no crossings
OAI.Barnette.Planar Planarity means existence of a crossing-free topological plane embedding
OAI.Barnette.ThreeVertexConnected Deleting any set of at most two vertices leaves a connected graph of order at least two
OAI.Barnette.HasHamiltonianCycle A single spanning cycle, not a possibly disconnected spanning 2-factor
OAI.Barnette.MainStatement Cubic bipartite three-vertex-connected plane graphs have a Hamiltonian cycle
OAI.Barnette.main@ComparatorChallenges/BarnetteHamiltonian.lean Challenge statement: Barnette's Hamiltonian-cycle conjecture
OAI.TorsionFreeBass.TorsionFree A group is torsion-free when its only finite-order element is the identity
OAI.TorsionFreeBass.augmentation The sum of coefficients, or augmentation, of the complex group algebra
OAI.TorsionFreeBass.canonicalTrace The canonical trace is the coefficient of the identity
OAI.TorsionFreeBass.matrixTrace The matrix trace obtained by applying the canonical trace to each diagonal entry
OAI.TorsionFreeBass.augmentedMatrix Entrywise augmentation
OAI.TorsionFreeBass.rawAugmentationRank The augmentation rank on the free abelian group of idempotents, before imposing isomorphism and direct-sum relations
OAI.TorsionFreeBass.augmentationRank@ComparatorChallenges/BassTorsionFree.lean The integer-valued augmentation rank on the usual idempotent presentation of algebraic K₀: on a generator it is the complex dimension of the augmented image
OAI.TorsionFreeBass.traceK0 Coefficient at the identity class of the Hattori--Stallings trace on K₀
OAI.TorsionFreeBass.torsion_free_corollary@ComparatorChallenges/BassTorsionFree.lean Challenge statement: Trace rank and characteristic-zero Kaplansky idempotents for torsion-free groups
OAI.BassTrace.RightProjective.bassTraceModules_vanishing_and_support@ComparatorChallenges/BassTrace.lean Challenge statement: Complex Bass trace vanishing and support
OAI.Percolation.BenjaminiSchramm.full_main@ComparatorChallenges/BenjaminiSchramm.lean Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs
OAI.Percolation.BenjaminiSchramm.critical_laws@ComparatorChallenges/BenjaminiSchramm.lean Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs
OAI.Percolation.BenjaminiSchramm.cayley_main@ComparatorChallenges/BenjaminiSchramm.lean Challenge statement: Nonuniqueness phase and critical laws on quasi-transitive graphs
OAI.Bernoulli.Test Compactly supported smooth real tests in the open set
OAI.Bernoulli.WeakGradient Distributional gradient, tested in every constant direction
OAI.Bernoulli.H1 H¹(D), with its weak gradient
OAI.Bernoulli.H10 H¹₀(D) is H¹-closure of C∞ compactly supported functions
OAI.Bernoulli.H1Loc Ballwise H¹_loc, on an open set (balls have compact closure inside D)
OAI.Bernoulli.energy The exact volume-one Bernoulli energy, not just Dirichlet energy
OAI.Bernoulli.LocalMinimizer Full ballwise local comparison
OAI.Bernoulli.GlobalMinimizer Nonnegative global minimizer, with all centers and all positive radii
OAI.Bernoulli.Flat Flatness is a.e
OAI.Bernoulli.nonflat_in_seven@ComparatorChallenges/BernoulliNonflatInSeven.lean Challenge statement: The critical dimension for the one-phase Bernoulli problem
OAI.WeakMTWTransport.cost Squared-distance cost with factor one half
OAI.WeakMTWTransport.euclideanVolumeFactor Calibration of Hausdorff measure to Euclidean volume
OAI.WeakMTWTransport.metricVolume Riemannian volume calibrated to Lebesgue measure in Euclidean space
OAI.WeakMTWTransport.AdmissibleDensity Almost-everywhere measurable probability densities between fixed bounds
OAI.WeakMTWTransport.densityMeasure Multiplication by a density, ignoring exceptional negative values on null sets
OAI.WeakMTWTransport.IsOptimalMap Optimality for the Monge minimization problem
OAI.WeakMTWTransport.BiHolderEstimate The two global estimates have the very same exponent and constant
OAI.WeakMTWTransport.IsGeodesicWithInitialData Complete affinely parametrized geodesic with prescribed initial tangent
OAI.WeakMTWTransport.riemannianExp Evaluation at time one of the geodesic determined by initial data
OAI.WeakMTWTransport.injectivityDomain The open injectivity domain, defined by extendible minimizing vectors
OAI.WeakMTWTransport.mtw The Ma–Trudinger–Wang fourth derivative with factor -3/2
OAI.WeakMTWTransport.WeakMTW Weak MTW only at interior velocities and only for orthogonal test vectors
OAI.WeakMTWTransport.uniform_biHolder_transport@ComparatorChallenges/BiholderTransport.lean Challenge statement: Uniform bi-Hölder optimal transport
OAI.BinPackingGap.main_results@ComparatorChallenges/BinPackingGap.lean Challenge statement: Bin packing and unbounded configuration-LP gaps
OAI.TreeEdit.EditStep A single unit-cost insertion, deletion, or substitution at any position
OAI.TreeEdit.EditScript An edit script with no restriction on intermediate word lengths
OAI.TreeEdit.ed Ordinary unit-cost edit distance
OAI.TreeEdit.RealL1 The full infinite-dimensional real ℓ₁ space
OAI.TreeEdit.BinaryLower.distortion@ComparatorChallenges/BinaryEditLower.lean The product of the two maximal pairwise distance ratios
OAI.TreeEdit.BinaryLower.c1@ComparatorChallenges/BinaryEditLower.lean The infimum over every injective map into the full real sequence space ℓ₁
OAI.TreeEdit.binary_lower_bound@ComparatorChallenges/BinaryEditLower.lean Challenge statement: Binary edit-distance distortion lower bound
OAI.BinaryMatching.deterministic_approximate_counting@ComparatorChallenges/BinaryMatching.lean Challenge statement: Deterministic approximate matching count
OAI.BinaryCoordinateSweeps.Slot The positions of a binary deck of dimension d
OAI.BinaryCoordinateSweeps.coordinateLayer Independent switches on the edges parallel to one coordinate
OAI.BinaryCoordinateSweeps.binarySweep The coordinate layers are applied in increasing coordinate order
OAI.BinaryCoordinateSweeps.totalVariation Half the unnormalized sum of absolute probability-mass differences
OAI.BinaryCoordinateSweeps.convolutionPower The law of independent repetitions, with the empty product at the identity
OAI.BinaryCoordinateSweeps.UniformSweepMixingTarget A single number of sweeps works uniformly over deterministic initial decks
OAI.binary_sweep_contraction_and_mixing@ComparatorChallenges/BinarySweep.lean Challenge statement: Binary sweep contraction and mixing
OAI.Zarankiewicz.mainTarget_proof@ComparatorChallenges/BipartiteCrossing.lean Challenge statement: Crossing number of complete bipartite graphs
OAI.BogomolovPop.main_graph_injective@ComparatorChallenges/BogomolovPopInjectivity.lean Challenge statement: Function-field reconstruction from Milnor K-theory and Galois data
OAI.BoltzmannNonuniqueness.sphereArea Ordinary surface area, rather than normalized probability on the sphere
OAI.BoltzmannNonuniqueness.torusRepresentative A representative in the fundamental half-open unit cube, used only to evaluate periodic derivatives
OAI.BoltzmannNonuniqueness.FiniteEntropyDatum The convention 0 |log 0| = 0 is automatic in this real-valued moment
OAI.BoltzmannNonuniqueness.extendedEntropyProduction Lower semicontinuous extension of (A-B) log(A/B) on the nonnegative quadrant
OAI.BoltzmannNonuniqueness.Renormalization The renormalizations of Definition 2.1, with the right derivative at zero
OAI.BoltzmannNonuniqueness.KineticTest A smooth test, periodic in the spatial variable and compact in time and velocity
OAI.BoltzmannNonuniqueness.MassTest Smooth local mass tests have no velocity cutoff, since their velocity dependence is introduced only by the transport derivative
OAI.BoltzmannNonuniqueness.AdmissibleGlobal Full global admissibility, including both separately renormalized collision terms, local mass, total momentum, and the every-time energy and entropy inequalities
OAI.BoltzmannNonuniqueness.StrongEarly Additional regularity asserted on the common initial interval
OAI.BoltzmannNonuniqueness.nonuniqueness@ComparatorChallenges/BoltzmannNonuniqueness.lean Challenge statement: Nonuniqueness with local conservation for the hard-sphere Boltzmann equation
OAI.FiniteAlgebraicEnvelopes.main@ComparatorChallenges/BooneHigman.lean Challenge statement: Boone–Higman equivalence
OAI.BorsukNine.main_theorem@ComparatorChallenges/BorsukNine.lean Challenge statement: Borsuk's covering assertion fails in dimension nine
OAI.BoundedRecovery.bounded_recovery@ComparatorChallenges/BoundedRecovery.lean Challenge statement: Relative bicentralizers and modular spectral recovery
OAI.BoundedTreePotentials.TreeCalculus.main_counterexample@ComparatorChallenges/BoundedTreePotentials.lean Challenge statement: Tree-potential midpoint convexity and renorming obstruction
OAI.BoundedTreewidthL1.walkLength Sum of the given positive real edge lengths along a graph walk
OAI.BoundedTreewidthL1.HasL1Embedding A map to genuine finite-dimensional real ℓ₁, not just a cut pseudometric
OAI.BoundedTreewidthL1.main_theorem@ComparatorChallenges/BoundedTreewidthL1.lean Challenge statement: Bounded-treewidth graph metrics in $L_1$
OAI.Problem358.E@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.uniformMeasure@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.IsSupported@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.IsCoupling@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.quadraticPlanCost@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.wasserstein2@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.graphPlan@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.IsQuadraticOptimalMap@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.IsUniqueQuadraticOptimalMap@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.mapL2Dist@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.cube@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.HasExactlyThreeAtoms@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.one_third_stability@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Problem358.one_third_exponent_is_sharp@ComparatorChallenges/Brenier.lean Challenge statement: Sharp one-third stability of Brenier maps
OAI.Brennan.main_theorem@ComparatorChallenges/Brennan.lean Challenge statement: Brennan and inverse-square integral-means bounds
OAI.Brennan.Sharp.sharp_endpoints@ComparatorChallenges/BrennanSharp.lean Challenge statement: Sharp endpoint divergence
OAI.BufferedIsing.FiniteGraph A finite graph given by its edge list
OAI.BufferedIsing.conditionalProb Conditional probability of σ_I=a, with σ_J=b and σ_F=τ prescribed
OAI.BufferedIsing.keptEdges Edges remaining after DELETION, not pinning, of F
OAI.BufferedIsing.comparisonRel Open-edge adjacency together with the two separate terminal identifications
OAI.BufferedIsing.comparisonSetoid The equivalence closure implements components of the contracted open graph
OAI.BufferedIsing.fkWeight Zero-field FK weight with q=2 and p_e=1-exp(-2 K_e)
OAI.BufferedIsing.qZero Choose any i in I and j in J
OAI.BufferedIsing.mixtureProb Any probability mixture of source prescriptions
OAI.BufferedIsing.finite_graph_comparison@ComparatorChallenges/BufferedIsing.lean Challenge statement: Conformal universality for weakly interacting and random-bond Ising models
OAI.C0Absorption.main_result@ComparatorChallenges/C0Absorption.lean Challenge statement: Bi-Lipschitz absorption of $c_0$
OAI.Problem340.exists_C1_entropy_counterexample@ComparatorChallenges/C1EntropyCounterexample.lean Challenge statement: A C1 counterexample to the entropy conjecture
OAI.CHObstruction.main@ComparatorChallenges/CHObstruction.lean Challenge statement: Shelah's eventual categoricity and the prescribed-threshold obstruction
OAI.CKSSourceExterior.area_controlled_end_replacement@ComparatorChallenges/CKSBondiPenrose.lean Challenge statement: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions
OAI.CKSMain.schwarzschild_equality_examples@ComparatorChallenges/CKSBondiPenrose.lean Challenge statement: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions
OAI.CannonRelease.CayleyData.ThinTriangles A uniform thinness constant for geodesic triangles in the Cayley graph
OAI.CannonRelease.BasedRay Based geodesic rays, parametrized at integer times
OAI.CannonRelease.raySetoid Finite synchronous distance, equivalent to asymptoticity for based rays
OAI.CannonRelease.HyperbolicThree The upper-half-space model of hyperbolic three-space
OAI.CannonRelease.hyperbolicIsometries The full isometry group, including orientation-reversing isometries
OAI.CannonRelease.cannon@ComparatorChallenges/CannonGeometricAction.lean Challenge statement: Cannon's conjecture
OAI.CartierSections.isCompact_closedChartFieldRetraction_cone@ComparatorChallenges/CartierChartCompactnessSupport.lean Challenge statement: Bounded klt complements for Fano contractions
OAI.InternalCatalan.catalan_irrational@ComparatorChallenges/Catalan.lean Challenge statement: Catalan's constant is irrational
OAI.Percolation.arbitrary_cayley@ComparatorChallenges/CayleyPercolation.lean Challenge statement: Nonuniqueness for every nonamenable Cayley graph
OAI.KirchbergRordam.character_criterion@ComparatorChallenges/CharacterCriterion.lean Challenge statement: The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability
OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_allSeams@ComparatorChallenges/CharacterVarietiesAllSeamsSupport.lean Challenge statement: Potential integral density on curve character varieties
OAI.CPTSeparation.main@ComparatorChallenges/ChoicelessPolynomialTime.lean Challenge statement: Polynomial-time query outside choiceless polynomial time
OAI.CirculantHadamard.exists_iff_order_one_or_four@ComparatorChallenges/CirculantHadamard.lean Challenge statement: Real circulant Hadamard matrices have order one or four
OAI.ClassicalON.main@ComparatorChallenges/ClassicalON.lean Challenge statement: Canonical $`O(3)`$ continuum limit and exact $`O(4)`$ mass asymptotics
OAI.CliqueFreeLog.logarithmic_independence_bound@ComparatorChallenges/CliqueFreeLog.lean Challenge statement: Correspondence coloring with a fixed forbidden subgraph
OAI.CoarseAssembly.bounded_geometry_graph_counterexample_unconditional@ComparatorChallenges/CoarseAssembly.lean Challenge statement: Failure of rational injectivity for maximal coarse assembly
OAI.CoboundaryExpanders.Complex A finite abstract simplicial complex with every labelled vertex present
OAI.CoboundaryExpanders.Complex.facesOf Faces of dimension i have exactly i + 1 vertices
OAI.CoboundaryExpanders.Complex.Pure Exact purity: top faces exist and every face lies in a top face
OAI.CoboundaryExpanders.Complex.Connected Connectedness of the nonempty one-skeleton
OAI.CoboundaryExpanders.Complex.weight Weights are normalized counts of incident top-dimensional faces
OAI.CoboundaryExpanders.Complex.norm Weighted support norm
OAI.CoboundaryExpanders.Complex.coboundary Simplicial coboundary over F₂
OAI.CoboundaryExpanders.Complex.coboundaries Actual coboundaries, with constant cochains in degree zero
OAI.CoboundaryExpanders.Complex.distance Distance in the weighted support norm; on a nonempty finite set it is a minimum
OAI.CoboundaryExpanders.Complex.topDegree Number of top-dimensional faces incident to a vertex
OAI.CoboundaryExpanders.MainStatement Both constants are uniform over the sequence, all degrees below d, and all cochains
OAI.CoboundaryExpanders.main@ComparatorChallenges/CoboundaryExpanders.lean Challenge statement: Bounded-degree coboundary expanders
OAI.common_bases_fpras@ComparatorChallenges/CommonBasesFPRAS.lean Challenge statement: Approximate counting of common integer polymatroid bases
OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_with_ordinary_extras@ComparatorChallenges/CommutingDerivations.lean Challenge statement: Commuting locally nilpotent derivations
OAI.CompactBanach.main@ComparatorChallenges/CompactBanach.lean Challenge statement: Compact counterexamples in infinite-dimensional Banach spaces
OAI.Paper170.complete_graph_crossing_number@ComparatorChallenges/CompleteCrossing.lean Challenge statement: Crossing number of complete graphs
OAI.CompleteCrouzeix.main@ComparatorChallenges/CompleteCrouzeix.lean Challenge statement: The complete Crouzeix inequality has sharp constant two
OAI.ComplexCancellation.main@ComparatorChallenges/ComplexCancellation.lean Challenge statement: Zariski cancellation and affine fibrations over the complex numbers
OAI.ScalarConductivity.main_nonuniqueness@ComparatorChallenges/Conductivity.lean Challenge statement: Joint metric and connection recovery from one boundary patch
OAI.ThreeManifold.main_theorem@ComparatorChallenges/ConjugatePoints.lean Challenge statement: A three-manifold without conjugate points or nonpositive curvature
OAI.MatchingFPRAS.encodeNat Binary numeral followed by a delimiter
OAI.MatchingFPRAS.encodeRat A rational encoded by its reduced numerator and positive denominator
OAI.MatchingFPRAS.RandomMachine A uniform randomized Post-Turing machine: a single finite transition table
OAI.MatchingFPRAS.tick A halted configuration is absorbing
OAI.MatchingFPRAS.run Bounded execution on a finite prefix of the random tape
OAI.ContingencyTables.Algorithms.alphabetSize_neZero The tape alphabet has positive cardinality
OAI.ContingencyTables.Algorithms.OutputsTable A halted tape contains the row-major binary matrix encoding
OAI.ContingencyTables.Algorithms.BoundedSamplingStatement Paper 200-01, Theorem main(i): bounded runtime on every random tape and total variation at most 2⁻ᵏ, with freely varying dimensions
OAI.ContingencyTables.Algorithms.ExactSamplingStatement Documented declaration: ExactSamplingStatement
OAI.ContingencyTables.Algorithms.CountingStatement Paper 200-02, Theorem main
OAI.ContingencyTables.boundedSampling@ComparatorChallenges/ContingencyTables.lean Challenge statement: Sampling and counting contingency tables with arbitrary margins
OAI.ContingencyTables.exactSampling@ComparatorChallenges/ContingencyTables.lean Challenge statement: Sampling and counting contingency tables with arbitrary margins
OAI.ContingencyTables.counting@ComparatorChallenges/ContingencyTables.lean Challenge statement: Sampling and counting contingency tables with arbitrary margins
OAI.ContinuousCircleWeight.main_theorem@ComparatorChallenges/ContinuousCircleWeight.lean Challenge statement: Continuous-weight invariant-projection counterexample
OAI.ContinuumCoulomb.unit_coulomb_qmaHard@ComparatorChallenges/ContinuumCoulombHardness.lean Challenge statement: QMA-hardness of continuum Coulomb energy
OAI.ContinuumCoulomb.binary_coulomb_qmaHard@ComparatorChallenges/ContinuumCoulombHardness.lean Challenge statement: QMA-hardness of continuum Coulomb energy
OAI.ContinuumTemperature.main_theorem@ComparatorChallenges/ContinuumTransition.lean Challenge statement: Temperature singularity over a density interval
OAI.CoordinateSweeps.orderedProduct Coordinate zero acts first
OAI.CoordinateSweeps.Grid.Allowed The side lengths are in [R, R²], where the single global scale is R = 2^r
OAI.CoordinateSweeps.Grid.Holes Full disjoint paths, including every boundary of the ordered sweep
OAI.CoordinateSweeps.Grid.Holes.stabilizer The symmetric group on the unmarked input sites
OAI.CoordinateSweeps.Grid.Holes.residual A reference completion identifies the free input and output sites
OAI.CoordinateSweeps.Grid.choiceWeight Independent line permutations with law (1-z) U + z B
OAI.CoordinateSweeps.schattenMoment Unnormalized Schatten 2q moment, without division by the dimension
OAI.CoordinateSweeps.logMoment The logarithm of a zero moment is minus infinity
OAI.CoordinateSweeps.all_grid_moment@ComparatorChallenges/CoordinateSweeps.lean Challenge statement: Conditional coordinate-sweep moment estimate
OAI.CoordinateSweeps.conditional_main@ComparatorChallenges/CoordinateSweeps.lean Challenge statement: Conditional coordinate-sweep moment estimate
OAI.ThorpNine.Harmonic.Thorp.LowPlanes.regular_trace_smoothing@ComparatorChallenges/CoordinateTrace.lean Challenge statement: Regular trace smoothing and full-permutation mixing
OAI.Cotype.mainTarget_proved@ComparatorChallenges/Cotype.lean Challenge statement: The cotype–cotype conjecture under the approximation property
OAI.Problem356.coulomb_counterexample_and_equal_infima@ComparatorChallenges/CoulombCounterexample.lean Challenge statement: Nonattainment of the three-marginal Coulomb Monge problem
OAI.CoulombAtom.generalized_ionization@ComparatorChallenges/CoulombIonization.lean Challenge statement: Generalized Coulomb ionization-energy asymptotics
OAI.NeutralAtom.generalized_outer_radii@ComparatorChallenges/CoulombRadii.lean Challenge statement: Asymptotic outer-electron radii of neutral atoms
OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment@ComparatorChallenges/CourtadeKumar.lean Challenge statement: Courtade–Kumar inequality and attainment
OAI.CoveringOrder.LatticeCover Actual discrete full-rank lattice coverings; no assumed density theorem
OAI.CoveringOrder.orderBounds The finite real comparison scale, viewed in extended nonnegative reals
OAI.CoveringOrder.OptimalOrder All four extremal quantities have common absolute positive comparison constants
OAI.CoveringOrder.optimal_order@ComparatorChallenges/CoveringDensity.lean Challenge statement: Optimal order for translative and lattice covering-density suprema
OAI.CriticalPercolation.BondGraph An undirected graph with labelled bonds, including loops and parallel bonds
OAI.CriticalPercolation.BondGraph.openGraph The graph of retained bonds
OAI.CriticalPercolation.BondGraph.fullGraph The underlying connectivity graph with every bond retained
OAI.CriticalPercolation.BondGraph.LocallyFinite Local finiteness counts bonds, not just distinct neighbors
OAI.CriticalPercolation.BondGraph.Aut Automorphisms preserve the vertex and bond structure, including multiplicities
OAI.CriticalPercolation.BondGraph.QuasiTransitive Finitely many vertex orbits under the full automorphism group
OAI.CriticalPercolation.BondGraph.cluster Finite open paths, including the path of length zero, define the open cluster
OAI.CriticalPercolation.BondGraph.percolates The event that at least one open cluster is infinite
OAI.CriticalPercolation.BondGraph.law Independent retention with parameter p ∈ [0,1] of each labelled bond
OAI.CriticalPercolation.BondGraph.criticalProbability The infimum of parameters with positive probability of an infinite cluster
OAI.CriticalPercolation.BondGraph.no_percolation_at_criticality@ComparatorChallenges/CriticalPercolation.lean Challenge statement: No infinite cluster at the critical probability
OAI.CriticalSK.linearRayleigh The supremum of variance divided by the rate-one Dirichlet form over nonzero linear spin observables
OAI.CriticalSK.continuousGoodMass Gibbs mass of realized initial states still farther than 1 / 4 from equilibrium
OAI.CriticalSK.discreteGoodMass@ComparatorChallenges/CriticalSK.lean Gibbs mass of realized initial states still farther than 1 / 4 after k attempts
OAI.CriticalSK.realized_equilibrium_initial_states@ComparatorChallenges/CriticalSK.lean Challenge statement: Equilibrium starts, covariance, and mixing lower bounds
OAI.CriticalSK.covariance_and_linear_tests@ComparatorChallenges/CriticalSK.lean Challenge statement: Equilibrium starts, covariance, and mixing lower bounds
OAI.CriticalSK.critical_mixing_lower_bounds@ComparatorChallenges/CriticalSK.lean Challenge statement: Equilibrium starts, covariance, and mixing lower bounds
OAI.CriticalSK.critical_mixing_bounds@ComparatorChallenges/CriticalSKMixing.lean Challenge statement: Critical SK mixing bounds
OAI.CriticalStrip.critical_strip_mass@ComparatorChallenges/CriticalStripMass.lean Challenge statement: Critical honeycomb strip mass and displacement moment
OAI.CriticalZ3.critical_no_infinite@ComparatorChallenges/CriticalZ3.lean Challenge statement: No infinite critical clusters on $\mathbb Z^3$
OAI.CrouzeixHilbert.hilbert@ComparatorChallenges/CrouzeixHilbert.lean Challenge statement: Complete sharp Crouzeix theorem on arbitrary Hilbert spaces
OAI.CubicTorus.quotientMap The quotient R³ → R³/Z³ in orthonormal coordinates
OAI.CubicTorus.fundamentalCube One unit-volume fundamental domain; its boundary is immaterial to integration
OAI.CubicTorus.torusVolume The Riemannian volume measure of the unit flat torus
OAI.CubicTorus.latticeVector An integer lattice vector in the Euclidean cover
OAI.CubicTorus.AdmissibleField The smooth vector fields on the flat torus with pointwise length at most one, expressed as Z³-periodic fields on its Euclidean cover
OAI.CubicTorus.divergence Euclidean divergence in the orthonormal coordinate frame
OAI.CubicTorus.perimeter De Giorgi perimeter, allowed to be infinite; no regularity of E is imposed
OAI.CubicTorus.FinitePerimeter Finite-perimeter measurable regions, including all null-set modifications
OAI.CubicTorus.IsMinimizerAt A global perimeter minimizer under the prescribed volume constraint
OAI.CubicTorus.candidateProfile The candidate unit-torus isoperimetric profile
OAI.CubicTorus.canonicalBall Canonical centered ball
OAI.CubicTorus.canonicalTube Canonical tube around the shortest closed geodesic in coordinate direction 0
OAI.CubicTorus.canonicalSlab Canonical slab of width V between two parallel coordinate tori
OAI.CubicTorus.CongruentAE Equality of regions up to ambient flat isometry and a null set
OAI.CubicTorus.SmallStandardRegion Exactly the closed phase ranges, so adjacent types are BOTH included at ties
OAI.CubicTorus.StandardRegionAt The equality class at every interior volume, including complementation
OAI.CubicTorus.unit_cubic_isoperimetric@ComparatorChallenges/CubicTorus.lean Challenge statement: The isoperimetric profile of the cubic three-torus
OAI.CycleClique.thm_main@ComparatorChallenges/CycleCliqueRamsey.lean Challenge statement: Cycle–clique Ramsey numbers
OAI.ErdosGallai.erdos_gallai@ComparatorChallenges/CycleDecomposition.lean Challenge statement: The Erdős–Gallai cycle-decomposition conjecture
OAI.RuledApproximation.SmoothNear No boundary hypothesis is included in this neighborhood regularity predicate
OAI.RuledApproximation.HyperbolicAt In dimension two these two distinct nonzero eigenvalues are all the eigenvalues
OAI.CylinderCovering.fourPaperMain@ComparatorChallenges/CylinderCovering.lean Challenge statement: Cylinder-covering counterexamples and companion approximations
OAI.ExactModuli.Cofinite Closed linear subspaces of finite codimension
OAI.ExactModuli.averagedIncrement Averaged increment for directions of norm at least one
OAI.ExactModuli.EquivalentNorm Two-sided comparison makes this seminorm a genuine norm equivalent to the original
OAI.ExactModuli.Daugavet Every rank-one operator has the form ell.smulRight v
OAI.ExactModuli.measureDistance Convergence-in-measure distance on L1 equivalence classes
OAI.ExactModuli.MeasurePrecompactBall Finite covers of the entire unit ball in convergence-in-measure distance
OAI.ExactModuli.UnitSliceProperty Every nonempty unit-ball slice contains an almost antipodal unit vector
OAI.ExactModuli.KWOmega The countable product of unit intervals
OAI.ExactModuli.exact_main@ComparatorChallenges/DaugavetModuli.lean Challenge statement: Exact asymptotic moduli and a Daugavet example
OAI.ExactModuli.kadets_werner_existence@ComparatorChallenges/DaugavetModuli.lean Challenge statement: Exact asymptotic moduli and a Daugavet example
OAI.ExactModuli.exact_example@ComparatorChallenges/DaugavetModuli.lean Challenge statement: Exact asymptotic moduli and a Daugavet example
OAI.DefocusingNLS.sobolevProduct@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.DefocusingNLS.sobolevOddPower@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.DefocusingNLS.schrodingerFlow@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.DefocusingNLS.stable_blowup@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.DefocusingNLS.gaussian_blowup@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.DefocusingNLS.gaussian_not_almost_sure_global@ComparatorChallenges/DefocusingNLS.lean Challenge statement: Stable blowup for the defocusing Schrödinger equation
OAI.TuringRigidity.ManuscriptMain.rigidity@ComparatorChallenges/DegreeRigidity.lean Challenge statement: Rigidity of the Turing degrees
OAI.DeligneDrinfeld.main@ComparatorChallenges/DeligneDrinfeld.lean Challenge statement: The Deligne–Drinfeld conjecture
OAI.Problem335.main@ComparatorChallenges/DepthFive.lean Challenge statement: Homogeneous depth-five lower bounds for iterated matrix multiplication
OAI.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound@ComparatorChallenges/DepthThree.lean Challenge statement: Beyond the square-root exponent for depth-three circuits
OAI.DiamondDistortion.SegmentSystem.Family The represented disjoint families in the definition of the primal segment norm
OAI.DiamondDistortion.SegmentSystem.Family.test Segment testing as a Euclidean-valued linear map
OAI.DiamondDistortion.SegmentSystem.singletonFamily Singleton families ensure that the segment seminorm separates points
OAI.DiamondDistortion.SegmentSystem.Dual Its full real continuous dual
OAI.DiamondDistortion.SegmentSystem.coordinateFinite Coordinate evaluation on finite arrays, bounded by the singleton test
OAI.DiamondDistortion.SegmentSystem.unitFinite Primal unit coordinate and its canonical image in the completion
OAI.DiamondDistortion.SegmentSystem.CoordinatePredual The norm-closed coordinate span, not the full infinite-tree dual
OAI.DiamondDistortion.intervalSystem A finite interval in an ancestral order
OAI.DiamondDistortion.Ancestry An ancestral partial order: the predecessors of any vertex form a chain
OAI.DiamondDistortion.Ancestry.segments Nonempty finite intervals for an ancestral order
OAI.DiamondDistortion.infiniteAncestry Prefix order on all finite words, explicitly distinct from their lexicographic order
OAI.DiamondDistortion.infiniteSegments The infinite-height tree of all finite words; this includes the empty root
OAI.DiamondDistortion.Diamond.Edge Stage edges, retaining their parent, child number, and side
OAI.DiamondDistortion.Diamond.Vertex At every replacement every parent edge receives countably many distinct new vertices
OAI.DiamondDistortion.Diamond.graph The undirected replacement graph
OAI.DiamondDistortion.Diamond.distance Final edges have length 2⁻ᵏ: this is the shortest-path metric of the normalized graph
OAI.DiamondDistortion.headline_all_pairs@ComparatorChallenges/DiamondDistortion.lean Challenge statement: All-pairs diamond distortion bound
OAI.DilutedSpinGlass.InteractionSample One interaction together with its factorization witness: theta,a,b,f
OAI.DilutedSpinGlass.Admissible Exactly the standing hypotheses (model:integrability through positivity)
OAI.DilutedSpinGlass.logWeight Minus the Hamiltonian, with all index choices including repetitions
OAI.DilutedSpinGlass.pressure F_N, using an explicit uniform average over the independent index labels
OAI.DilutedSpinGlass.appendSpin Append the distinguished cavity spin in the last position
OAI.DilutedSpinGlass.Hierarchy Nested probability laws: H_0=R and H_{j+1}=P(H_j), with weak topologies
OAI.DilutedSpinGlass.logMean Logarithmic form of the conditional power means T_0 using independent message labels
OAI.DilutedSpinGlass.trialLog Expectation over the root laws eta_0 of each independent message label
OAI.DilutedSpinGlass.Exponents Admissible exponents 0<m_1<...<m_r<1; vacuous at r=0
OAI.DilutedSpinGlass.functional The exact finite-depth cavity functional B_r
OAI.DilutedSpinGlass.mezard_parisi@ComparatorChallenges/DilutedSpin.lean Challenge statement: The Mézard–Parisi formula for diluted spin glasses
OAI.DimensionTen.exists_channel_fin21@ComparatorChallenges/DimensionTenChannel.lean Challenge statement: PPT channel on dimension 21 whose square is not entanglement breaking
OAI.DimensionTen.main_pair@ComparatorChallenges/DimensionTenPair.lean Challenge statement: Dimension-ten PPT pair with non-entanglement-breaking composition
OAI.DirectCrouzeix.complete_crouzeix@ComparatorChallenges/DirectCrouzeix.lean Challenge statement: Complete Crouzeix inequality and sharpness
OAI.DirectCrouzeix.uniform_sharpness@ComparatorChallenges/DirectCrouzeix.lean Challenge statement: Complete Crouzeix inequality and sharpness
OAI.DirectedFeedback.natBits Unary self-delimiting natural numbers
OAI.DirectedFeedback.pairBits The explicit framing used for an input and its NP certificate
OAI.DirectedFeedback.FiniteAlphabet Finitely many stacks and control states are already part of FinTM2
OAI.DirectedFeedback.NPVerifier Polynomially bounded certificates checked by an actual deterministic finite-alphabet machine, on the explicitly encoded input/certificate pair
OAI.DirectedFeedback.InNP NP is defined independently of SAT or any hardness assertion
OAI.DirectedFeedback.Digraph Finite loopless digraph
OAI.DirectedFeedback.Digraph.IsCycle An actual simple directed cycle of positive length
OAI.DirectedFeedback.Digraph.Feedback A feedback set intersects EVERY actual directed cycle
OAI.DirectedFeedback.Digraph.dfvs Minimum number of vertices of a feedback set
OAI.DirectedFeedback.Digraph.bits Full explicit vertex and arc serialization, including isolated vertices
OAI.DirectedFeedback.GapInstance Output includes a strictly positive integer threshold
OAI.DirectedFeedback.GapReduction A strict YES/NO gap reduction implemented by a finite-alphabet machine with polynomial runtime in the raw input bit length
OAI.DirectedFeedback.MainStatement Constant-factor directed feedback vertex set hardness for all NP languages
OAI.DirectedFeedback.main@ComparatorChallenges/DirectedFeedback.lean Challenge statement: Constant-factor hardness of directed feedback vertex set
OAI.DirectionalTransience.directional_transience_implies_ballisticity@ComparatorChallenges/DirectionalBallisticity.lean Challenge statement: Directional transience implies ballisticity
OAI.DirectionalZeroOne.directional_zero_one@ComparatorChallenges/DirectionalWalk.lean Challenge statement: Directional zero–one law under strict ellipticity
OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re@ComparatorChallenges/DirichletSevenEighths.lean Challenge statement: Zero-free half-plane for Dirichlet L-functions
OAI.DiscreteFree.source_endpoints@ComparatorChallenges/DiscreteLipschitzFree.lean Challenge statement: Uniformly discrete Lipschitz-free space with AP but no BAP
OAI.CenteredDiskEndpoint.Plane The Euclidean plane, not the product space with its max norm
OAI.CenteredDiskEndpoint.absoluteDiskAverage Absolute disk average, retaining possible infinite values
OAI.CenteredDiskEndpoint.maximal The actual centered disk maximal function, over every positive real radius
OAI.CenteredDiskEndpoint.maximalReal Real representative; the endpoint also asserts that maximal f is finite a.e
OAI.CenteredDiskEndpoint.testPartial The i-th coordinate derivative of a smooth test function
OAI.CenteredDiskEndpoint.HasWeakGradient Distributional first derivatives represented by a vector-valued function
OAI.CenteredDiskEndpoint.InW11Loc Local W^(1,1), expressed using the same distributional gradient convention
OAI.CenteredDiskEndpoint.gradientNorm The gradient L1 norm in Euclidean norm
OAI.CenteredDiskEndpoint.EndpointStatement Exact endpoint, including finiteness before passing to the real representative
OAI.CenteredDiskEndpoint.main_endpoint@ComparatorChallenges/DiskMaximal.lean Challenge statement: Endpoint gradient bound for the centered disk maximal operator
OAI.Dixmier.Amenable A positive normalized left-invariant complex mean
OAI.Dixmier.NonamenableWitness A uniformly 101-bounded nonunitarizable representation on a separable complete complex Hilbert space, with its universe explicit
OAI.Dixmier.MainTheorem Every countable discrete nonamenable group has a bounded nonunitarizable witness
OAI.Dixmier.main_theorem_all_universes@ComparatorChallenges/Dixmier.lean Challenge statement: Separable nonunitarizable witnesses for countable nonamenable groups
OAI.Dixmier.current_main_theorem@ComparatorChallenges/DixmierAllDiscrete.lean Challenge statement: Unitarizability for all discrete groups
OAI.DoublingHilbert.DoublingAtMost Intrinsic open-ball doubling with a specified integer bound and centers in the subset
OAI.DoublingHilbert.AdmitsBiLipschitzEmbedding Finite distortion includes an arbitrary positive change of scale
OAI.DoublingHilbert.main@ComparatorChallenges/DoublingHilbert.lean Challenge statement: Doubling Hilbert subset without finite-dimensional embedding
OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional@ComparatorChallenges/DukePrimeDegree.lean Challenge statement: Torus-packet equidistribution in prime, quartic, and sextic degrees
OAI.DukePrimeDegree.prime_degree_packet_measures_tendsto_haar_unconditional@ComparatorChallenges/DukePrimeDegree.lean Challenge statement: Torus-packet equidistribution in prime, quartic, and sextic degrees
OAI.Lech.dutta_domain@ComparatorChallenges/DuttaDomain.lean Challenge statement: Lech’s multiplicity conjecture
OAI.Problem310.dyadic_affine_avoidance@ComparatorChallenges/DyadicAvoidance.lean Challenge statement: A large compact set avoiding every affine dyadic sequence
OAI.EditDistortion.Step A single unit-cost insertion, deletion, or (when enabled) substitution
OAI.EditDistortion.edit Minimum script length
OAI.EditApproximation.almostLinearEditDistanceRawBand@ComparatorChallenges/EditApproximation.lean Challenge statement: Almost-linear approximation of edit distance
OAI.EditDistortion.Script@ComparatorChallenges/EditDistance.lean An unrestricted script of exactly n unit edits
OAI.EditDistortion.distortion The product of the two maximal distance ratios
OAI.EditDistortion.leastDistortion The infimum over injective maps to real absolutely summable sequences
OAI.EditDistortion.alphabetSup Supremum over finite alphabet cardinalities
OAI.EditDistortion.BinaryWitness A finite nonempty subset of binary words of one common length
OAI.EditDistortion.MainClaim Uniform two-sided bounds with common positive constants and threshold
OAI.edit_distance_main@ComparatorChallenges/EditDistance.lean Challenge statement: Matching exponential-scale bounds for edit-distance distortion
OAI.Problem337.egyptian_length_is_minimum@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.main_double_log_order@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.one_expansions_finite_and_bounded@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.counting_double_log_order@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.exact_marker_padding@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.every_exact_marker_occurs@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.quantitative_marked_length@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.missing_denominator_semantics@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.Problem337.prescribed_denominator_corollary@ComparatorChallenges/EgyptianFractions.lean Challenge statement: Short expansions, counting, and prescribed denominators
OAI.EilenbergGanea.seedWord The signed words encode the relators x²y⁻⁵ and x²(yx⁻¹)³
OAI.EilenbergGanea.seedGraph@ComparatorChallenges/EilenbergGanea.lean Comparability graph of the seven vertices, 51 edges and 45 sectors
OAI.EilenbergGanea.cohomologicalDimension@ComparatorChallenges/EilenbergGanea.lean Projective dimension of the trivial integral left group-ring module
OAI.EilenbergGanea.HasClassifyingSpace@ComparatorChallenges/EilenbergGanea.lean Ordinary classifying CW spaces, with no bound on the cardinality of their cells
OAI.EilenbergGanea.source_main@ComparatorChallenges/EilenbergGanea.lean Challenge statement: A finitely generated Eilenberg-Ganea counterexample
OAI.PositiveEinsteinFour.Geometry.FrameOrientation An orientation is a clopen choice of determinant sign in every frame fiber
OAI.PositiveEinsteinFour.ClosedOrientedMetricFour@ComparatorChallenges/EinsteinFour.lean A connected closed oriented smooth Riemannian four-manifold
OAI.PositiveEinsteinFour.Classified Positive rescaling identifies the metric with one of the three standard models
OAI.PositiveEinsteinFour.orientedClassification@ComparatorChallenges/EinsteinFour.lean Challenge statement: Nonnegative-curvature Einstein classification and an L2 topological gap
OAI.PositiveEinsteinFour.classificationOn@ComparatorChallenges/EinsteinFour.lean Challenge statement: Nonnegative-curvature Einstein classification and an L2 topological gap
OAI.PositiveEinsteinFour.classification@ComparatorChallenges/EinsteinFour.lean Challenge statement: Nonnegative-curvature Einstein classification and an L2 topological gap
OAI.Elasticity.global_uniqueness@ComparatorChallenges/ElasticityUniqueness.lean Challenge statement: Global uniqueness in smooth isotropic elasticity
OAI.elementaryPositivityWitness@ComparatorChallenges/ElementaryPositivity.lean Challenge statement: Shareshian–Wachs elementary positivity
OAI.ThresholdParallelRepetition.threshold_parallel_repetition@ComparatorChallenges/EntangledGames.lean Challenge statement: Threshold repetition for entangled games
OAI.EntropyPhotonNumber.NumberIndex The number-basis indices for n bosonic modes
OAI.EntropyPhotonNumber.Fock The full, untruncated bosonic Fock space ℓ²(ℕⁿ, ℂ)
OAI.EntropyPhotonNumber.numberKet A number-basis vector
OAI.EntropyPhotonNumber.entry Matrix entries of an operator in the number basis
OAI.EntropyPhotonNumber.State Positive trace-one operators
OAI.EntropyPhotonNumber.totalNumber Total number of quanta in a number-basis vector
OAI.EntropyPhotonNumber.FiniteEnergy Exactly finiteness of the expectation of the nonnegative number operator
OAI.EntropyPhotonNumber.entropy −Tr ρ log ρ, using the continuous extension of −t log t at zero and continuous functional calculus for the positive operator ρ
OAI.EntropyPhotonNumber.g The thermal entropy per mode, with the convention 0 log 0 = 0
OAI.EntropyPhotonNumber.gInv The inverse of increasing g : [0,∞) → [0,∞), expressed by its lower level cut
OAI.EntropyPhotonNumber.oneModeBeamCoefficient One-mode passive beam-splitter coefficient, in number bases
OAI.EntropyPhotonNumber.beamCoefficient The same passive rotation is performed on all mode indices
OAI.EntropyPhotonNumber.SectorSplit Choices of the first input number in the total-number sector of (k,e)
OAI.EntropyPhotonNumber.outputBlock A single discarded-number diagonal block of U(ρA ⊗ ρB)U†
OAI.EntropyPhotonNumber.IsBeamSplitterOutput Reduced state after passive beam-splitter mixing of independent ports
OAI.EntropyPhotonNumber.entropy_photon_number_inequality@ComparatorChallenges/EntropyPhotonNumber.lean Challenge statement: The entropy photon-number inequality
OAI.Erdos3.manuscriptReciprocalProgressionTheorem@ComparatorChallenges/ErdosReciprocal.lean Challenge statement: Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds
OAI.EuclideanFiveColor.ProperColoring@ComparatorChallenges/EuclideanFiveColor.lean Challenge statement: No proper five-coloring
OAI.EuclideanFiveColor.no_proper_five_coloring@ComparatorChallenges/EuclideanFiveColor.lean Challenge statement: Five colors cannot properly color the Euclidean plane
OAI.EuclideanRamsey.classification@ComparatorChallenges/EuclideanRamsey.lean Challenge statement: Tensor-field classification of Ramsey configurations
OAI.EuclideanRamsey.CircleConsequence.at_most_five_circle_points_ramsey@ComparatorChallenges/EuclideanRamseyCircle.lean Challenge statement: Ramsey property for at most five circle points
OAI.EuclideanRamsey.NineStatement.nine_circle_configuration@ComparatorChallenges/EuclideanRamseyNine.lean Challenge statement: Nine-point non-Ramsey circle configuration
OAI.EuclideanRamsey.spherical_quadraticIndependent_ramsey_all@ComparatorChallenges/EuclideanRamseyQuadratic.lean Challenge statement: Quadratic-independence criterion for spherical configurations
OAI.EuclideanRamsey.ramsey_cospherical@ComparatorChallenges/EuclideanRamseySpherical.lean Challenge statement: Cosphericity of Ramsey configurations
OAI.EuclideanRamsey.TransitiveConsequence.subset_of_finite_transitive_ramsey@ComparatorChallenges/EuclideanRamseyTransitive.lean Challenge statement: Ramsey property for subsets of finite transitive configurations
OAI.CirculantHadamard.Barker.even_length_eq_two_or_four@ComparatorChallenges/EvenBarker.lean Challenge statement: Classification of positive even Barker lengths
OAI.ExactFourier.Gate One charged scalar gate, referencing only available values
OAI.ExactFourier.Program A topologically ordered scalar DAG; available values are never consumed
OAI.ExactFourier.Circuit Outputs name available values, so permutations and arbitrary fanout are uncharged
OAI.ExactFourier.MainStatement The precise quantified formulation of source theorem thm:main
OAI.ExactFourier.main_theorem@ComparatorChallenges/ExactFourier.lean Challenge statement: Subsequential savings for exact Fourier circuits
OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_individuallyProperlyInfinite_any@ComparatorChallenges/ExactInfiniteness.lean Challenge statement: Fixed-amplification pure infiniteness for exact algebras
OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite@ComparatorChallenges/ExactInfiniteness.lean Challenge statement: Fixed-amplification pure infiniteness for exact algebras
OAI.ExactQuantumFactoring.Primitive The five primitive gates exactly as in Section 2
OAI.ExactQuantumFactoring.Gate An inverse and/or one added control
OAI.ExactQuantumFactoring.Primitive.matrix Matrix entries are indexed by lists in wire order (row first, column second)
OAI.ExactQuantumFactoring.Instruction A primitive is placed on distinct actual wires, with no operation of unbounded arity hidden in a circuit instruction
OAI.ExactQuantumFactoring.inputBasis Input wires are first, least significant bit first; all other wires start zero
OAI.ExactQuantumFactoring.paddedLength The cutoff and padding are the standing parameters in Section 2
OAI.ExactQuantumFactoring.outputList n entries of n bits each, in the n² wires immediately after the input
OAI.ExactQuantumFactoring.CorrectEncoding Complete nondecreasing prime factorization, multiplicities included, padded by zeros, as in Section 6
OAI.ExactQuantumFactoring.Circuit.correctProbability Unnormalized Born sum on correct outputs; success is exactly one, not positivity, postselection, or a limiting high probability
OAI.ExactQuantumFactoring.natWord Unary natural words with delimiters make the circuit description explicit
OAI.ExactQuantumFactoring.Uniform A single finite-alphabet classical generator receives only the INPUT LENGTH
OAI.ExactQuantumFactoring.MainTheorem Literal main endpoint: one length-uniform family, exact output for EVERY binary integer N≥2, and worst-case polynomial gates AND qubits
OAI.ExactQuantumFactoring.exact_quantum_factoring@ComparatorChallenges/ExactQuantumFactoring.lean Challenge statement: Exact quantum factoring over a fixed finite gate set
OAI.FKCRT.spanningGraph Documented declaration: spanningGraph
OAI.FKCRT.MapConditions Labelled connected orientable genus-zero rotation systems
OAI.FKCRT.MapIso Root-preserving isomorphism of oriented maps (both dart permutations intertwine)
OAI.FKCRT.clusterCount The source k_M(A), including isolated vertices
OAI.FKCRT.fkWeight Exact decorated finite-map weight from eq:finite-law
OAI.FKCRT.MetricMeasureData Unbundled presentation of a measured metric space; validity is specified below
OAI.FKCRT.MetricMeasureData.Valid Exactly compact metric probability spaces, with their Borel sigma algebras
OAI.FKCRT.degreeMass Normalized degree measure is uniform dart mass pushed to vertices
OAI.FKCRT.mapSpace Root and decoration are not included in the metric probability space
OAI.FKCRT.Amalgamates An ambient pseudometric on the disjoint union giving isometric embeddings
OAI.FKCRT.ghpEDist The common-isometric-embedding definition of the source GHP distance
OAI.FKCRT.IsGHPTest Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations
OAI.FKCRT.excursionDist Source excursion pseudometric, with the closed interval minimum
OAI.FKCRT.treeSpace The quotient by d_e=0, its induced metric, and pushforward of uniform time
OAI.FKCRT.standardExcursion Standard normalized excursion, realized as the 3D Bessel bridge
OAI.FKCRT.finiteExpectation Exact expectation under the finite law, with n+1 edges
OAI.FKCRT.MainStatement thm:main
OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt@ComparatorChallenges/FKCRT.lean Challenge statement: The geometric phase diagram, diffusion, and spectra of random planar maps
OAI.Generator.single_generation_of_II1_separable_predual@ComparatorChallenges/FactorGeneration.lean Challenge statement: Single generation of separable-predual $\mathrm{II}_1$ factors
OAI.Falconer.falconer_distance_conjecture@ComparatorChallenges/FalconerAllDimensions.lean Challenge statement: Falconer distance theorem in every dimension
OAI.SharpIntegralFillings.coefficient_optimal@ComparatorChallenges/FillingCoefficient.lean Challenge statement: Optimality of the Euclidean filling coefficient
OAI.finiteCircle_fullMain@ComparatorChallenges/FiniteCircle.lean Challenge statement: Finite-circle obstructions and histogram embeddings for edit distance
OAI.FiniteCongruence.graph_criterion@ComparatorChallenges/FiniteCongruenceGraph.lean Challenge statement: Finite lattice representation and undecidability
OAI.FiniteEntropySeparation.main@ComparatorChallenges/FiniteEntropySeparation.lean Challenge statement: Two notions of free entropy differ even when both are finite
OAI.FiniteFactor.HasScalarCenter A concrete factor has scalar center
OAI.FiniteFactor.IsFiniteAlgebra Finiteness: every isometry in the algebra is unitary
OAI.FiniteFactor.HasNoMinimalProjection No nonzero projection is minimal, excluding matrix factors
OAI.FiniteFactor.HasSeparablePredual A separable Banach space whose dual is conjugate-linearly isometric to M
OAI.FiniteFactor.main_theorem@ComparatorChallenges/FiniteFactor.lean Challenge statement: Finite-factor invariant-projection counterexample
OAI.LittleFinitistic.extreme_left_right_asymmetry@ComparatorChallenges/FinitisticAsymmetry.lean Challenge statement: Left/right finitistic-dimension asymmetry
OAI.FixedClauseThreshold.main@ComparatorChallenges/FixedClauseThreshold.lean Challenge statement: Limiting satisfiability threshold for every fixed $k\ge3$
OAI.BalancedTransport.balanced_three_stack_realization@ComparatorChallenges/ForcedNavierStokesComputation.lean Challenge statement: Finite computation in a balanced zero-data fluid flow
OAI.ForestSpace.Cofinite The closed finite-codimensional subspaces
OAI.ForestSpace.aucValues The inner one-sided excess values and their infimum
OAI.ForestSpace.aucModulus The one-sided asymptotic uniform convexity modulus, with the order of infimum, supremum and infimum
OAI.ForestSpace.averageValues The inner averaged signed excess; it is not replaced by a maximum
OAI.ForestSpace.averageModulus The averaged asymptotic midpoint modulus
OAI.ForestSpace.EquivalentNorm An equivalent norm is kept as its exact real seminorm, with explicit positive comparison constants
OAI.ForestSpace.Reflexive Canonical (not merely abstract) reflexivity
OAI.ForestSpace.IsAUC AUC requires positivity at every strictly positive parameter
OAI.ForestSpace.IsSegment A finite, order-convex chain
OAI.ForestSpace.segSum The sum of coordinates over a segment
OAI.ForestSpace.TestBound Squared bound on every disjoint family of segment tests
OAI.ForestSpace.testValues All squared disjoint-segment tests
OAI.ForestSpace.rho Exactly the disjoint-segment norm, written as the square root of its squared testing supremum
OAI.ForestSpace.segmentSeminorm The disjoint-segment seminorm on finite coordinate vectors
OAI.ForestSpace.TestVector Finite coordinate vectors with the segment norm (a type synonym prevents clashes with any other norm on finitely supported functions)
OAI.ForestSpace.J J(T), completion of the finite-support disjoint-segment norm
OAI.ForestSpace.FullDual The full continuous dual, used for the finite-height forest example
OAI.ForestSpace.Word Finite words, ordered by extension, including the empty root
OAI.ForestSpace.Vertex A disjoint forest: one copy of Nat^{≤h} for every h≥1
OAI.ForestSpace.Diamond.Network An oriented edge enumeration; only the associated undirected unit-edge simple graph is used for distances
OAI.ForestSpace.Diamond.Network.refine Every edge is replaced by countably many internally disjoint two-edge paths
OAI.ForestSpace.Diamond.Network.iterate Iterating the very same edge replacement, starting from an arbitrary network
OAI.ForestSpace.Diamond.base D₀ is precisely one edge
OAI.ForestSpace.Diamond.diamond Countably branching diamonds, all current edges of length one
OAI.ForestSpace.Diamond.distance@ComparatorChallenges/ForestSpace.lean The shortest-path distance, via Mathlib's actual graph distance
OAI.ForestSpace.Diamond.EmbeddingBound The distortion convention, including its arbitrary positive scale
OAI.ForestSpace.main_theorem@ComparatorChallenges/ForestSpace.lean Challenge statement: Reflexive tree space, midpoint modulus, and diamond distortion
OAI.NCHitting.universal_hitting@ComparatorChallenges/FormulaHitting.lean Challenge statement: One rational matrix tuple hitting all bounded-size noncommutative formulas
OAI.Problem346.canonical_foulkes_howe_surjective@ComparatorChallenges/FoulkesHowe.lean Challenge statement: Foulkes' conjecture for sixth powers and quadratic stabilization
OAI.FourRow.robust_permanent@ComparatorChallenges/FourRowPermanent.lean Challenge statement: Strict four-row permanent inequality near the uniform law
OAI.FourierLLogL.paperMain@ComparatorChallenges/FourierLLogL.lean Challenge statement: The $`L\log L`$ Fourier-convergence conjecture
OAI.Problem367.free_ising_factor_iff_threshold@ComparatorChallenges/FreeIsing.lean Challenge statement: The exact factor-of-IID threshold for free Ising spins on trees
OAI.Problem336.fusf_is_factor_iid@ComparatorChallenges/FreeUniformSpanningForest.lean Challenge statement: A universal IID factor for the free uniform spanning forest
OAI.GammaFPP.HasC1CurveChart A regular C¹ parametrization of the curve near a point, with a continuous inverse
OAI.GammaFPP.GammaDifferentiabilityTarget The Gamma theorem: an actual deterministic passage-time limit norm exists for every positive shape and rate and every iid environment with that law
OAI.GammaFPP.gamma_differentiability@ComparatorChallenges/GammaPassage.lean Challenge statement: Differentiability for every positive Gamma edge-weight law
OAI.RepeatedLocalization.FiniteEntropy.finite_expected_regularization@ComparatorChallenges/GaussianFiniteEntropy.lean Challenge statement: Finite-entropy localization and regularization bounds
OAI.RepeatedLocalization.repeated_localization@ComparatorChallenges/GaussianInformation.lean Challenge statement: Information growth under repeated exact Gaussian observations
OAI.AllScaleInverseVolume.inverse_volume_without_support@ComparatorChallenges/GaussianInformation.lean Challenge statement: Information growth under repeated exact Gaussian observations
OAI.KernelPotential.kernel_coercivity@ComparatorChallenges/GaussianInformation.lean Challenge statement: Information growth under repeated exact Gaussian observations
OAI.KernelPotential.actual_row_drift@ComparatorChallenges/GaussianInformation.lean Challenge statement: Information growth under repeated exact Gaussian observations
OAI.GaussianMoat.fullMain@ComparatorChallenges/GaussianMoat.lean Challenge statement: Uniformly bounded components of Gaussian-prime graphs
OAI.GaussianPropeller.all_partitions@ComparatorChallenges/GaussianPropeller.lean Challenge statement: The Gaussian propeller conjecture in every dimension
OAI.CurrentProjection.mixedMomentMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.actualRowMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.actualRowRefinement@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.actualRowSourceMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.actualRowSourceRefinement@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.criticalComparisonMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.oneLevelComparisonMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.twoLabelComparisonMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.hybridBlockMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.fiberTwoPointMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.CurrentProjection.fiberBlockMain@ComparatorChallenges/GaussianReplacement.lean Challenge statement: Gaussian replacement and information bounds
OAI.GeneralMahler.polarAt@ComparatorChallenges/GeneralMahler.lean The polar of a convex body translated by an interior center
OAI.GeneralMahler.volumeProduct The volume product minimized over the interior centers of the body
OAI.GeneralMahler.general_mahler@ComparatorChallenges/GeneralMahler.lean Challenge statement: The general Mahler bound, with equality exactly for simplices
OAI.GeneralizedStarHeight.main@ComparatorChallenges/GeneralizedStarHeight.lean Challenge statement: Generalized star height at most three
OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement@ComparatorChallenges/GotsmanLinial.lean Challenge statement: Average sensitivity of polynomial threshold functions
OAI.GrahamSpherical.full_main@ComparatorChallenges/GrahamSpherical.lean Challenge statement: Twelve-point spherical non-Ramsey example
OAI.Grothendieck.elementary_expansion@ComparatorChallenges/GrothendieckElementaryExpansion.lean Challenge statement: The Grothendieck homotopy hypothesis
OAI.GroupRingDeterminant.Hilbert The Hilbert space l²(G)^n, with the product coordinates flattened
OAI.GroupRingDeterminant.identityVector The identity vector in component i
OAI.GroupRingDeterminant.groupTrace The unnormalized matrix trace, linear in its operator argument
OAI.GroupRingDeterminant.fkDet The invertible-case Fuglede--Kadison determinant
OAI.GroupRingDeterminant.IsRegularOperator Exact coordinate specification of the bounded left-regular operator of A
OAI.GroupRingDeterminant.rationalMatrix Coefficientwise extension from the integral to the rational group ring
OAI.GroupRingDeterminant.MainStatement An integral group-ring matrix with rational and bounded inverses and determinant in (0, 1)
OAI.GroupRingDeterminant.main@ComparatorChallenges/GroupRingDeterminant.lean Challenge statement: Group-ring determinant counterexample
OAI.HadamardSix.rowRatio_cubeFiber_sum_zero@ComparatorChallenges/HadamardCubeFiber.lean Challenge statement: Cube-fiber cancellation for order-six Hadamard row ratios
OAI.HadwigerCounterexample.exists_counterexamples@ComparatorChallenges/HadwigerCounterexample.lean Challenge statement: Counterexamples of arbitrarily large order
OAI.HadwigerCounterexample.not_hadwiger_conjecture@ComparatorChallenges/HadwigerCounterexample.lean Challenge statement: Hadwiger's conjecture fails
OAI.PlanarHalving.power_bounds@ComparatorChallenges/HalvingLines.lean Challenge statement: Power savings for planar halving lines and k-sets
OAI.HardSphere.condensation_with_mixed@ComparatorChallenges/HardSphere.lean Challenge statement: Positive-temperature Bose–Einstein condensation and exact quantum depletion
OAI.HarmonicArtin.salvetti_cover_contractible@ComparatorChallenges/HarmonicArtin.lean Challenge statement: Contractibility of the Salvetti cover
OAI.HarmonicCounterexample.SmoothMetric A genuine smooth positive definite covariant metric tensor on R^n
OAI.HarmonicCounterexample.coordDeriv The coordinate directional derivative
OAI.HarmonicCounterexample.christoffel Levi-Civita connection in the single global Cartesian chart
OAI.HarmonicCounterexample.ricci Ricci tensor, with the convention in which the round sphere has positive Ricci
OAI.HarmonicCounterexample.laplaceBeltrami Trace of the covariant Hessian, i.e
OAI.HarmonicCounterexample.pathLength Riemannian length of a path on the unit parameter interval
OAI.HarmonicCounterexample.distance Infimum of smooth path lengths, the intrinsic Riemannian distance
OAI.HarmonicCounterexample.Complete Sequential metric completeness, for the intrinsic distance, not the background one
OAI.HarmonicCounterexample.ballVolume Riemannian measure of the intrinsic open ball, retaining infinite values
OAI.HarmonicCounterexample.omega The ordinary Euclidean unit ball volume, in Cartesian Lebesgue measure
OAI.HarmonicCounterexample.PositiveSubunitAVR The volume-ratio limit is finite, positive, and strictly below one
OAI.HarmonicCounterexample.HarmonicGrowth Membership in the actual space H_k, with the bound required at every point
OAI.HarmonicCounterexample.MainClaim The manuscript's unconditional main existence claim
OAI.HarmonicCounterexample.main@ComparatorChallenges/HarmonicGrowth.lean Challenge statement: Failure of integer-degree harmonic dimension comparison
OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_seven_eighths_lt_re@ComparatorChallenges/HeckeSevenEighths.lean Challenge statement: Finite-order Hecke $L$-function $7/8$ bound
OAI.Problem355.heilbronn_power_lower_bound@ComparatorChallenges/HeilbronnTriangle.lean Challenge statement: A power improvement in the Heilbronn triangle lower bound
OAI.Problem355.almost_n_minus_two_refuted@ComparatorChallenges/HeilbronnTriangle.lean Challenge statement: A power improvement in the Heilbronn triangle lower bound
OAI.Heisenberg.spontaneous_magnetization@ComparatorChallenges/Heisenberg.lean Challenge statement: Bloch's law, its lattice correction, and the spherical magnetization law
OAI.HenonLaneEmden.main_nonexistence@ComparatorChallenges/HenonEmden.lean Challenge statement: The Lane–Emden and Hénon–Lane–Emden conjectures
OAI.HilbertCrouzeix.numericalClosure_geometry@ComparatorChallenges/HilbertCrouzeix.lean Challenge statement: Numerical-range geometry and finite-compression support
OAI.HilbertCrouzeix.exists_finite_compression@ComparatorChallenges/HilbertCrouzeix.lean Challenge statement: Numerical-range geometry and finite-compression support
OAI.HilbertCrouzeix.rational_denominator_isUnit@ComparatorChallenges/HilbertCrouzeix.lean Challenge statement: Numerical-range geometry and finite-compression support
OAI.HilbertCrouzeix.zeroConclusion@ComparatorChallenges/HilbertCrouzeix.lean Challenge statement: Numerical-range geometry and finite-compression support
OAI.PolynomialVacuumBridge.Corridor.finite_bridge_sums@ComparatorChallenges/HoneycombBridgeFiniteness.lean Challenge statement: Finiteness of critical bridge mass and first length moments
OAI.CriticalHoneycomb.Adj Adjacency across a full triangular edge
OAI.CriticalHoneycomb.centerPosition The fixed Euclidean embedding in the unit triangular tiling
OAI.CriticalHoneycomb.Port A midpoint port, oriented into the triangle domain
OAI.CriticalHoneycomb.IsTrace A simple center trace, with no premature boundary exit
OAI.CriticalHoneycomb.weight Length counts centers; the port half-edges contribute no factors
OAI.CriticalHoneycomb.strip The source's strip and tilt-compatible terminal support
OAI.CriticalHoneycomb.FiniteBridgeMassEstimate Necessary estimate c:finite(1), inputs.tex:13, on the actual path sum
OAI.CriticalHoneycomb.finiteBridgeMassEstimate@ComparatorChallenges/HoneycombBridgeMassSupport.lean Challenge statement: Strict honeycomb bridge mass of order $(1+h)^{-1/4}$
OAI.HoneycombForce.logPartition_tendsto@ComparatorChallenges/HoneycombFreeEnergy.lean Challenge statement: Existence of the honeycomb free-energy limit
OAI.StrictHotSpots.main_theorem@ComparatorChallenges/HotSpots.lean Challenge statement: The hot spots conjecture for simply connected planar domains
OAI.Paper256.main_result@ComparatorChallenges/HyperbolicCones.lean Challenge statement: Hyperbolicity cones without semidefinite lifts
OAI.HyperbolicObstruction.FiniteComplex.DiskMove An elementary disk move
OAI.HyperbolicObstruction.FiniteComplex.DiskHomotopy A disk certificate obtained by elementary triangle attachments/removals, with spurs/collapses allowed
OAI.HyperbolicObstruction.IsSegment A constant-speed metric segment, parametrized on [0,1]
OAI.HyperbolicObstruction.CATZero The CN characterization of CAT(0), with whole metric segments
OAI.HyperbolicObstruction.CATNegOne The hyperbolic-cosh midpoint characterization of CAT(-1)
OAI.HyperbolicObstruction.GeometricAction A proper, cocompact isometric action of a discrete group
OAI.HyperbolicObstruction.WordHyperbolic Four-point word hyperbolicity, for some finite generating set
OAI.HyperbolicObstruction.CompatibleLocallyCATNegOne A metric on the given finite polyhedron, not on a different topology
OAI.HyperbolicObstruction.MainStatement A finite aspherical complex with hyperbolic fundamental group, no geometric CAT(0) action, and no homotopy equivalent finite complex admitting a locally CAT(-1) metric
OAI.HyperbolicObstruction.main@ComparatorChallenges/HyperbolicObstruction.lean Challenge statement: A hyperbolic group without a geometric CAT(0) action
OAI.Hyperinvariant.main_theorem@ComparatorChallenges/HyperinvariantSubspaces.lean Challenge statement: Quasinilpotent operator with a transitive commutant
OAI.IndependentProducts.Vertex The tree of finite sequences of positive integers
OAI.IndependentProducts.Edge Coordinates are attached only to nonroot vertices
OAI.IndependentProducts.productMeasure The product law of independent copies of the multiplier
OAI.IndependentProducts.pathPrefix The nonroot prefix ending at position j
OAI.IndependentProducts.pathProduct Root product is the empty product 1; every other product uses the path prefixes
OAI.IndependentProducts.productSpan The closed real L1 span of the path products
OAI.IndependentProducts.MultiplierHypotheses@ComparatorChallenges/IndependentProducts.lean Positivity, nonconstancy, mean one, and finite second moment of the multiplier law
OAI.IndependentProducts.CofiniteSubspaces Closed subspaces of finite codimension, with respect to the inherited topology
OAI.IndependentProducts.averagedMidpointModulus The averaged asymptotic midpoint modulus, with directions of norm at least 1
OAI.IndependentProducts.oneSidedModulus The usual one-sided modulus, whose directions have norm exactly 1
OAI.IndependentProducts.IsEquivalentNorm A seminorm with these bounds is a genuine norm equivalent to the original norm
OAI.IndependentProducts.gaussianTail Gaussian-tail probability, in real rather than extended-nonnegative-real notation
OAI.IndependentProducts.excessConstant The Gaussian excess constant at threshold twice the parameter
OAI.IndependentProducts.exponentialLaw The density exp(-w) on the positive half-line
OAI.IndependentProducts.gaussianSquareLaw The law of the square of a standard real Gaussian
OAI.IndependentProducts.main_general@ComparatorChallenges/IndependentProducts.lean Challenge statement: Independent-product spaces and positive midpoint moduli
OAI.IndependentProducts.main_exponential@ComparatorChallenges/IndependentProducts.lean Challenge statement: Independent-product spaces and positive midpoint moduli
OAI.IndependentProducts.main_gaussian_24@ComparatorChallenges/IndependentProducts.lean Challenge statement: Independent-product spaces and positive midpoint moduli
OAI.IndependentProducts.main_gaussian_12@ComparatorChallenges/IndependentProducts.lean Challenge statement: Independent-product spaces and positive midpoint moduli
OAI.LargeIndependentSets.frame Binary framing: true,b for a payload bit and false as terminator
OAI.LargeIndependentSets.Graph A nonempty, finite, simple, undirected, unweighted graph
OAI.LargeIndependentSets.graphBits Full explicit adjacency matrix, row-major, with binary vertex count
OAI.LargeIndependentSets.RealGraphReduction Polynomial-time graph reduction with a real independence-ratio threshold
OAI.LargeIndependentSets.mainTheoremReal@ComparatorChallenges/IndependentSets.lean Challenge statement: Hardness of coloring three-colorable graphs
OAI.MainGap.Manuscript.individual_to_strong_main@ComparatorChallenges/IndividualStrongInfiniteness.lean Challenge statement: Individual proper infiniteness implies strong pure infiniteness
OAI.InfiniteMatroidCounterexample.main@ComparatorChallenges/InfiniteMatroid.lean Challenge statement: Infinite matroid packing/covering counterexample
OAI.InfiniteMatroidCounterexample.partitional_intersection_counterexample@ComparatorChallenges/InfiniteMatroidCorollaries.lean Challenge statement: Partitional intersection, covering, and packing counterexamples
OAI.InfiniteMatroidCounterexample.separate_covering_packing_counterexamples@ComparatorChallenges/InfiniteMatroidCorollaries.lean Challenge statement: Partitional intersection, covering, and packing counterexamples
OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic@ComparatorChallenges/InterpolatedFactors.lean Challenge statement: Isomorphism of the free group factors
OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.positive_temperature_pressure_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.ground_state_limit_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.random_pressure_limit_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional@ComparatorChallenges/InvariantIsing.lean Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses
OAI.Invariant233.Results.prescribed_irrational_counterexample@ComparatorChallenges/IrrationalRotation.lean Challenge statement: Invariant-projection counterexamples for every irrational rotation
OAI.Invariant233.Results.product_realization@ComparatorChallenges/IrrationalRotation.lean Challenge statement: Invariant-projection counterexamples for every irrational rotation
OAI.TriangularBilliards.Triangle Three affinely independent vertices in the Euclidean plane
OAI.TriangularBilliards.Triangle.table The open table; the complex plane carries its ordinary real Euclidean metric
OAI.TriangularBilliards.Triangle.side The open side from vertex i to the next vertex, indexed cyclically
OAI.TriangularBilliards.Triangle.tangent A tangent vector to side i, with no choice of inward or outward normal
OAI.TriangularBilliards.Triangle.angle Interior angle at vertex i
OAI.TriangularBilliards.reflect Reflection in the real line spanned by the nonzero tangent e
OAI.TriangularBilliards.FlightChain A complete nonsingular billiard trajectory, indexed by its collisions
OAI.TriangularBilliards.FlightChain.at The geometric state on a chain, using outgoing velocity at a collision
OAI.TriangularBilliards.billiardFlow The actual specular flow on complete regular chains
OAI.TriangularBilliards.angularMeasure Uniform angular probability, parameterized by [0,2π)
OAI.TriangularBilliards.phaseMeasure Exactly normalized area in the open table times uniform angular measure
OAI.TriangularBilliards.MainConclusion The main conclusion, together with the geometric/nonvacuity guarantees needed by the concrete definition of the actual two-sided billiard
OAI.TriangularBilliards.irrational_triangle_billiard@ComparatorChallenges/IrrationalTriangleBilliard.lean Challenge statement: Weak mixing of triangular billiards with an irrational angle
OAI.IsingPerceptron.variationalValue_real_of_continuous@ComparatorChallenges/IsingFiniteness.lean Challenge statement: Finiteness of the Ising-perceptron variational value
OAI.SmoothLocal.Geometry.exists_local_metric_without_local_immersion@ComparatorChallenges/IsometricImmersion.lean Challenge statement: A smooth surface metric with no local isometric immersion in ℝ3
OAI.Erdos970.Erdos970Final.erdos_970_quadratic@ComparatorChallenges/Jacobsthal.lean Challenge statement: Quadratic Jacobsthal bound
OAI.Erdos970.Erdos970Final.erdos_970_iterated_log@ComparatorChallenges/JacobsthalImproved.lean Challenge statement: Jacobsthal bound with an iterated-logarithm saving
OAI.Erdos970.NumberTheoryLean.Dickman.rho The continuous delay-equation construction of the Dickman function
OAI.JointDickman.realDensity Ordinary natural density over 2 ≤ n ≤ X, normalized by the real endpoint
OAI.JointDickmanPaper.joint_law@ComparatorChallenges/JointDickman.lean Challenge statement: Independent largest prime factors of consecutive integers
OAI.JointDickmanPaper.increasing_order@ComparatorChallenges/JointDickman.lean Challenge statement: Independent largest prime factors of consecutive integers
OAI.JointDickmanPaper.decreasing_order@ComparatorChallenges/JointDickman.lean Challenge statement: Independent largest prime factors of consecutive integers
OAI.KLInvariance.BruhatStep An upward edge in the strong Bruhat graph, with left reflection labels
OAI.KLInvariance.BruhatLE The actual strong Bruhat order, not the weak order
OAI.KLInvariance.Interval The unlabelled interval, including both endpoints
OAI.KLInvariance.rankDifference d(x,y) in the manuscript, used only for comparable endpoints
OAI.KLInvariance.NormalizedKL Exact equal-parameter normalization in the introduction
OAI.KLInvariance.klFamilies The polynomial families selected by their equal-parameter normalization
OAI.KLInvariance.combinatorial_invariance@ComparatorChallenges/KLInvariance.lean Challenge statement: Combinatorial invariance of Kazhdan–Lusztig polynomials
OAI.MetricKMedianRecovery.global_application@ComparatorChallenges/KMedianRecovery.lean Challenge statement: Randomized metric $k$-median approximation below two
OAI.MetricKMedianRecovery.RefinedRecovery.refined_recovery@ComparatorChallenges/KMedianRefinedRecovery.lean Challenge statement: Exact-budget recovery from accurate distinct cluster proxies
OAI.MetricKMedian.Complexity.FinitePolyTime Polynomial-time computation with every physical work alphabet finite
OAI.MetricKMedian.Complexity.PNeNP Separation of deterministic polynomial time from finite-verifier nondeterministic polynomial time
OAI.MetricKMedian.FactorCorrect An actual nonempty feasible facility set, encoded by its membership mask
OAI.MetricKMedian.approximationFactors Deterministic polynomial-time approximation factors for arbitrary specified clients and facilities
OAI.MetricKMedian.threshold@ComparatorChallenges/KMedianThreshold.lean Challenge statement: Exact approximation threshold under $P\ne NP$
OAI.KServer.Configuration Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.LabelDistribution@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.Policy Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.serve@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.serviceCost@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.pathProbability@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.expectedCost@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.optimalCost@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.MainStatement@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.KServer.main_theorem@ComparatorChallenges/KServer.lean Challenge statement: Squared-logarithmic randomized $k$-server on arbitrary metrics
OAI.BoundedHochschild.KadisonRingrose.main_result@ComparatorChallenges/KadisonRingrose.lean Challenge statement: The Kadison–Ringrose cohomology conjecture
OAI.KadisonSimilarity.universalCommutatorTheorem@ComparatorChallenges/KadisonSimilarity.lean Challenge statement: Kadison's similarity theorem and uniform hyperreflexivity
OAI.KadisonSimilarity.universalHyperreflexivity@ComparatorChallenges/KadisonSimilarity.lean Challenge statement: Kadison's similarity theorem and uniform hyperreflexivity
OAI.KadisonSimilarity.similarityTheorem@ComparatorChallenges/KadisonSimilarity.lean Challenge statement: Kadison's similarity theorem and uniform hyperreflexivity
OAI.UniversalCoverSplitting.main@ComparatorChallenges/KahlerSplitting.lean Challenge statement: Universal-cover product splitting
OAI.KaplanskyCounterexample.MainClaim Challenge statement: Failure of direct finiteness in characteristic 2
OAI.KaplanskyCounterexample.main_theorem@ComparatorChallenges/KaplanskyDirectFiniteness.lean Challenge statement: Main theorem of the Kaplansky counterexample after OAI.KaplanskyCounterexample.MainClaim
OAI.KaplanskyCounterexample.finitelyPresented_counterexample@ComparatorChallenges/KaplanskyFinitelyPresented.lean Challenge statement: Finitely presented characteristic-two counterexample
OAI.Kaplansky.kaplansky_quasitrace_counterexample@ComparatorChallenges/KaplanskyQuasitrace.lean Challenge statement: Nonadditive normalized $2$-quasitraces
OAI.KaplanskyConsequences.stable_finiteness_bundle@ComparatorChallenges/KaplanskyStableFiniteness.lean Challenge statement: Tensor-product failure of stable finiteness and quasitrace consequences
OAI.Kervaire.coefficient_injective@ComparatorChallenges/Kervaire.lean Challenge statement: Nonsingular systems of equations over arbitrary groups
OAI.Problem047.koebe_circle_domain@ComparatorChallenges/KoebeCircleDomains.lean Challenge statement: Koebe's unrestricted circle-domain uniformization
OAI.Problem047.removability_implies_rigidity@ComparatorChallenges/KoebeCircleDomains.lean Challenge statement: Conformal removability implies circle-domain rigidity
OAI.Laughlin.mainTarget_proved@ComparatorChallenges/Laughlin.lean Challenge statement: Uniform Laughlin $V_1$ spectral gap
OAI.LaughlinFock.thm_fock@ComparatorChallenges/LaughlinFock.lean Challenge statement: Uniform Fock-space spectral-gap inequality
OAI.LaughlinGap.thm_main@ComparatorChallenges/LaughlinGap.lean Challenge statement: Uniform unperturbed spherical Laughlin gap inequality
OAI.Laughlin.Planar.HomogeneousState Occupation coefficients with fixed particle number in every homogeneous degree
OAI.Laughlin.planar_gap@ComparatorChallenges/LaughlinPlanar.lean Challenge statement: Planar spectral-gap inequality
OAI.SharpLiebThirring.schrodingerForm The polarized form of -d²/dx² - W, on exactly H¹
OAI.SharpLiebThirring.IsNegativeEigenfunction Weak eigenfunction at the negative energy -k²
OAI.SharpLiebThirring.negativeMoment An unlimited finite-family-size supremum, in ℝ≥0∞, includes the entire sum
OAI.SharpLiebThirring.oneStateMoment The moment retaining at most one negative eigenvalue
OAI.SharpLiebThirring.MainClaim The full spectral bound, optimal constants, and attainment at the explicit potential
OAI.SharpLiebThirring.sharp_lieb_thirring@ComparatorChallenges/LiebThirring.lean Challenge statement: Sharp finite-matrix Lieb–Thirring inequalities and all equality cases
OAI.LipschitzCounterexample.main@ComparatorChallenges/LipschitzEquivalence.lean Challenge statement: Bi-Lipschitz equivalent nonisomorphic Banach spaces
OAI.LipschitzHilbert.shortTransform The symmetrized form of the hard-truncated directional integral
OAI.LipschitzHilbert.twoSidedTruncation The two hard-cutoff intervals in the directional Hilbert transform
OAI.LipschitzHilbert.smoothPrincipalValue@ComparatorChallenges/LipschitzHilbert.lean The symmetric quotient extended continuously at zero for smooth inputs
OAI.LipschitzHilbert.main@ComparatorChallenges/LipschitzHilbert.lean Challenge statement: Hilbert transforms along Lipschitz directions
OAI.LipschitzHilbert.uniform_truncation@ComparatorChallenges/LipschitzHilbert.lean Challenge statement: Hilbert transforms along Lipschitz directions
OAI.LinearListHadwiger.main_theorem@ComparatorChallenges/ListHadwiger.lean Challenge statement: Linear list-coloring bound in the Hadwiger number
OAI.LittleFinitistic.Main.exists_counterexample@ComparatorChallenges/LittleFinitistic.lean Challenge statement: Infinite little finitistic dimension
OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.littlewoodValue The consecutive-degree polynomial of a real coefficient family
OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.IsRealSigning Every coefficient is a real sign
OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.main@ComparatorChallenges/LittlewoodFiniteFlatness.lean Challenge statement: Finite-exponent flatness of one all-length Littlewood family
OAI.LogBrunnMinkowski.main@ComparatorChallenges/LogBrunnMinkowski.lean Challenge statement: Logarithmic and Lp Brunn–Minkowski inequalities and the B-conjecture
OAI.LogConcaveSampling.Admissible Normalized twice continuously differentiable potentials with Hessian between the identity and twice the identity
OAI.LogConcaveSampling.gibbsDensity The unnormalized Gibbs density relative to Euclidean volume
OAI.LogConcaveSampling.gibbs The Gibbs probability law, normalized by its partition function
OAI.LogConcaveSampling.OracleAlgorithm Measurable adaptive queries and output, parametrized by private randomness
OAI.LogConcaveSampling.CanSample A uniform sampler with a deterministic query budget on every execution and total-variation error at most one tenth
OAI.LogConcaveSampling.queryComplexity The smallest feasible integer query budget, or infinity when no budget is feasible
OAI.LogConcaveSampling.ExponentBound The quantified dimension-exponent upper bound with every positive exponent slack
OAI.LogConcaveSampling.exact_source_main@ComparatorChallenges/LogConcaveQuery.lean Challenge statement: Subpolynomial query complexity for log-concave sampling
OAI.ReverseLogKodaira.SmoothProjectiveVariety.veryGenerally_fiber_negative_branch@ComparatorChallenges/LogKodairaFiberNegative.lean Challenge statement: Iitaka subadditivity, variation, and logarithmic additivity
OAI.ExactDerandomization.Word Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Language Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.CoinTape Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Direction.move Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Direction.moveInput Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.readInput Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.initial Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.step Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.run Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.spaceThrough Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.LogSpace Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.Deterministic Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.HaltsBy Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.Decides Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.extendCoins Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.Machine.acceptanceProbability Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.polynomialClock Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.L Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.RL Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.BPL Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.ExactDerandomization.exact_logarithmic_space_derandomization@ComparatorChallenges/LogspaceEquality.lean Challenge statement: Exact derandomization of logarithmic space: $`\mathsf L=\mathsf{RL}=\mathsf{BPL}`$
OAI.MUB6.Equivalent Full Hadamard equivalence, with arbitrary unit complex phases
OAI.MUB6.taoExponent The five-cycle exponent matrix in equation (cubic-matrix)
OAI.MUB6.fourier_and_family_bound@ComparatorChallenges/MUBSix.lean Challenge statement: Order-six Hadamard Fourier vanishing and a five-basis upper bound
OAI.SymmetricMahler.symmetric_mahler@ComparatorChallenges/MahlerConjecture.lean Challenge statement: Symmetric Mahler volume bound
OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm@ComparatorChallenges/MarkovType.lean Challenge statement: Markov type characterizes superreflexivity
OAI.Problem326.global_bounded_persistent_solution@ComparatorChallenges/MassAction.lean Challenge statement: Classwise permanence for weakly reversible mass-action systems
OAI.PerfectMatchingPSD.affine_lift_lower_bound@ComparatorChallenges/MatchingAffineLift.lean Challenge statement: Superpolynomial lower bound for affine semidefinite lifts
OAI.MatchingEntropy.probabilitySimplex Nonnegative real weights with total mass one
OAI.MatchingEntropy.entropy_main@ComparatorChallenges/MatchingEntropy.lean Challenge statement: Perfect-matching entropy bound
OAI.MatchingEntropyBounds.Refined.pointwise_entropy@ComparatorChallenges/MatchingEntropyBounds.lean Challenge statement: Refined pointwise perfect-matching entropy bounds
OAI.MatchingFPRAS.GraphInput Each unordered edge is represented once, by increasing endpoints
OAI.MatchingFPRAS.Perfect Exactly one selected edge is incident to every vertex
OAI.MatchingFPRAS.Z The exact unweighted count, including the empty graph
OAI.MatchingFPRAS.encodeInput Explicit sparse graph encoding, then the two rational parameters
OAI.MatchingFPRAS.timeBound A fixed-degree polynomial in input bits, ε⁻¹, and log δ⁻¹
OAI.MatchingFPRAS.MainStatement A uniform approximation scheme using independent fair bits
OAI.MatchingFPRAS.thm_main@ComparatorChallenges/MatchingFPRAS.lean Challenge statement: Randomized approximation of the perfect-matching count
OAI.PerfectMatchingPSD.HasFactorization Real PSD factors of order r, without equivariance or rank-one restrictions
OAI.PerfectMatchingPSD.psdRank The least positive order of a real PSD factorization
OAI.PerfectMatchingPSD.MainClaim Every positive real power is eventually smaller than the PSD rank, uniformly over all even vertex counts
OAI.PerfectMatchingPSD.main@ComparatorChallenges/MatchingPSD.lean Challenge statement: Superpolynomial PSD rank for the perfect-matching slack matrix
OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent Positive slack, one uniform constant, and a correct program at every size
OAI.MatrixAllFields.MatrixMultiplication.AllFieldMain.omega_lt_source_constant@ComparatorChallenges/MatrixFields.lean Challenge statement: Matrix-multiplication exponent over every field
OAI.MatrixMultiplication.Arithmetic.AdmissibleExponent Positive slack, one uniform constant, and a correct program at every size
OAI.MatrixMultiplication.Arithmetic.innerSize The inner dimension of an n × n^k by n^k × n multiplication
OAI.MatrixMultiplication.Arithmetic.complexAlpha The dual exponent is a supremum of exact exponent-two rectangular shapes
OAI.MatrixMultiplication.complex_omega_le_nine_quarters@ComparatorChallenges/MatrixMultiplication.lean Complex matrix multiplication has exponent at most 9/4
OAI.MatrixMultiplication.complex_alpha_gt_93_div_200@ComparatorChallenges/MatrixMultiplication.lean The complex dual matrix-multiplication exponent is greater than 0.465
OAI.MatrixMultiplication.complex_rectangular_omega_lt_523_div_250@ComparatorChallenges/MatrixMultiplication.lean Rectangular complex matrix multiplication at aspect ratio 0.709 has exponent below 2.092
OAI.Problem348.no_polynomial_removal_bound@ComparatorChallenges/MatrixRemoval.lean Challenge statement: Polynomial removal fails for ordered binary matrices
OAI.MatroidProphet.one_sample@ComparatorChallenges/MatroidProphet.lean Challenge statement: One-sample matroid prophet inequality against an almighty adversary
OAI.MatroidProphet.Assigned.one_sample@ComparatorChallenges/MatroidSecretary.lean Challenge statement: Hidden-vector matroid selection with worst-order guarantee
OAI.MatroidProphet.Assigned.hidden_vector@ComparatorChallenges/MatroidSecretary.lean Challenge statement: Hidden-vector matroid selection with worst-order guarantee
OAI.MatroidProphet.Assigned.secretary@ComparatorChallenges/MatroidSecretary.lean Challenge statement: Hidden-vector matroid selection with worst-order guarantee
OAI.MaximalSeshadri.Geometry.maximalSeshadriConstants@ComparatorChallenges/MaximalSeshadriConstants.lean Challenge statement: Eventual maximal Seshadri constants
OAI.MemoryPrecision.cube_coordinate_square_le Every coordinate of the paired cube has square at most one quarter
OAI.MemoryPrecision.main@ComparatorChallenges/MemoryPrecision.lean Challenge statement: Projection estimates and memory–precision bounds
OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers@ComparatorChallenges/MetricEntropyDuality.lean Challenge statement: A counterexample to metric-entropy duality
OAI.MetricKMedian.main_finite_work@ComparatorChallenges/MetricKMedian.lean Challenge statement: Deterministic metric $k$-median approximation at the threshold
OAI.SegmentLenses.midpoint_lens_main@ComparatorChallenges/MidpointLenses.lean Challenge statement: Midpoint-lens tail estimate
OAI.MinUncut.main@ComparatorChallenges/MinUncut.lean Challenge statement: Arbitrary constant-factor hardness of Min-UnCut
OAI.Nagata.AffineMultiplicity.ordinaryMultiplicity@ComparatorChallenges/Nagata.lean The least total degree of a nonzero Taylor coefficient
OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast@ComparatorChallenges/Nagata.lean Local multiplicity lower bounds are membership in powers of the point ideal
OAI.Nagata.Workers.W30.exists_positive_degree_equation_of_homogeneous_cycle@ComparatorChallenges/Nagata.lean Challenge statement: Nagata's conjecture
OAI.Nagata.Workers.W10.EffectivePlaneCurve@ComparatorChallenges/Nagata.lean Nonzero finite cycles of homogeneous prime plane ideals, with natural weights
OAI.Nagata.Workers.W10.curveEquation@ComparatorChallenges/Nagata.lean An equation realizing the entire cycle, including repeated components
OAI.Nagata.nagata_conjecture@ComparatorChallenges/Nagata.lean Challenge statement: Nagata's conjecture
OAI.Nagata.nagata_conjecture_coordinates@ComparatorChallenges/Nagata.lean Challenge statement: Nagata's conjecture
OAI.NaimarkZFC.IsSimpleCStar Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.IsState Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.IsFaithfulTracialState Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.IsIrreducible Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.UnitarilyEquivalent Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.HasUniqueIrreducibleRepresentation Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.IsIsomorphicToCompacts Challenge statement: A ZFC counterexample to Naimark's problem
OAI.NaimarkZFC.main@ComparatorChallenges/Naimark.lean Challenge statement: A ZFC counterexample to Naimark's problem
OAI.AlternatingNS.alternating@ComparatorChallenges/NavierStokesAlternating.lean Challenge statement: Rapidly decaying alternating-coordinate memory
OAI.VelocityDetection.main_result@ComparatorChallenges/NavierStokesVelocity.lean Challenge statement: Pointwise and integral velocity-field detection of halting
OAI.SharpNodal.Main@ComparatorChallenges/NodalLength.lean Challenge statement: Sharp upper bound for nodal length on smooth surfaces
OAI.NoiselessRegression.main@ComparatorChallenges/NoiselessRegression.lean Challenge statement: Subquadratic and fixed-quadratic memory–precision lower bounds
OAI.NuclearUltrapower.G The exact group of the semidirect-product construction
OAI.NuclearUltrapower.BoundedSeq Bounded sequences, with their supremum norm
OAI.NuclearUltrapower.ultraRel Equality modulo I_omega(B)
OAI.NuclearUltrapower.ultraCon The ring congruence defining the norm (not algebraic) ultrapower
OAI.NuclearUltrapower.NormUltrapower The exact quotient l-infinity(N,B)/I_omega(B) as a complex star algebra
OAI.NuclearUltrapower.IsFree Freeness: no finite subset of N belongs to the ultrafilter
OAI.NuclearUltrapower.ComplexHilbert A bundled complex Hilbert space, without any separability assumption
OAI.NuclearUltrapower.spatialEval Spatial evaluation of the algebraic tensor product on separate Hilbert spaces
OAI.NuclearUltrapower.commutingEval Evaluation on one Hilbert space; used only when the two ranges commute
OAI.NuclearUltrapower.minTensorNorm The minimal C*-tensor norm: supremum over spatial representations
OAI.NuclearUltrapower.maxTensorNorm The maximal C*-tensor norm: supremum over commuting representations
OAI.NuclearUltrapower.IsNuclear Nuclearity in the tensor-norm convention of the tensor-norm formulation
OAI.NuclearUltrapower.UnitalCStar A nonzero unital complex C*-algebra
OAI.NuclearUltrapower.IsFullGroupAlgebra The universal property defining the full, not the reduced, group C*-algebra
OAI.NuclearUltrapower.CuntzTwoRelations The two Cuntz relations, including unit preservation explicitly
OAI.NuclearUltrapower.IsCuntzTwoAlgebra The universal nonzero unital C*-algebra on the two Cuntz isometries
OAI.NuclearUltrapower.MainStatementWithCuntzCorollary The manuscript's main statement including its explicitly stated O_2 corollary
OAI.NuclearUltrapower.main_no_embedding@ComparatorChallenges/NuclearUltrapower.lean Challenge statement: Kirchberg's $`\mathcal O_2`$ norm-ultrapower embedding problem
OAI.CubeShuffle.Specht.hilbertSpace Challenge statement: Row–column overlap on occupied boards
OAI.CubeShuffle.Specht.unitaryRepresentation@ComparatorChallenges/OccupiedOverlap.lean Challenge statement: Row–column overlap on occupied boards
OAI.CubeShuffle.Specht.relabelledUnitary@ComparatorChallenges/OccupiedOverlap.lean Challenge statement: Row–column overlap on occupied boards
OAI.CubeShuffle.UnitaryFinite.IsUnitary@ComparatorChallenges/OccupiedOverlap.lean Challenge statement: Row–column overlap on occupied boards
OAI.RowColumn.lineGroup Permutations preserving each fibre of a given line map
OAI.RowColumn.InHook Zero-based form of the manuscript's (h,h)-hook
OAI.RowColumn.Intertwines An actual equivariant inclusion, not an unspecified overlap matrix
OAI.RowColumn.CompleteCopies All orthogonal multiplicity copies of one irreducible type
OAI.RowColumn.allCopyOverlap The all-copy operator-overlap sum, with each squared operator norm
OAI.RowColumn.OccupiedOverlapEndpoint Challenge statement: Row–column overlap on occupied boards
OAI.RowColumn.occupied_overlap_endpoint@ComparatorChallenges/OccupiedOverlap.lean Challenge statement: Row–column overlap on occupied boards
OAI.RowColumn.occupied_overlap@ComparatorChallenges/OccupiedOverlap.lean Challenge statement: Row–column overlap on occupied boards
OAI.OddKaplansky.main_theorem@ComparatorChallenges/OddKaplansky.lean Challenge statement: Prescribed odd-characteristic counterexample
OAI.Fifths.Single.capped@ComparatorChallenges/OneTapeSpace.lean Challenge statement: One-tape time simulation in two-fifths-power space
OAI.Fifths.Single.unknown@ComparatorChallenges/OneTapeSpace.lean Challenge statement: One-tape time simulation in two-fifths-power space
OAI.OneWayLiveness.BRel.live Nonemptiness is the existence of a path through the word's ordered product
OAI.OneWayLiveness.scanned The finite word including both endmarkers
OAI.OneWayLiveness.FiniteRun The positive convention explicitly excludes a length-zero computation
OAI.OneWayLiveness.main_theorem@ComparatorChallenges/OneWayLiveness.lean Challenge statement: Exponential deterministic state lower bound for liveness
OAI.MaxCutGames.BinaryFormula.Formula An ordinary conjunction of three-slot clauses with sparse variable names
OAI.MaxCutGames.BinaryEncoding.frame Prefix-free framing on the two-symbol input alphabet
OAI.MaxCutGames.BinaryEncoding.parseName Equality with the canonical digits rejects alternate padded encodings
OAI.MaxCutGames.BinaryEncoding.parseClauses Fuel bounds the number of clause iterations, not the size of any name
OAI.OptimalMaxCut.alphaGW The exact Goemans–Williamson ratio, as an infimum over -1 ≤ ρ < 1
OAI.OptimalMaxCut.binary3SAT The ordinary binary 3SAT language, including rejection of malformed words
OAI.OptimalMaxCut.Graph A finite simple unweighted graph with its full Boolean adjacency table
OAI.OptimalMaxCut.Graph.cutSize Each unordered distinct edge crossing the cut is counted exactly once
OAI.OptimalMaxCut.Graph.maxCut The maximum over all Boolean cuts of the finite vertex set
OAI.OptimalMaxCut.ScaledGraph The positive integer scale Q is part of the output
OAI.OptimalMaxCut.ScaledGraph.bits Canonical delimited binary vertex count and scale, followed by the full adjacency table in lexicographic order
OAI.OptimalMaxCut.GapReduction The rational gap bounds and the finite machine are fixed before the input
OAI.OptimalMaxCut.main@ComparatorChallenges/OptimalMaxCut.lean Challenge statement: Optimal Max-Cut hardness gap
OAI.OrdinaryCorrelations.binary_corrected_elliott@ComparatorChallenges/OrdinaryElliott.lean Challenge statement: Ordinary Elliott cancellation under uniform nonpretentiousness
OAI.OrdinaryTwoPointCorrelations.liouville_log_saving@ComparatorChallenges/OrdinaryTwoPointCorrelations.lean Challenge statement: Ordinary Liouville and multiplicative two-point correlations
OAI.OrdinaryTwoPointCorrelations.binary_corrected_elliott@ComparatorChallenges/OrdinaryTwoPointCorrelations.lean Challenge statement: Ordinary Liouville and multiplicative two-point correlations
OAI.OrdinaryTwoPointCorrelations.affine_corrected_elliott@ComparatorChallenges/OrdinaryTwoPointCorrelations.lean Challenge statement: Ordinary Liouville and multiplicative two-point correlations
OAI.Ostmann.inverseGoldbach@ComparatorChallenges/OstmannComplete.lean Challenge statement: Ostmann's inverse Goldbach theorem and the infinite-summands case
OAI.Ostmann.twoInfiniteSummandsImpossible@ComparatorChallenges/OstmannComplete.lean Challenge statement: Ostmann's inverse Goldbach theorem and the infinite-summands case
OAI.Ostmann.main@ComparatorChallenges/OstmannPrimes.lean Challenge statement: Additive indecomposability of the primes up to finite changes
OAI.ParityWL.parity_reduction@ComparatorChallenges/ParityLifts.lean Challenge statement: Parity-lift characterization of Weisfeiler–Leman equivalence
OAI.PartialPermutation.complementaryCosets_finite@ComparatorChallenges/PartialPermutation.lean Challenge statement: Fourier bounds from complementary coset caps
OAI.PartitionConsistency.Formula Pure first-order membership syntax with equality
OAI.PartitionConsistency.Formula.liftRen Under a binder, a renaming leaves the newly bound variable bound
OAI.PartitionConsistency.Formula.rename Capture-avoiding renaming; in this relational language all terms are variables
OAI.PartitionConsistency.Formula.instantiate Substitution of a variable term for the variable just quantified
OAI.PartitionConsistency.Formula.close Universal closure of all the free variables
OAI.PartitionConsistency.Derives Classical first-order natural deduction with equality
OAI.PartitionConsistency.Theory.at Sentences are usable as open hypotheses with any finite supply of variables
OAI.PartitionConsistency.Consistent Ordinary syntactic consistency: there is no finite natural-deduction proof of falsity from the theory, with any finite supply of free variables
OAI.PartitionConsistency.SetLanguage.subset a ⊆ b
OAI.PartitionConsistency.SetLanguage.empty a = ∅
OAI.PartitionConsistency.SetLanguage.nonempty a ≠ ∅, stated as existence of a member
OAI.PartitionConsistency.SetLanguage.unorderedPair p = {x,y}
OAI.PartitionConsistency.SetLanguage.successor b = a ∪ {a}
OAI.PartitionConsistency.SetLanguage.orderedPair Kuratowski ordered pair: p = {{x},{x,y}}
OAI.PartitionConsistency.SetLanguage.edge The internal graph relation ⟨x,y⟩ ∈ f
OAI.PartitionConsistency.SetLanguage.functionOn f is a set graph of a function whose domain is exactly d
OAI.PartitionConsistency.SetLanguage.mapsTo Internal set function f : d → r
OAI.PartitionConsistency.SetLanguage.surjection Internal set surjection f : d ↠ r
OAI.PartitionConsistency.SetLanguage.injection Internal set injection f : d ↪ r
OAI.PartitionConsistency.SetLanguage.transitiveSet Transitivity of a set (not transitivity of the external structure)
OAI.PartitionConsistency.SetLanguage.membershipLinear Membership is an internal strict linear order on a
OAI.PartitionConsistency.SetLanguage.membershipWellFounded Every nonempty internal subset of a has a membership-minimal element
OAI.PartitionConsistency.SetLanguage.ordinal A von Neumann ordinal: a transitive set internally wellordered by membership
OAI.PartitionConsistency.SetLanguage.choiceOn A choice function on the set A of nonempty sets
OAI.PartitionConsistency.SetLanguage.nonemptyFamily A graph F coding a family of nonempty sets indexed by ordinal η
OAI.PartitionConsistency.SetLanguage.choiceForFamily c(ξ) ∈ F(ξ) for every ξ ∈ η, with c an internal function
OAI.PartitionConsistency.SetLanguage.PP The Partition Principle
OAI.PartitionConsistency.SetLanguage.AC Ordinary Choice for every set of nonempty sets
OAI.PartitionConsistency.SetLanguage.ACwo Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model
OAI.PartitionConsistency.SetLanguage.separation The instance of Separation for an entirely arbitrary formula p(params,x)
OAI.PartitionConsistency.SetLanguage.relation Substitution into a binary formula with n additional parameters
OAI.PartitionConsistency.SetLanguage.replacement The instance of Replacement for an entirely arbitrary formula p(params,x,y): if it is single-valued and total on A, its image is a set
OAI.PartitionConsistency.SetLanguage.IsZFAxiom Exactly the axioms and all schema instances of pure first-order ZF
OAI.PartitionConsistency.SetLanguage.ZF Zermelo–Fraenkel set theory, without Choice
OAI.PartitionConsistency.SetLanguage.targetTheory ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice
OAI.PartitionConsistency.main_consistency@ComparatorChallenges/PartitionConsistency.lean Challenge statement: Relative consistency of the Partition Principle with ordinal Choice and failure of Choice
OAI.PartitionPilot.Forcing.TransitiveGround.exists_model_partitionPrinciple_without_choice@ComparatorChallenges/PartitionPrinciple.lean Challenge statement: Partition Principle without Choice from a ground model
OAI.CubicFirstMoment.patterson_firstMoment@ComparatorChallenges/PattersonFirstMoment.lean Challenge statement: Patterson's first moment for cubic Gauss sums
OAI.CubicFirstMoment.patterson_angularComparison@ComparatorChallenges/PattersonFirstMoment.lean Challenge statement: Patterson's first moment for cubic Gauss sums
OAI.CubicFirstMoment.patterson_angularCancellation@ComparatorChallenges/PattersonFirstMoment.lean Challenge statement: Patterson's first moment for cubic Gauss sums
OAI.SphericalPerceptronFreeEnergy.main@ComparatorChallenges/PerceptronFreeEnergy.lean Challenge statement: Variational formula for spherical-perceptron pressure
OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord Encode one natural number in unary with a zero terminator
OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords Concatenate a list of unary natural-number words
OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet Every physical tape of the reduction machine has a finite alphabet
OAI.PerfectCompleteness.Theorem11.exists_reduction@ComparatorChallenges/PerfectCompleteness.lean Challenge statement: Perfect completeness for 2-to-1 games
OAI.SourceBurnside.thm_main@ComparatorChallenges/PeriodicGroup.lean Challenge statement: An infinite finitely presented residually finite 2-group and a finitely presented nil algebra
OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality@ComparatorChallenges/PeriodicTilingThree.lean Challenge statement: A counterexample to periodic tiling in dimension three
OAI.PermanentBorder.permanent_cubic_lower_bounds@ComparatorChallenges/PermanentCubic.lean Challenge statement: Cubic lower bounds for permanent determinantal complexity
OAI.PettyProjection.shadowVolume Volume in the induced Euclidean structure on the orthogonal hyperplane
OAI.PettyProjection.projectionBody The body with support function equal to the volumes of orthogonal shadows, expressed as its defining intersection of supporting half-spaces
OAI.PettyProjection.petty_projection_volume@ComparatorChallenges/PettyProjectionVolume.lean Challenge statement: Petty's projection-volume inequality
OAI.PiExponent.main@ComparatorChallenges/PiExponent.lean Challenge statement: The irrationality exponent of π is exactly 2
OAI.PinchedHartogs.main_theorem@ComparatorChallenges/PinchedKahler.lean Challenge statement: Negative Kähler curvature without bounded holomorphic coordinates
OAI.PinchedHartogs.controlled_potential@ComparatorChallenges/PinchedKahler.lean Challenge statement: Negative Kähler curvature without bounded holomorphic coordinates
OAI.PinchedHartogs.metric_transfer@ComparatorChallenges/PinchedKahler.lean Challenge statement: Negative Kähler curvature without bounded holomorphic coordinates
OAI.WeakPinned.main@ComparatorChallenges/PinnedDistances.lean Challenge statement: Weak pinned planar distance theorem
OAI.PlanarAnderson.anderson_spectrum_ae@ComparatorChallenges/PlanarAndersonSpectrum.lean Challenge statement: Localization and delocalization in the Anderson model
OAI.PlanarFalconer.mainTarget_proved@ComparatorChallenges/PlanarFalconer.lean Challenge statement: Planar Falconer distance theorem
OAI.PlanarFPP.manuscriptMain@ComparatorChallenges/PlanarFirstPassage.lean Challenge statement: Differentiability of the exponential first-passage limit shape
OAI.PlanarL1.IsPlanar A topological drawing by simple plane arcs, with injective vertex placement, no vertex in an edge interior, and disjoint interiors for distinct unoriented edges
OAI.PlanarL1.walkLength The sum of edge lengths along a finite graph walk
OAI.PlanarL1.graphDistance The infimum of lengths of actual walks between the two vertices
OAI.PlanarL1.MainStatement One universal distortion bound for finite connected planar graphs with arbitrary symmetric positive edge lengths, realized in a real L¹ space
OAI.PlanarL1.planar_graph_metrics_embed_L1@ComparatorChallenges/PlanarL1.lean Challenge statement: Planar graph metrics in $L_1$
OAI.SharpPlanar.Radial Radiality of a real function on the Euclidean plane
OAI.SharpPlanar.fourier Fourier transformation with kernel exp (-2πi⟪x, ξ⟫)
OAI.SharpPlanar.SharpCertificate A normalized sharp certificate for disks of radius one half
OAI.sharp_fourier_certificate@ComparatorChallenges/PlanarPacking.lean Challenge statement: Sharp Fourier certificate for planar circle packing
OAI.PlanarUnitDistances.main@ComparatorChallenges/PlanarUnitDistances.lean Challenge statement: Power saving for planar unit distances
OAI.Problem160.properColoring_seven@ComparatorChallenges/PlaneColoring.lean Challenge statement: Proper seven-coloring
OAI.PolycyclicRecognition.GroupBornologous Uniform control of finite sets of group differences
OAI.PolycyclicRecognition.GroupCoarseEquivalence Coarse inverse maps with errors contained in fixed finite sets
OAI.PolycyclicRecognition.IsPolycyclic Polycyclicity expressed by an actual cyclic subnormal series
OAI.PolycyclicRecognition.IsVirtuallyPolycyclic@ComparatorChallenges/PolycyclicRecognition.lean Virtual polycyclicity means a polycyclic subgroup of finite index
OAI.PolycyclicRecognition.IsUniformLattice@ComparatorChallenges/PolycyclicRecognition.lean A uniform lattice is discrete and has a compact fundamental cover
OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel A connected simply connected finite-dimensional real solvable Lie group
OAI.PolycyclicRecognition.IsFiniteCovolumeLattice A discrete subgroup with a normalized invariant measure on its coset space
OAI.PolycyclicRecognition.LinearMetricChains@ComparatorChallenges/PolycyclicRecognition.lean Explicit chains with bounded steps and a linear bound on their length
OAI.PolycyclicRecognition.ProperChainMetric A compatible proper left-invariant metric with large-scale-geodesic chains
OAI.PolycyclicRecognition.ProperChainMetric.compatibleMetric@ComparatorChallenges/PolycyclicRecognition.lean The compatible metric retains the original topology definitionally
OAI.PolycyclicRecognition.heightKernel The common kernel, including the empty family of characters
OAI.PolycyclicRecognition.HeightSpace The canonical linear height quotient
OAI.PolycyclicRecognition.heightProjection The quotient map defining infinitesimal height
OAI.PolycyclicRecognition.TriangularAdjoint A simultaneous real upper triangular basis for the adjoint representation
OAI.PolycyclicRecognition.TriangularAdjoint.character@ComparatorChallenges/PolycyclicRecognition.lean The diagonal entries of the adjoint representation
OAI.PolycyclicRecognition.IsGroupExponential@ComparatorChallenges/PolycyclicRecognition.lean The exponential is characterized by its one-parameter subgroups and by their tangent vectors at the identity
OAI.PolycyclicRecognition.ModelIsUnimodular Unimodularity for the canonical Borel Haar measure of the Lie group
OAI.PolycyclicRecognition.SelfQuasiIsometry@ComparatorChallenges/PolycyclicRecognition.lean The upper, lower, and coarse-surjectivity bounds of a self quasi-isometry
OAI.PolycyclicRecognition.group_recognition@ComparatorChallenges/PolycyclicRecognition.lean Challenge statement: Quasi-isometric recognition of virtually polycyclic groups
OAI.PolycyclicRecognition.main_uniform_bounded_height@ComparatorChallenges/PolycyclicRecognition.lean Challenge statement: Quasi-isometric recognition of virtually polycyclic groups
OAI.PolycyclicRecognition.lattice_recognition@ComparatorChallenges/PolycyclicRecognition.lean Challenge statement: Quasi-isometric recognition of virtually polycyclic groups
OAI.PosteriorReplicas.source_main@ComparatorChallenges/PosteriorReplicas.lean Challenge statement: Posterior-replica comparisons and sample lower bound
OAI.QuarticPowerFree.allDegrees@ComparatorChallenges/PowerFreeValues.lean Challenge statement: Squarefree quartics and power-free polynomial values
OAI.Problem344.large_gaps_and_ratio_density@ComparatorChallenges/PrimeGaps.lean Challenge statement: Positive lower density of large prime gaps
OAI.FiniteFactor.productBrown@ComparatorChallenges/ProductBrown.lean Challenge statement: Brown measure of the selected product weighted shift
OAI.ProjectionCounterexample.universal_simplex_upper_bound_false@ComparatorChallenges/ProjectionCounterexample.lean Challenge statement: Failure of the simplex upper bound in dimension 20
OAI.ProjectionMoments.main@ComparatorChallenges/ProjectionMoments.lean Challenge statement: Projection, cap, and Riesz estimates with regression bounds
OAI.Paper092.product_counterexample@ComparatorChallenges/ProjectionVolume.lean Challenge statement: Explicit product-of-simplices counterexample
OAI.QAC.tensorMatrix Tensor product in the computational basis
OAI.QAC.Gate A one-qubit unitary or an unbounded-arity Toffoli gate
OAI.QAC.Gate.toffoliWord A Toffoli flips its target iff all controls are one
OAI.QAC.physicalCircuitMatrix Chronological order: the rightmost matrix acts first
OAI.QAC.inputWord The computational-basis input with the remaining qubits initialized to zero
OAI.QAC.successProbability Born probability, summing all final garbage with no cleanliness assumption
OAI.QAC.ParityStatement The literal measured-output, polynomial-total-qubit parity lower bound
OAI.QAC.parity_lower_bound@ComparatorChallenges/QACParity.lean Challenge statement: Constant-depth quantum parity lower bound
OAI.QuadricCounterexample.main_theorem@ComparatorChallenges/QuadricBundles.lean Challenge statement: A counterexample to Griffiths’ positivity conjecture
OAI.QuantitativeVanDerWaerden.W@ComparatorChallenges/QuantitativeVanDerWaerden.lean The least positive Ramsey interval size
OAI.QuantitativeVanDerWaerden.uniform_lower_bound@ComparatorChallenges/QuantitativeVanDerWaerden.lean Challenge statement: Superexponential van der Waerden numbers
OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re@ComparatorChallenges/QuasiRiemannHypothesis.lean Challenge statement: Zero-free half-plane for the Riemann zeta function
OAI.QuinticLienard.main@ComparatorChallenges/QuinticLienard.lean Challenge statement: Exactly two is the sharp limit-cycle bound for quintic Liénard systems
OAI.RadialTransition.densityInterval@ComparatorChallenges/RadialDensityInterval.lean Challenge statement: A common radial phase transition over a density interval
OAI.RadialTransition.main@ComparatorChallenges/RadialTransition.lean Challenge statement: Fixed-density radial continuum phase transition
OAI.SharpRamseyFive.main@ComparatorChallenges/RamseyFive.lean Challenge statement: Sharp logarithmic exponent of $r(5,t)$
OAI.randomized_quasipolynomial_mean_payoff@ComparatorChallenges/RandomizedMeanPayoff.lean Challenge statement: Randomized quasipolynomial mean-payoff algorithm
OAI.RationalHitting.Formula.Eval Evaluation in any rational algebra; a unary inverse requires an actual two-sided inverse of the evaluated operand, not a totalized inverse
OAI.RationalHitting.Output All output tuples have one common positive dimension
OAI.RationalHitting.encodeNat Little-endian unsigned binary, prefixed by a unary bit-length and a zero terminator
OAI.RationalHitting.encodeRat Sign bit, binary numerator magnitude, and positive binary denominator
OAI.RationalHitting.Alphabet 0 is blank, 1 and 2 are the two literal binary digits, 3 is work space
OAI.RationalHitting.run Exactly t ordinary deterministic TM0 transitions
OAI.RationalHitting.MainStatement A fixed polynomial bound on bit time, full binary output length, and common positive dimension
OAI.RationalHitting.main@ComparatorChallenges/RationalHitting.lean Challenge statement: Polynomial hitting lists for rational formulas
OAI.DiscreteFree.real_l1_quantitative_renorming@ComparatorChallenges/RealL1Renorming.lean Challenge statement: Quantitative renorming of real $\ell_1$
OAI.ComparatorModel.RecursivePotentials.main@ComparatorChallenges/RecursivePotentials.lean Challenge statement: Recursive-potential spaces and midpoint convexity
OAI.ReflexiveFixedPoints.CanonicallyReflexive Surjectivity of the canonical map into the continuous bidual
OAI.ReflexiveFixedPoints.exists_fixedPoint_of_canonicallyReflexive@ComparatorChallenges/ReflexiveFixedPoints.lean Challenge statement: Nonexpansive fixed points in reflexive Banach spaces
OAI.QAC.parity_lower_bound_polynomial_size@ComparatorChallenges/RegularParity.lean Challenge statement: Polynomial-size parity specialization
OAI.RelativeGeneration.WOTClosed Weak operator closedness of a concrete unital star subalgebra
OAI.RelativeGeneration.wstar The weakly closed unital star algebra generated by a set of operators
OAI.RelativeGeneration.IsII1Factor A nonzero, weakly closed, finite diffuse algebra with scalar center
OAI.RelativeGeneration.HasSeparablePredual A same-universe separable Banach predual, with the conjugate-linear dual convention
OAI.RelativeGeneration.ultraweakTopology The ultraweak topology is generated by absolutely summable vector functionals
OAI.RelativeGeneration.algebraUltraweakTopology The concrete algebra carries the induced ultraweak topology
OAI.RelativeGeneration.IsNormalizedTrace A faithful normal normalized trace, not an additional hypothesis on the inclusion
OAI.RelativeGeneration.traceDistance The normalized trace two-distance between genuine unitaries of the original algebra
OAI.RelativeGeneration.traceTopology The topology generated by trace two-distance balls, not the inherited operator norm topology
OAI.RelativeGeneration.relativeGeneratorLocus The entire relative-generator locus in the original unitary group
OAI.RelativeGeneration.MainTarget Documented declaration: MainTarget
OAI.RelativeGeneration.main_theorem@ComparatorChallenges/RelativeGeneration.lean Challenge statement: Dense relative generators for irreducible inclusions of finite factors
OAI.RieszRectifiability.QuantitativeFullStatement A single mass fraction and Lipschitz bound work for all measures with fixed AD and Riesz bounds
OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability@ComparatorChallenges/RieszQuantitative.lean Challenge statement: Riesz transforms and rectifiability in higher codimension
OAI.Rokhlin.timeMap Challenge statement: Rokhlin’s multiple-mixing problem
OAI.Rokhlin.IsMixing Challenge statement: Rokhlin’s multiple-mixing problem
OAI.Rokhlin.layoutTime Challenge statement: Rokhlin’s multiple-mixing problem
OAI.Rokhlin.MixingOfOrder Challenge statement: Rokhlin’s multiple-mixing problem
OAI.Rokhlin.mixing_all_finite_orders@ComparatorChallenges/Rokhlin.lean Challenge statement: Ordinary mixing implies mixing of every finite order
OAI.RuledApproximation.tetrahedron The regular edge-2 tetrahedron in physical coordinates
OAI.RuledApproximation.fullMain@ComparatorChallenges/RuledCovering.lean Challenge statement: Finite cylinder approximation for the selected ruled families
OAI.RyserCoveringCounterexample.exists_prime_eventually_counterexampleRank@ComparatorChallenges/RyserCovering.lean Challenge statement: Fixed-prime Ryser counterexamples
OAI.RyserOdd.eventualOddFailures_and_infinite@ComparatorChallenges/RyserOddExtensions.lean Challenge statement: Counterexamples in odd extension degrees
OAI.FixedClauseThreshold.Computability.main@ComparatorChallenges/SATComputability.lean Challenge statement: Computability of the random $3$-SAT threshold
OAI.RandomKSAT.sharpness@ComparatorChallenges/SATSharpness.lean Challenge statement: Sharpness of random $k$-SAT lifetime and replacement bounds
OAI.RandomKSAT.variance_main@ComparatorChallenges/SATVariance.lean Challenge statement: Variance bounds for the random $k$-SAT hitting time
OAI.SK.main@ComparatorChallenges/SKBarriers.lean Challenge statement: Stretched-exponential barriers from typical equilibrium initial states
OAI.ZeroTemperatureSK.full_support@ComparatorChallenges/SKFullSupport.lean Challenge statement: Full support of zero-temperature SK minimizers
OAI.SKGap.conditionalExpectation Conditional expectation under the actual Gibbs law given all other spins
OAI.SKGap.dirichlet Unscaled form: each site has a rate-one clock
OAI.SKGap.discreteGap Rayleigh quotient definition of the uniform-site discrete heat-bath gap
OAI.SKGap.sk_main@ComparatorChallenges/SKHighTemperature.lean Challenge statement: Spectral-gap bound throughout the high-temperature SK phase
OAI.SKRatio.ratio_cutoff@ComparatorChallenges/SKRatio.lean Challenge statement: Discrete mixing-time ratio cutoff for $\beta<1/2$
OAI.SKValue.value_consequences@ComparatorChallenges/SKValue.lean Challenge statement: Parisi ground-state value identities and finite Gaussian approximation
OAI.SLEExactGauge.sourceLowerMain_proved@ComparatorChallenges/SLELowerPositivity.lean Challenge statement: Exact Hausdorff gauges for SLE
OAI.Saxl.saxl_conjecture@ComparatorChallenges/Saxl.lean Challenge statement: Saxl's conjecture
OAI.LeanBlast.SecondKahnKalai.Edge The unordered non-loop edges of the complete graph on n vertices
OAI.LeanBlast.SecondKahnKalai.graphOfEdges A set of edges, interpreted as an ordinary graph on all n vertices
OAI.LeanBlast.SecondKahnKalai.edgeCount The number of unordered edges, each counted once
OAI.LeanBlast.SecondKahnKalai.expectedCopies Expected number of actual unlabelled non-induced copies in G(n,p)
OAI.LeanBlast.SecondKahnKalai.containmentProbability Probability that G(n,p) contains at least one non-induced copy
OAI.LeanBlast.SecondKahnKalai.secondKahnKalaiBounds@ComparatorChallenges/SecondKahnKalai.lean Challenge statement: The second Kahn–Kalai conjecture with an edge-count bound
OAI.EntropyRateDimension.entropy_rate_dimension@ComparatorChallenges/SelfSimilar.lean Challenge statement: Entropy-rate dimension formula
OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct@ComparatorChallenges/SelfSimilarCorollaries.lean Challenge statement: Homogeneous-measure and self-similar-attractor dimension formulas
OAI.CorSetReference.cor_set@ComparatorChallenges/SelfSimilarCorollaries.lean Challenge statement: Homogeneous-measure and self-similar-attractor dimension formulas
OAI.Paper320.quantitative_separation@ComparatorChallenges/SensitivitySeparation.lean Challenge statement: A superquadratic separation of sensitivity and block sensitivity
OAI.SeparableQuotient.CH The continuum hypothesis
OAI.SeparableQuotient.HasSeparableQuotient A bounded linear surjection onto an infinite-dimensional separable Banach space
OAI.SeparableQuotient.SQ The separable quotient assertion at an arbitrary ambient universe
OAI.SeparableQuotient.negative_main@ComparatorChallenges/SeparableQuotientNegative.lean Challenge statement: Independence of the separable quotient problem
OAI.SeymourSecondNeighborhood.IsOriented The loopless, asymmetric relation underlying an oriented graph
OAI.SeymourSecondNeighborhood.firstNeighbors The first out-neighborhood of a vertex
OAI.SeymourSecondNeighborhood.secondNeighbors Vertices at directed distance exactly two
OAI.SeymourSecondNeighborhood.GoodVertex A vertex with at least as many second as first out-neighbors
OAI.SeymourSecondNeighborhood.exists_goodVertex@ComparatorChallenges/SeymourSecondNeighborhood.lean Challenge statement: Seymour's second-neighborhood conjecture
OAI.CAT0Fillings.sharp_integral_filling@ComparatorChallenges/SharpCAT0Filling.lean Challenge statement: Sharp integral fillings in proper $\mathrm{CAT}(0)$ spaces
OAI.SharpLogRamsey.RamseyProperty Every graph has an s-clique or an independent set of size t
OAI.SharpLogRamsey.MainBounds The upper-bound constant is chosen independently of epsilon
OAI.SharpLogRamsey.MainLimit The logarithmic exponent converges along all natural orders
OAI.SharpLogRamsey.main@ComparatorChallenges/SharpLogRamsey.lean Challenge statement: Sharp logarithmic exponent for fixed off-diagonal Ramsey numbers
OAI.Problem313.sharp_threshold_width@ComparatorChallenges/SharpThreshold.lean Challenge statement: Uniform influence and sharp thresholds for graph and hypergraph properties
OAI.ShortEgyptian.main@ComparatorChallenges/ShortEgyptianFractions.lean Challenge statement: The optimal uniform length of Egyptian-fraction expansions
OAI.SidorenkoCounterexample.main@ComparatorChallenges/SidorenkoCounterexample.lean Challenge statement: Counterexamples to Sidorenko’s conjecture and the forcing conjecture
OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap@ComparatorChallenges/SiegelZeros.lean Challenge statement: Uniform gap for real zeros of L-functions
OAI.SiegelZeros.WeightedTorusJets.dirichletRealZeroBound_proof@ComparatorChallenges/SiegelZeros.lean Challenge statement: Uniform real-zero gap
OAI.SignedDisk.CenteredDiskEndpoint.Plane The Euclidean plane, with its Euclidean norm
OAI.SignedDisk.CenteredDiskEndpoint.testPartial The i-th coordinate derivative of a smooth test function
OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient Distributional first derivatives represented by a vector-valued function
OAI.SignedDisk.CenteredDiskEndpoint.gradientNorm The gradient L1 norm in Euclidean norm
OAI.SignedDisk.CenteredDiskEndpoint.signedBand Signed envelope over all real radii in the closed band, including its endpoints
OAI.SignedDisk.CenteredDiskEndpoint.main_signed_finite_band@ComparatorChallenges/SignedFiniteBand.lean Challenge statement: Signed finite-band disk-maximal gradient bound
OAI.SignedSweeps.signed_occurrence_moment_bound@ComparatorChallenges/SignedSweepMoment.lean Challenge statement: Uniform signed-occurrence moment bound for coordinate sweeps
OAI.SimpleAmenable.main@ComparatorChallenges/SimpleAmenable.lean Challenge statement: An infinite finitely presented simple amenable group
OAI.SimpleFInftyOvergroups.main@ComparatorChallenges/SimpleOvergroups.lean Challenge statement: Simple type $F_\infty$ overgroups of groups with decidable word problem
OAI.SingleFold.evalNat Evaluation over the integers of an integer polynomial at natural inputs
OAI.SingleFold.Represents Exact existence on members, no witness on nonmembers, and uniqueness of the whole witness on every input
OAI.SingleFold.MainStatement Single-fold representation with positive input and witness lengths
OAI.SingleFold.main@ComparatorChallenges/SingleFold.lean Challenge statement: Single-fold Diophantine representations and undecidability under an at-most-one-solution promise
OAI.SingleLatticeCovering.single_lattice_covering@ComparatorChallenges/SingleLatticeCovering.lean Challenge statement: Single-lattice covering bound
OAI.LoopMatching.fullEndpoint@ComparatorChallenges/SingletonLoopMatching.lean Challenge statement: Approximate counting with singleton loops
OAI.PermanentBorder.smooth_initial_form_lower_bound@ComparatorChallenges/SmoothInitialForm.lean Challenge statement: Determinantal lower bound from a smooth initial form
OAI.SmoothObstruction.entropyTerm Shannon entropy in bits; the value at mass zero is zero
OAI.SmoothObstruction.blockEntropy The entropy of the length-n join of the partition with labels in Fin q
OAI.SmoothObstruction.FiniteKSEntropy All finite-partition entropy rates exist and have one finite real upper bound
OAI.SmoothObstruction.ConullIsomorphic Measure-space isomorphism after removing measurable null sets
OAI.SmoothObstruction.StandardNonatomic Standard nonatomic in the source's explicit modulo-null-set sense
OAI.SmoothObstruction.ConullConjugate Measurable conjugacy on invariant conull measurable subsets, not a continuous conjugacy and not merely a factor map
OAI.SmoothObstruction.SmoothPositiveDensity Positive smooth local coordinate densities
OAI.SmoothObstruction.HasModelWith A smooth positive-volume model with a specified Euclidean or half-space manifold model
OAI.SmoothObstruction.HasSmoothPositiveVolumeModel Closed manifolds of all dimensions (including zero), and smooth manifolds with boundary of every positive finite dimension
OAI.SmoothObstruction.main@ComparatorChallenges/SmoothObstruction.lean Challenge statement: Zero entropy does not guarantee a smooth positive-volume model
OAI.YauCounterexamples.SmoothMetric Ordinary smooth positive-definite Riemannian metrics, with the existing tangent topology
OAI.YauCounterexamples.coordinateVector A coordinate vector, pushed from a chart back into the tangent bundle
OAI.YauCounterexamples.metricCoefficients Metric coefficients in a chart
OAI.YauCounterexamples.laplaceBeltrami The local coordinate formula det(g)^(-1/2) d_i(det(g)^(1/2) g^{ij} d_j u)
OAI.YauCounterexamples.CoordinateTest One compact-chart seminorm test for the usual smooth topology of metrics
OAI.YauCounterexamples.IsSmoothNeighborhood The finite compact-chart derivative tests defining a C∞ neighborhood
OAI.YauCounterexamples.nodalMeasure Hausdorff measure for the path distance of the actual Riemannian metric, not the metric inherited from any ambient embedding
OAI.YauCounterexamples.HasUnboundedNodalRatio The eigensequence belongs to one fixed metric and has finite nodal measure
OAI.YauCounterexamples.IsRound The round metric is the pullback of the Euclidean scalar product under inclusion of the unit sphere
OAI.YauCounterexamples.sphere_three@ComparatorChallenges/SmoothYau.lean Challenge statement: Nodal counterexamples in dimensions three and four
OAI.YauCounterexamples.sphere_two_torus_two@ComparatorChallenges/SmoothYau.lean Challenge statement: Nodal counterexamples in dimensions three and four
OAI.SnakyCertificate.certificate_correct@ComparatorChallenges/SnakyCertificate.lean Challenge statement: Reconstruction of the 35-move Snaky certificate
OAI.SnakyConditional.snaky_winning_strategy_with_legal_states@ComparatorChallenges/SnakyConditional.lean Challenge statement: Conditional winning templates from finite partial positions
OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states@ComparatorChallenges/SnakyTwentyOne.lean Challenge statement: Legal Snaky winning strategy within 21 Maker moves
OAI.SoftChannel204.F Defined by this formula on [0, L); no finite endpoint value at L is asserted
OAI.SoftChannel204.S The excess F s - 2 * s, used for s < L, is extended by zero to negative arguments
OAI.SoftChannel204.reserve The reserve is used for |m| < 1 and 0 ≤ I < H m
OAI.SoftChannel204.fullMain@ComparatorChallenges/SoftChannel204.lean Challenge statement: Sharp binary-channel contraction and entropy production
OAI.Solenoidal.sheet_theorem@ComparatorChallenges/SolenoidalSheetPrograms.lean Challenge statement: Positive diagonal programs on incompressible coding sheets
OAI.SphericalPerceptron.spherical_linear_field_formula@ComparatorChallenges/SphericalField.lean Challenge statement: Spherical linear-field dual formula and approximation
OAI.SpinAngle.TypeAngle.row Challenge statement: One-sided angle bound for signed spin types
OAI.SpinAngle.TypeAngle.column Challenge statement: One-sided angle bound for signed spin types
OAI.SpinAngle.TypeAngle.phi Challenge statement: One-sided angle bound for signed spin types
OAI.SpinAngle.TypeAngle.one_sided_type_angle@ComparatorChallenges/SpinAngle.lean Challenge statement: One-sided angle bound for signed spin types
OAI.SplitTangent.integrability_main@ComparatorChallenges/SplitTangentIntegrability.lean Challenge statement: Integrability of both holomorphic tangent summands
OAI.SquareDifference.power_saving@ComparatorChallenges/SquareDifference.lean Challenge statement: Power savings for intersective polynomial differences and prime arguments
OAI.SquareRootDegree.main@ComparatorChallenges/SquareRootDegree.lean Challenge statement: Boolean functions violate the square-root degree bound by arbitrary factors
OAI.StableCoordinate.principal_package@ComparatorChallenges/StableCoordinateFour.lean Challenge statement: Degree-five stable noncoordinate with nonrectifiable affine-space fibers
OAI.StandardMapEntropy.main_components@ComparatorChallenges/StandardMapComponents.lean Challenge statement: Positive-area hyperbolic Bernoulli component
OAI.StandardMapEntropy.main_entropy@ComparatorChallenges/StandardMapEntropy.lean Challenge statement: Positive metric entropy for all sufficiently large parameters
OAI.StandardMapEntropy.main_entropy_complete@ComparatorChallenges/StandardMapLyapunov.lean Challenge statement: Positive Lyapunov exponents and entropy
OAI.EuclideanSteinitzBergstrom.main@ComparatorChallenges/SteinitzBergstrom.lean Challenge statement: The Euclidean Steinitz–Bergström bound
OAI.StrictInverseFirstPower.main@ComparatorChallenges/StrictMeans.lean Challenge statement: Strict inverse-first-power bound and consequences
OAI.KadisonKastler.universal_strong_stability@ComparatorChallenges/StrongKadisonKastler.lean Challenge statement: Strong Kadison–Kastler stability and its spatial boundaries
OAI.StrongThinTree.strongThinTree@ComparatorChallenges/StrongThinTree.lean Challenge statement: Strong thin-tree bound
OAI.Problem336AdditiveD139.finite_strongly_rayleigh_response@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.Problem336AdditiveD139.strongly_rayleigh_group_factor@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.Problem336AdditiveD139.finite_positive_contraction_dpp_is_strongly_rayleigh@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.Problem336AdditiveD139.countable_positive_contraction_dpp_exists_unique@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.Problem336AdditiveD139.invariant_positive_contraction_dpp_factor@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.Problem336AdditiveD139.translation_invariant_kernel_dpp_factor@ComparatorChallenges/StronglyRayleighDPP.lean Challenge statement: Strongly Rayleigh and determinantal-process IID factors
OAI.StructuralCrouzeixReference.challenge@ComparatorChallenges/StructuralCrouzeix.lean Challenge statement: Optimal similarity and boundary representation
OAI.SubpolynomialLp.GoodDimension The universal property used in the definition of d_p(n,D)
OAI.SubpolynomialLp.dimension The least universal coordinate dimension
OAI.SubpolynomialLp.source_main@ComparatorChallenges/SubpolynomialLp.lean Challenge statement: Subpolynomial dimension reduction in Lp
OAI.SubsphereCurrent.full_current_main_scope@ComparatorChallenges/SubsphereCurrent.lean Challenge statement: Subsphere estimates and memory–sample lower bounds
OAI.Superstring.encodeList Prefix markers encode the list spine, including its final boundary
OAI.Superstring.IsCommonSuperstring Ordinary contiguous substring containment, including the empty word
OAI.Superstring.opt The optimum in symbols, not in bits
OAI.Superstring.HasPolynomialImplementation A deterministic finite-stack-machine implementation, with a polynomial bound on bit-level running time in the explicitly encoded input length
OAI.Superstring.main@ComparatorChallenges/Superstring.lean Challenge statement: A factor-two approximation for shortest common superstring
OAI.SmallCM.candidate_ring_properties@ComparatorChallenges/SurfaceConeCandidateSupport.lean Challenge statement: A counterexample to the small Cohen–Macaulay module conjecture
OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion@ComparatorChallenges/SurfaceImmersion.lean Challenge statement: Smooth isometric immersions of surfaces into ℝ4
OAI.Problem315.switch_chain_main@ComparatorChallenges/SwitchChain.lean Challenge statement: Rapid mixing of graph switches for every degree sequence
OAI.Problem315.switch_chain_tv_bound@ComparatorChallenges/SwitchChain.lean Challenge statement: Rapid mixing of graph switches for every degree sequence
OAI.Problem315.switch_connectivity@ComparatorChallenges/SwitchChain.lean Challenge statement: Rapid mixing of graph switches for every degree sequence
OAI.Release061.main@ComparatorChallenges/SymmetricDomains.lean Challenge statement: Semialgebraic universal covers and bounded domains
OAI.SymmetricMahler.symmetric_mahler_equality@ComparatorChallenges/SymmetricMahlerEquality.lean Challenge statement: Symmetric Mahler equality characterization
OAI.SymmetricPolar.symmetric_polar_main@ComparatorChallenges/SymmetricPolar.lean Challenge statement: Gromov width of symmetric polar products
OAI.Tachikawa.main_theorem@ComparatorChallenges/Tachikawa.lean Challenge statement: Tachikawa counterexample
OAI.TalagrandDiscreteConvexity.bernoulliMass Independent Bernoulli coordinates, including every absent coordinate
OAI.TalagrandDiscreteConvexity.familyMeasure The probability of an arbitrary family, with no monotonicity condition
OAI.TalagrandDiscreteConvexity.cost Each distinct generator is charged once at the original density
OAI.TalagrandDiscreteConvexity.Covers Every covered set contains a generator
OAI.TalagrandDiscreteConvexity.Small An actual finite containment cover with total cost at most one half
OAI.TalagrandDiscreteConvexity.unionTuple Exactly k entries, with no distinctness or disjointness restriction
OAI.TalagrandDiscreteConvexity.exceptional All subsets contained in no union of k members of the given family
OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity@ComparatorChallenges/TalagrandDiscreteConvexity.lean Challenge statement: Talagrand discrete convexity
OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence@ComparatorChallenges/TalagrandExpectationThreshold.lean Challenge statement: Integral–fractional expectation-threshold comparison
OAI.TamingCompatibility.taming_implies_compatibility@ComparatorChallenges/TamingCompatibility.lean Challenge statement: Donaldson's tamed-to-compatible conjecture
OAI.Thomason.main@ComparatorChallenges/ThomasonModelStructures.lean Challenge statement: Thomason model structures in all strict higher dimensions
OAI.Thomason.nerveDetection_allDimensions@ComparatorChallenges/ThomasonModelStructures.lean Challenge statement: Thomason model structures in all strict higher dimensions
OAI.ThompsonNonamenability.thompson_F_nonamenable_composition@ComparatorChallenges/ThompsonNonamenability.lean Challenge statement: Thompson's group F has no invariant mean
OAI.Thorp.Current.first_reciprocal_main@ComparatorChallenges/ThorpFirstReciprocal.lean Challenge statement: Reciprocal Specht degrees and eight-block Fourier bound
OAI.ThorpResults.remaining_main@ComparatorChallenges/ThorpRemaining.lean Challenge statement: Frame, spectral, and density estimates for Thorp mixing
OAI.ThorpNine.main@ComparatorChallenges/ThorpRouting.lean Challenge statement: Nine routing-density and representation estimates
OAI.ThorpCompatibility.weightedCompatibility_main@ComparatorChallenges/ThorpWeightedCompatibility.lean Challenge statement: Weighted row–column compatibility bound
OAI.ThreeMachine.main_theorem@ComparatorChallenges/ThreeMachine.lean Challenge statement: Polynomial-time scheduling on three identical machines
OAI.ThreeState.regular_supercritical@ComparatorChallenges/ThreeStateSupercritical.lean Challenge statement: Supercritical reconstruction on regular and Poisson trees
OAI.ThreeState.poisson_supercritical@ComparatorChallenges/ThreeStateSupercritical.lean Challenge statement: Supercritical reconstruction on regular and Poisson trees
OAI.ThreeState.TreeClauses.Tree.regular_reconstructs_above_KS@ComparatorChallenges/ThreeStateTreeClauses.lean Challenge statement: Three-state reconstruction above the Kesten–Stigum threshold
OAI.ThreeState.TreeClauses.Tree.poisson_reconstructs_above_KS@ComparatorChallenges/ThreeStateTreeClauses.lean Challenge statement: Three-state reconstruction above the Kesten–Stigum threshold
OAI.ThreeTorus.meanZero The full complex subspace defined by zero Lebesgue integral
OAI.ThreeTorus.MainConclusion Complete simple Lebesgue spectrum, including the stated consequences
OAI.ThreeTorus.simple_lebesgue_spectrum@ComparatorChallenges/ThreeTorus.lean Challenge statement: A smooth probability-preserving system with simple Lebesgue spectrum
OAI.Tingley.tingley_sphere_isometry_full@ComparatorChallenges/TingleySphereIsometry.lean Challenge statement: Every surjective Banach-sphere isometry extends uniquely and linearly
OAI.Release075.TorsionFree No nonidentity element has finite order
OAI.Release075.Geodesic A shortest edge path in the unit-edge graph
OAI.Release075.SideThin Each vertex of p is within δ of a vertex of q or r
OAI.Release075.WordHyperbolic A finitely generated group with a unit-edge Cayley graph whose geodesic triangles are uniformly thin
OAI.Release075.main@ComparatorChallenges/TorsionFreeHyperbolic.lean Challenge statement: A torsion-free hyperbolic group that is neither residually finite nor linear over any field
OAI.TorsionFreeZeroDivisors.TorsionFree Ordinary group torsion-freeness, without requiring uniqueness of all roots
OAI.TorsionFreeZeroDivisors.HasFiniteTwoDimensionalClassifyingSpace A connected finite Hausdorff 2-dimensional CW K(G,1)
OAI.TorsionFreeZeroDivisors.MainTheorem The entire main theorem, including its "Moreover" clause
OAI.TorsionFreeZeroDivisors.main@ComparatorChallenges/TorsionFreeZeroDivisors.lean Challenge statement: A counterexample to Kaplansky’s zero-divisor conjecture
OAI.TotientAsymptotic.totient_asymptotic_formula@ComparatorChallenges/TotientAsymptotic.lean Challenge statement: Totient-count asymptotics and regular variation
OAI.TotientAsymptotic.weighted_totient_asymptotic@ComparatorChallenges/TotientAsymptotic.lean Challenge statement: Totient-count asymptotics and regular variation
OAI.TotientAsymptotic.weighted_totient_one_two@ComparatorChallenges/TotientAsymptotic.lean Challenge statement: Totient-count asymptotics and regular variation
OAI.TotientAsymptotic.coefficient_nonnegative@ComparatorChallenges/TotientAsymptotic.lean Challenge statement: Totient-count asymptotics and regular variation
OAI.TotientAsymptotic.companion_zero_case@ComparatorChallenges/TotientCompanionZero.lean Challenge statement: Exact zero case for the companion totient counts
OAI.TraceConeClassification.closed_ideal_weight_exists@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.zero_mem_finiteSquareSet@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.star_mem_finiteSquareSet@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.smul_mem_finiteSquareSet@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.add_mem_finiteSquareSet@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteSquareSet_left@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.isClosed_finiteIdeal@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_left@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.mul_mem_finiteIdeal_right@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.lowerSemicontinuous_supportWeight@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ClosedIdeal.weight_idempotent@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ClosedIdeal.finiteIdeal_weight@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ClosedIdeal.le_iff_add_weight@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.ExtendedTrace.idempotent_eq_weight@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.closedIdealEquivOfAdditive_weight@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_finIdeal@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_zeroIdeal@ComparatorChallenges/TraceIdealTransportSupport.lean Challenge statement: Trace cones and Razak–Jacelon stabilization
OAI.TraceReconstruction.traceOfMask true retains the bit
OAI.TraceReconstruction.maskWeight The deletion-mask probability, with deletion probability q
OAI.TraceReconstruction.traceMass Law of a single complete trace
OAI.TraceReconstruction.traceSpace All possible complete outputs from length-n inputs, with lengths included
OAI.TraceReconstruction.traceTV 1/2 sum of absolute differences, on the full finite output space
OAI.TraceReconstruction.IsEstimator The estimator may depend arbitrarily on n, q and every complete sample
OAI.TraceReconstruction.reconstructionSuccess Independent masks generate independent complete traces; no retained positions, boundaries or other latent variables are revealed to A
OAI.TraceReconstruction.sampleComplexity Natural fixed sample budget; infimum of the empty set is infinity
OAI.TraceReconstruction.minTraceTV@ComparatorChallenges/TraceReconstruction.lean The real infimum is a minimum for n>0 (a nonempty finite set)
OAI.TraceReconstruction.quantitative_sample_lower_bound@ComparatorChallenges/TraceReconstruction.lean Challenge statement: Quantitative trace-reconstruction bounds with a uniform decoder
OAI.TraceReconstruction.superpolynomial_one_trace@ComparatorChallenges/TraceReconstruction.lean Challenge statement: Quantitative trace-reconstruction bounds with a uniform decoder
OAI.TraceReconstruction.superpolynomial_sample_complexity@ComparatorChallenges/TraceReconstruction.lean Challenge statement: Quantitative trace-reconstruction bounds with a uniform decoder
OAI.TreeEdit.distortion Product of the two maximal pairwise distance ratios
OAI.TreeEdit.c1 Infimum over all injective ℓ₁ maps, used on finite sets with at least two points
OAI.TreeEdit.BinaryLowerBound The binary main endpoint, for every sufficiently large cap (natural logarithms)
OAI.TreeEdit.binary_torus@ComparatorChallenges/TreeEdit.lean Challenge statement: Tree-based binary edit-distance distortion lower bound
OAI.TriangleFace198.triangle_expansion_face@ComparatorChallenges/TriangleFace.lean Challenge statement: Face correspondence under triangle expansion
OAI.SharpTerminalLeave.sharp_terminal_leave@ComparatorChallenges/TriangleRemoval.lean Challenge statement: The sharp terminal leave in random triangle removal
OAI.TriangularCovering.main@ComparatorChallenges/TriangularCovering.lean Challenge statement: Explicit triangular-cylinder cover below half area
OAI.AtomicTriangular.latticeEnergy The full nonzero-lattice energy, allowing a divergent series
OAI.AtomicTriangular.universal_energy_minimum@ComparatorChallenges/TriangularEnergy.lean Challenge statement: Universal energy minimality of the triangular lattice
OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction@ComparatorChallenges/TriangularGaussian.lean Challenge statement: Gaussian Fourier minorants with their construction
OAI.TriangularHilbert.main_estimate@ComparatorChallenges/TriangularHilbert.lean Challenge statement: Annular variation and dyadic absolute bounds for the triangular Hilbert transform
OAI.TruffetV4Counterexample.finite_execution_not_optimal@ComparatorChallenges/TruffetCounterexample.lean Challenge statement: Finite counterexample to Truffet's optimization procedure
OAI.TwoWayComplementation.relStar Reflexive transitive closure, including the empty path
OAI.TwoWayComplementation.TwoNFA A read-only 2NFA
OAI.TwoWayComplementation.tapeSymbol Tape lookup includes two distinct endmarkers, even on empty input
OAI.TwoWayComplementation.TwoNFA.step One legal step: both head positions stay within the marked input
OAI.TwoWayComplementation.TwoNFA.language Existential finite-run acceptance, allowing a run of length zero
OAI.TwoWayComplementation.complementation_lower_bound_finite@ComparatorChallenges/TwoWayComplementation.lean Challenge statement: Two-way nondeterministic complementation lower bound
OAI.TwoWayComplementation.TwoNFA.Deterministic At most one next-state/move pair at every state and scanned symbol
OAI.TwoWayComplementation.relationProduct Relation product for an input word; the empty product is the identity
OAI.TwoWayComplementation.sourceLanguage The source language consists of the words with nonempty relation product
OAI.TwoWayComplementation.explicit_family_main@ComparatorChallenges/TwoWayDeterminization.lean Challenge statement: Same-family determinization lower bound
OAI.PureTypeSystem.StronglyNormalizing Accessibility for the converse of reduction: strong normalization, including reductions in all type annotations
OAI.PureTypeSystem.weak_implies_strong@ComparatorChallenges/TypeSystemNormalization.lean Challenge statement: Weak normalization implies strong normalization in pure type systems
OAI.Kadison.uniform_commutator@ComparatorChallenges/UniformCommutator.lean Challenge statement: Uniform amplified commutator estimate
OAI.PowerSaving.Tape Register arrays
OAI.PowerSaving.Tape.tab Materialized array
OAI.PowerSaving.Tape.look Read with fixed out of bounds default
OAI.PowerSaving.Tape.set Semantics of a write into fresh storage; out-of-range writes are ignored
OAI.PowerSaving.RAM.Bill One basic work unit below pays for O(1) primitive RAM operations; includes loop and stack overhead
OAI.PowerSaving.RAM.Bill.pay Charge some work and optionally a new word bound
OAI.PowerSaving.RAM.Bill.pass Both computations are evaluated
OAI.PowerSaving.RAM.Bill.steps Execute f 0 through f (n-1), iterating an accumulator
OAI.PowerSaving.RAM.Bill.sow Build Tape len by count writes (initialized with a blank z)
OAI.PowerSaving.RAM.Bill.tab Build Tape len
OAI.PowerSaving.RAM.Code call is internal for bounded recursion; a program has Port = none
OAI.PowerSaving.transform_main@ComparatorChallenges/UniformFourier.lean Challenge statement: Uniform exact DFT and convolution with a power saving
OAI.PowerSaving.convolution_main@ComparatorChallenges/UniformFourier.lean Challenge statement: Uniform exact DFT and convolution with a power saving
OAI.ComparatorModel.CurrentMain.main@ComparatorChallenges/UniformGamma.lean Challenge statement: Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability
OAI.UniformKServer.offlineCost All finite serving-label choices, knowing the entire request word
OAI.UniformKServer.BitMachine.install At a request boundary only the input/output interface is refreshed
OAI.UniformKServer.natCode Self-delimiting binary code: ℓ ones, a zero, then ℓ low-to-high bits
OAI.UniformKServer.polynomialBudget A dominating polynomial; every fixed polynomial nonnegative on natural inputs is bounded by one of this form after increasing c and e
OAI.UniformKServer.Reachable Reachability includes every binary choice, not merely an almost-sure set
OAI.UniformKServer.selectedLabel Modulo makes the semantic recursion total even for unsuccessful machines
OAI.UniformKServer.UniformAlgorithmClaim Full uniform main objective in the explicit bit model, not a theorem or assumption
OAI.UniformKServer.uniform_squared_logarithmic_main@ComparatorChallenges/UniformKServer.lean Challenge statement: Uniform bit algorithm for the squared-logarithmic $k$-server bound
OAI.UniformSparsestCut.mainGap@ComparatorChallenges/UniformSparsestCut.lean Challenge statement: Uniform sparsest cut: hardness and semidefinite gaps
OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable A finite permutation table with a certified inverse
OAI.UniqueGamesTheorem.Foundations.Target.Constraint One oriented permutation constraint
OAI.UniqueGamesTheorem.Foundations.Target.Constraint.satisfied Test whether one labeling satisfies one constraint
OAI.UniqueGamesTheorem.Foundations.Target.Instance An explicit, unweighted list of Unique Games constraints
OAI.UniqueGamesTheorem.Foundations.Target.countSatisfied Count satisfied constraint occurrences
OAI.UniqueGamesTheorem.BinaryFormula.Literal A signed Boolean variable occurrence
OAI.UniqueGamesTheorem.BinaryFormula.Literal.eval Evaluate a signed literal under a Boolean assignment
OAI.UniqueGamesTheorem.BinaryFormula.Clause Exactly three literal slots
OAI.UniqueGamesTheorem.BinaryFormula.Clause.eval Evaluate a 3SAT clause by disjunction
OAI.UniqueGamesTheorem.BinaryFormula.Formula Binary 3SAT as a finite list of three-literal clauses
OAI.UniqueGamesTheorem.BinaryFormula.Formula.Satisfiable One assignment satisfies every listed clause
OAI.UniqueGamesTheorem.BinaryEncoding.bitsValue Interpret a least-significant-bit-first Boolean list
OAI.UniqueGamesTheorem.BinaryEncoding.parseFrame Parse one self-delimiting frame of bits
OAI.UniqueGamesTheorem.BinaryEncoding.parseName Decode one canonically framed natural-number name
OAI.UniqueGamesTheorem.BinaryEncoding.parseLiteral Parse a sign bit followed by one canonical name
OAI.UniqueGamesTheorem.BinaryEncoding.parseClause Parse three literals in sequence
OAI.UniqueGamesTheorem.BinaryEncoding.parseClauses Decode a terminated clause list with structural fuel
OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula Accept exactly one complete canonical formula encoding
OAI.UniqueGamesTheorem.BinaryLanguage.language The encoded language of satisfiable binary 3SAT formulas
OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2 The two-element coefficient field
OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector A finite binary coordinate vector
OAI.UniqueGamesTheorem.Integration.TranslationTarget.IsTranslationInstance Every permutation constraint is addition by one binary shift
OAI.UniqueGamesTheorem.Foundations.Complexity.tableWords Serialize the forward half of a permutation table
OAI.UniqueGamesTheorem.Foundations.Complexity.constraintWords Serialize one constraint as endpoints plus a permutation table
OAI.UniqueGamesTheorem.Foundations.Complexity.gameWords Flatten an explicit game into natural-number fields
OAI.UniqueGamesTheorem.Foundations.Complexity.gameBits The comparator's concrete output bit string
OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite A certificate that the output graph is simple and bipartite
OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction The complete machine-checkable contract for the gap reduction
OAI.UniqueGamesTheorem.theorem11@ComparatorChallenges/UniqueGamesTheorem.lean Challenge statement: A polynomial-time binary-3SAT reduction proving the Unique Games gap
OAI.UniversalFInfinity.universal_group_of_type_FInfinity@ComparatorChallenges/UniversalFInfinity.lean Challenge statement: Universal group of type $F_\infty$
OAI.UniversalTensorSquares.universal_tensor_square@ComparatorChallenges/UniversalTensorSquares.lean Challenge statement: Universal irreducible tensor squares for symmetric groups
OAI.VariableWL.main@ComparatorChallenges/VariableWL.lean Challenge statement: EXPTIME-completeness of variable-dimension Weisfeiler–Leman equivalence
OAI.DirectionalTransience.positive_probability_transience_velocity_hemisphere@ComparatorChallenges/VelocityHemisphere.lean Challenge statement: Positive-probability transience and the velocity hemisphere
OAI.MinimalVertex.main@ComparatorChallenges/VertexAlgebraNet.lean Challenge statement: Unitary vertex operator algebras and conformal nets
OAI.VertexCover.explicit_cover_gap@ComparatorChallenges/VertexCover.lean Challenge statement: Vertex Cover gap and factor-two hardness
OAI.VertexCover.every_fixed_factor_below_two@ComparatorChallenges/VertexCover.lean Challenge statement: Vertex Cover gap and factor-two hardness
OAI.RVM.global_classical_solution@ComparatorChallenges/VlasovMaxwell.lean Challenge statement: Global smoothness for relativistic Vlasov–Maxwell
OAI.WLIdentification.NeighborColor Colors retain their full history, and hence are shared between graphs
OAI.WLIdentification.tupleColor Joint update: one multiset of whole replacement vectors, not independent marginals
OAI.WLIdentification.Identifies There is no restriction to mates from a graph construction or to a selected order
OAI.WLIdentification.WLdim The infimum of the positive identifying dimensions; this set is nonempty for finite G
OAI.WLIdentification.inputWord Unary order header, row-major binary matrix, then most-significant-first binary k
OAI.WLIdentification.dimensionLanguage A malformed word is rejected: membership requires a valid nonempty simple matrix and k>0
OAI.WLIdentification.step One read/write/head-movement transition
OAI.WLIdentification.Output Output is the binary word beginning at origin and ending at its first blank
OAI.WLIdentification.DecidesWithin Uniform genuine executions on every bit word, including malformed graph words
OAI.WLIdentification.main@ComparatorChallenges/WLIdentification.lean Challenge statement: EXPTIME-completeness of Weisfeiler–Leman graph identification
OAI.WeakHessian.IsGeodesic The constant-speed minimizing parametrization, including constant curves
OAI.WeakHessian.metricSpeed Metric speed
OAI.WeakHessian.IsAC2 Absolute continuity with a square-integrable metric control
OAI.WeakHessian.IsTestPlan A 2-test plan: bounded compression and finite average kinetic energy
OAI.WeakHessian.BoundedTracks Uniform bounded spatial support; used only to define the local Sobolev class
OAI.WeakHessian.IsLocalWeakUpperGradient Local weak upper gradients, in the integrated test-plan definition
OAI.WeakHessian.weakGradient A representative of the minimal weak upper gradient (zero off its domain)
OAI.WeakHessian.gamma Polarization of the minimal weak gradient on an infinitesimally Hilbertian space
OAI.WeakHessian.IsLaplacian Weak nonpositive generator convention, without a global L² assumption on F
OAI.WeakHessian.IsTestFunction Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian
OAI.WeakHessian.weakHessian The weak Hessian, with ∇_(∇g)∇g = ∇(Γ(g)/2)
OAI.WeakHessian.localSlope Asymptotic Lipschitz slope; zero at an isolated point
OAI.WeakHessian.cheegerEnergy Cheeger energy is the L² relaxation of one half the squared local slope
OAI.WeakHessian.sigmaCoeff The unreduced Lott–Sturm–Villani distortion coefficient σ
OAI.WeakHessian.tauCoeff The τ coefficient (not the reduced σ coefficient) in CD(K,N)
OAI.WeakHessian.renyiIntegral The positive of minus the N-Rényi entropy; singular mass contributes zero
OAI.WeakHessian.CurvatureDimension Unreduced CD(K,N), written with the standard dynamical optimal-plan formula
OAI.WeakHessian.CurveSecondDerivativeBound The literal second-distributional-derivative conclusion on (0,1)
OAI.WeakHessian.every_geodesic@ComparatorChallenges/WeakHessian.lean Challenge statement: Gigli’s characterization of Alexandrov curvature
OAI.WeakMTWGlobalSupport.current_main_convexity@ComparatorChallenges/WeakMTWGlobalSupport.lean Challenge statement: Convex injectivity domains under weak MTW
OAI.CubeShuffle.WeightedSweep.weighted_sweep_moments@ComparatorChallenges/WeightedSweepMoments.lean Challenge statement: Weighted Schatten moments and operator contraction for coordinate sweeps
OAI.WLTime.unconditional_time_lower_bound@ComparatorChallenges/WeisfeilerLeman.lean Challenge statement: Unconditional sequential time lower bounds for Weisfeiler–Leman equivalence
OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample@ComparatorChallenges/YauCounterexample.lean Challenge statement: A fixed smooth metric with unbounded normalized nodal four-volume
OAI.SeymourSecondNeighborhood.Extremal.no_strictSubsetGrowth_of_pruning Pruning contradicts the existence of a positive-indegree strict-growth graph
OAI.SeymourSecondNeighborhood.exists_goodVertex@OAI/Combinatorics/SecondNeighborhood/Main.lean Proof-bearing solution of Seymour's second-neighborhood conjecture
OAI.SeymourSecondNeighborhood.exists_minimal_counterexample Select a smallest counterexample and then minimize its arcs
OAI.SeymourSecondNeighborhood.Pruning.pruning Prune two pair families to compatibility with a controlled deletion cost
OAI.SeymourSecondNeighborhood.counterexample_reduction Reduce any counterexample to a positive-indegree strict-growth graph
OAI.SeymourSecondNeighborhood.Counterexample Every vertex has a strict first-neighborhood surplus
OAI.SeymourSecondNeighborhood.PositiveIndegree Every vertex has an incoming neighbor
OAI.SeymourSecondNeighborhood.StrictSubsetGrowth Every nonempty proper subset has a strict one-step image surplus
OAI.SeymourSecondNeighborhood.subsetDeficit_of_minimal Minimal counterexamples satisfy the strengthened subset deficit
OAI.SeymourSecondNeighborhood.blowup_strictSubsetGrowth A large transitive-tournament blowup amplifies subset deficit into strict growth