# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json # Catalog of papers with a formalized main result. Paths are relative to lean/. version: "v0.4" project: name: "OpenAI math repository" description: "Lean formalizations accompanying a mathematics manuscript collection." authors: ["OpenAI"] license: "Apache-2.0" sources: - title: "$L_1$ Embeddings of Graphs of Bounded Treewidth" authors: ["OpenAI"] id: ../preprints/L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026/paper.pdf type: article - title: "A CH obstruction to a prescribed categoricity threshold" authors: ["OpenAI"] id: ../preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf type: article - title: "A classification of finite Euclidean Ramsey configurations" authors: ["OpenAI"] id: ../preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026/paper.pdf type: article - title: "A continuum temperature singularity for a radial pair potential" authors: ["OpenAI"] id: ../preprints/A-continuum-temperature-singularity-for-a-radial-pair-potential-September-24-2026/paper.pdf type: article - title: "A counterexample to integer-degree harmonic dimension comparison" authors: ["OpenAI"] id: ../preprints/A-counterexample-to-integer-degree-harmonic-dimension-comparison-September-25-2026/paper.pdf type: article - title: "A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two" authors: ["OpenAI"] id: ../preprints/A-Counterexample-to-Kaplanskys-Direct-Finiteness-Conjecture-in-Characteristic-Two-September-23-2026/paper.pdf type: article - title: "A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd Characteristic" authors: ["OpenAI"] id: ../preprints/A-Counterexample-to-Kaplanskys-Direct-Finiteness-Conjecture-in-Odd-Characteristic-September-26-2026/paper.pdf type: article - title: "A counterexample to Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness" authors: ["OpenAI"] id: ../preprints/A-counterexample-to-Kaplanskys-quasitrace-conjecture-September-23-2026/paper.pdf type: article - title: "A counterexample to Ryser's covering conjecture" authors: ["OpenAI"] id: ../preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf type: article - title: "A counterexample to Tachikawa's second conjecture" authors: ["OpenAI"] id: ../preprints/A-counterexample-to-Tachikawas-second-conjecture-September-23-2026/paper.pdf type: article - title: "A Counterexample to the Group-Ring Determinant Conjecture" authors: ["OpenAI"] id: ../preprints/A-Counterexample-to-the-Group-Ring-Determinant-Conjecture-September-23-2026/paper.pdf type: article - title: "A Counterexample to the Infinite Matroid Packing/Covering Conjecture" authors: ["OpenAI"] id: ../preprints/A-Counterexample-to-the-Infinite-Matroid-Packing-Covering-Conjecture-September-24-2026/paper.pdf type: article - title: "A Cyclic Polytabloid Proof of Saxl's Conjecture" authors: ["OpenAI"] id: ../preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf type: article - title: "A Direct Proof of Optimal Max-Cut Hardness" authors: ["OpenAI"] id: ../preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026/paper.pdf type: article - title: "A direct proof of the complete Crouzeix inequality" authors: ["OpenAI"] id: ../preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf type: article - title: "A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding" authors: ["OpenAI"] id: ../preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf type: article - title: "A Fock-space inequality and the Laughlin spectral gap" authors: ["OpenAI"] id: ../preprints/A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026/A-Fock-space-inequality-and-the-Laughlin-spectral-gap-September-24-2026.pdf type: article - title: "A hyperbolic group with no geometric CAT(0) action" authors: ["OpenAI"] id: ../preprints/A-hyperbolic-group-with-no-geometric-CAT0-action-September-25-2026/paper.pdf type: article - title: "A linear cycle-and-edge decomposition of every graph" authors: ["OpenAI"] id: ../preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf type: article - title: "A logarithmic independence bound for clique-free graphs" authors: ["OpenAI"] id: ../preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026/paper.pdf type: article - title: "A negatively pinched Kähler threefold without bounded holomorphic coordinates" authors: ["OpenAI"] id: ../preprints/A-negatively-pinched-Kahler-threefold-without-bounded-holomorphic-coordinates-September-25-2026/paper.pdf type: article - title: "A nine-dimensional counterexample to Borsuk's covering assertion" authors: ["OpenAI"] id: ../preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026/paper.pdf type: article - title: "A nonspectrahedral hyperbolicity cone" authors: ["OpenAI"] id: ../preprints/A-Nonspectrahedral-Hyperbolicity-Cone-September-24-2026/nonspectrahedral-hyperbolicity-cone.pdf type: article - title: "A Polynomial-Time 2-Approximation for Shortest Common Superstring" authors: ["OpenAI"] id: ../preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/paper.pdf type: article - title: "A positive solution to Tingley's problem" authors: ["OpenAI"] id: ../preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf type: article - title: "A product counterexample to the simplex maximum for projection-body volume" authors: ["OpenAI"] id: ../preprints/A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026/paper.pdf type: article - title: "A proof of Seymour’s second-neighborhood conjecture" authors: ["OpenAI"] id: ../preprints/A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026/paper.pdf type: article - title: "A quadratic bound for Jacobsthal's function" authors: ["OpenAI"] id: ../preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf type: article - title: "A radial continuum phase transition with algebraic decay" authors: ["OpenAI"] id: ../preprints/A-radial-continuum-phase-transition-with-algebraic-decay-September-24-2026/paper.pdf type: article - title: "A single-lattice covering bound of order n log n" authors: ["OpenAI"] id: ../preprints/A-single-lattice-covering-bound-of-order-n-log-n-September-23-2026/paper.pdf type: article - title: "A Smooth Metric with No Local Isometric Immersion into Three-Space" authors: ["OpenAI"] id: ../preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf type: article - title: "A strict inverse-first-power bound for univalent functions" authors: ["OpenAI"] id: ../preprints/A-strict-inverse-first-power-bound-for-univalent-functions-September-24-2026/paper.pdf type: article - title: "A superquadratic separation between sensitivity and block sensitivity" authors: ["OpenAI"] id: ../preprints/A-superquadratic-separation-between-sensitivity-and-block-sensitivity-September-25-2026/paper.pdf type: article - title: "A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric" authors: ["OpenAI"] id: ../preprints/A-Three-Manifold-Without-Conjugate-Points-and-Without-a-Nonpositively-Curved-Metric-September-24-2026/paper.pdf type: article - title: "A Torsion-Free Group Algebra with Zero Divisors" authors: ["OpenAI"] id: ../preprints/A-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026/paper.pdf type: article - title: "A torsion-free hyperbolic group that is not residually finite" authors: ["OpenAI"] id: ../preprints/a-torsion-free-hyperbolic-group-that-is-not-residually-finite-September-23-2026/paper.pdf type: article - title: "A translational tile with no fully periodic tiling in dimension three" authors: ["OpenAI"] id: ../preprints/A-translational-tile-with-no-fully-periodic-tiling-in-dimension-three-September-23-2026/paper.pdf type: article - title: "A universal group of type F∞" authors: ["OpenAI"] id: ../preprints/A-universal-group-of-type-F-infinity-September-23-2026/paper.pdf type: article - title: "Additive hardness and unbounded configuration gaps in bin packing" authors: ["OpenAI"] id: ../preprints/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026.pdf type: article - title: "Ample rank-two bundles on the quadric surface without Griffiths-positive metrics" authors: ["OpenAI"] id: ../preprints/ample-rank-two-bundles-on-the-quadric-surface-without-griffiths-positive-metrics-September-24-2026/paper.pdf type: article - title: "An algebra of infinite little finitistic dimension" authors: ["OpenAI"] id: ../preprints/An-algebra-of-infinite-little-finitistic-dimension-September-23-2026/paper.pdf type: article - title: "An Artin group with no geometric CAT(0) action" authors: ["OpenAI"] id: ../preprints/An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026/paper.pdf type: article - title: "An Endpoint Gradient Bound for the Centered Disk Maximal Operator" authors: ["OpenAI"] id: ../preprints/An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026/article.pdf type: article - title: "An explicit counterexample to the Auslander-Reiten conjecture" authors: ["OpenAI"] id: ../preprints/An-explicit-counterexample-to-the-Auslander-Reiten-conjecture-September-23-2026/paper.pdf type: article - title: "An explicit failure of complex affine-space cancellation" authors: ["OpenAI"] id: ../preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf type: article - title: "An explicit noncoordinate polynomial with affine three-space zero fibre" authors: ["OpenAI"] id: ../preprints/An-explicit-noncoordinate-polynomial-with-affine-three-space-zero-fibre-September-24-2026/paper.pdf type: article - title: "An exponential state lower bound for two-way nondeterministic complementation" authors: ["OpenAI"] id: ../preprints/An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026/paper.pdf type: article - title: "An exponential two-way deterministic state lower bound for one-way liveness" authors: ["OpenAI"] id: ../preprints/An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026/main.pdf type: article - title: "An infinite finitely presented simple amenable group" authors: ["OpenAI"] id: ../preprints/An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026/paper.pdf type: article - title: "An Upper Bound of 9/4 for the Matrix Multiplication Exponent" authors: ["OpenAI"] id: ../preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026/paper.pdf type: article - title: "Approximate counting of common bases of two matroids" authors: ["OpenAI"] id: ../preprints/Approximate-counting-of-common-bases-of-two-matroids-September-23-2026/main.pdf type: article - title: "Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space" authors: ["OpenAI"] id: ../preprints/Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026/manuscript.pdf type: article - title: "Asymptotically minimal maxima of real Littlewood polynomials" authors: ["OpenAI"] id: ../preprints/Asymptotically-minimal-maxima-of-real-Littlewood-polynomials-September-23-2026/paper.pdf type: article - title: "Average sensitivity of polynomial threshold functions" authors: ["OpenAI"] id: ../preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/main.pdf type: article - title: "Backward intertwiners and a transitive commutant" authors: ["OpenAI"] id: ../preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf type: article - title: "Beyond the Square-Root Exponent for Depth-Three Boolean Circuits" authors: ["OpenAI"] id: ../preprints/Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026/main.pdf type: article - title: "Bi-Lipschitz Absorption of $c_0$ Without a Linear Copy of $c_0$" authors: ["OpenAI"] id: ../preprints/Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026/paper.pdf type: article - title: "Bounded recovery for modular spectral averages" authors: ["OpenAI"] id: ../preprints/Bounded-recovery-for-modular-spectral-averages-September-23-2026/Bounded-recovery-for-modular-spectral-averages-September-23-2026.pdf type: article - title: "Bounded-Step Walks on Gaussian Primes" authors: ["OpenAI"] id: ../preprints/Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026/paper.pdf type: article - title: "Brennan's conjecture and sharp inverse-square integral means" authors: ["OpenAI"] id: ../preprints/Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026/paper.pdf type: article - title: "Choiceless polynomial time with counting does not capture polynomial time" authors: ["OpenAI"] id: ../preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf type: article - title: "Classical capacity and entropy inequalities for generalized amplitude damping" authors: ["OpenAI"] id: ../preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf type: article - title: "Compatibility entropy and the spectrum of a Thorp sweep" authors: ["OpenAI"] id: ../preprints/Compatibility-entropy-and-the-spectrum-of-a-Thorp-sweep-September-26-2026/paper.pdf type: article - title: "Complex Matrix Multiplication Below 2.258 and Rectangular Bounds" authors: ["OpenAI"] id: ../preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026.pdf type: article - title: "Conditional coordinate sweeps and analytic transfer" authors: ["OpenAI"] id: ../preprints/Conditional-coordinate-sweeps-and-analytic-transfer-September-26-2026/main.pdf type: article - title: "Counterexamples to the duality conjecture for metric entropy" authors: ["OpenAI"] id: ../preprints/Counterexamples-to-the-duality-conjecture-for-metric-entropy-September-24-2026/main.pdf type: article - title: "Critical bond and site percolation on the cubic lattice" authors: ["OpenAI"] id: ../preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026/paper.pdf type: article - title: "Critical slowing down in the Sherrington–Kirkpatrick model" authors: ["OpenAI"] id: ../preprints/Critical-slowing-down-in-the-Sherrington-Kirkpatrick-model-September-24-2026/paper.pdf type: article - title: "Directional transience implies ballisticity" authors: ["OpenAI"] id: ../preprints/Directional-transience-implies-ballisticity-September-23-2026/paper.pdf type: article - title: "Distortion of countably branching diamonds from midpoint and tree energies" authors: ["OpenAI"] id: ../preprints/Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026/manuscript.pdf type: article - title: "Entropy and Face Dimension of the Perfect-Matching Polytope" authors: ["OpenAI"] id: ../preprints/Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026/main.pdf type: article - title: "Exact asymptotic moduli in a Daugavet subspace of L1" authors: ["OpenAI"] id: ../preprints/Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026/manuscript.pdf type: article - title: "Exponential decay in two-dimensional classical O(n) models" authors: ["OpenAI"] id: ../preprints/Exponential-decay-in-two-dimensional-classical-On-models-September-23-2026/paper.pdf type: article - title: "Finite tensor savings and exact Fourier circuits" authors: ["OpenAI"] id: ../preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026/main.pdf type: article - title: "Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces" authors: ["OpenAI"] id: ../preprints/Fixed-Points-of-Nonexpansive-Maps-in-Reflexive-Banach-Spaces-September-24-2026/paper.pdf type: article - title: "Generalized ionization energies for full Coulomb atoms" authors: ["OpenAI"] id: ../preprints/Generalized-ionization-energies-for-full-Coulomb-atoms-September-24-2026/paper.pdf type: article - title: "Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system" authors: ["OpenAI"] id: ../preprints/Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026/paper.pdf type: article - title: "Global Support and Convex Injectivity Domains under Weak MTW" authors: ["OpenAI"] id: ../preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf type: article - title: "Hardness of finding large independent sets in three-colorable graphs" authors: ["OpenAI"] id: ../preprints/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026.pdf type: article - title: "Harmonic heights and the Artin K(π,1) conjecture" authors: ["OpenAI"] id: ../preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf type: article - title: "Independent products in real L1: asymptotic midpoint convexity without AUC renormings" authors: ["OpenAI"] id: ../preprints/Independent-products-in-real-L1-asymptotic-midpoint-convexity-without-AUC-renormings-September-27-2026/manuscript.pdf type: article - title: "Integral and fractional expectation thresholds are equivalent" authors: ["OpenAI"] id: ../preprints/Integral-and-fractional-expectation-thresholds-are-equivalent-September-23-2026/paper.pdf type: article - title: "Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic" authors: ["OpenAI"] id: ../preprints/Lipschitz-Equivalent-Separable-Banach-Spaces-Need-Not-Be-Linearly-Isomorphic-September-24-2026/paper.pdf type: article - title: "Maximal Seshadri constants on arbitrary polarized surfaces" authors: ["OpenAI"] id: ../preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf type: article - title: "Memory and precision in noiseless Gaussian regression" authors: ["OpenAI"] id: ../preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf type: article - title: "Midpoint convexity from bounded tree potentials and path costs" authors: ["OpenAI"] id: ../preprints/Midpoint-convexity-from-bounded-tree-potentials-and-path-costs-September-27-2026/manuscript.pdf type: article - title: "Midpoint convexity from two recursive potentials" authors: ["OpenAI"] id: ../preprints/Midpoint-convexity-from-two-recursive-potentials-September-27-2026/manuscript.pdf type: article - title: "Midpoint lenses in segment spaces" authors: ["OpenAI"] id: ../preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf type: article - title: "Nagata's conjecture for plane curves" authors: ["OpenAI"] id: ../preprints/Nagatas-Conjecture-for-Plane-Curves-September-23-2026/main.pdf type: article - title: "Near-square-root logarithmic integrality gaps for uniform sparsest cut" authors: ["OpenAI"] id: ../preprints/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026.pdf type: article - title: "Nontrivial Markov Type Forces Superreflexivity" authors: ["OpenAI"] id: ../preprints/Nontrivial-Markov-Type-Forces-Superreflexivity-September-23-2026/paper.pdf type: article - title: "Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions" authors: ["OpenAI"] id: ../preprints/Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026/paper.pdf type: article - title: "Perfect completeness for 2-to-1 games" authors: ["OpenAI"] id: ../preprints/Perfect-completeness-for-2-to-1-games-September-23-2026/paper.pdf type: article - title: "Petty’s projection-volume conjecture in dimensions at least four" authors: ["OpenAI"] id: ../preprints/Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026/paper.pdf type: article - title: "Planar Graph Metrics Embed into $L_1$ with Constant Distortion" authors: ["OpenAI"] id: ../preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf type: article - title: "Polynomial Hitting Lists for Noncommutative Rational Formulas" authors: ["OpenAI"] id: ../preprints/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026.pdf type: article - title: "Polynomial removal fails for ordered binary matrices" authors: ["OpenAI"] id: ../preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026/paper.pdf type: article - title: "Posterior replicas and conditional information in Gaussian regression" authors: ["OpenAI"] id: ../preprints/Posterior-replicas-and-conditional-information-in-Gaussian-regression-September-27-2026/paper.pdf type: article - title: "Power-law violations of Yau's nodal upper bound" authors: ["OpenAI"] id: ../preprints/Power-law-violations-of-Yaus-nodal-upper-bound-September-23-2026/paper.pdf type: article - title: "Product-projection localization and the QAC⁰ parity lower bound" authors: ["OpenAI"] id: ../preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf type: article - title: "Projection moments, positive cap domination, and Riesz estimates on the sphere" authors: ["OpenAI"] id: ../preprints/Projection-moments-positive-cap-domination-and-Riesz-estimates-on-the-sphere-September-27-2026/paper.pdf type: article - title: "Quadratic stabilization of the canonical Foulkes–Howe map" authors: ["OpenAI"] id: ../preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026/paper.pdf type: article - title: "Quantitative Superexponential Bounds for van der Waerden Numbers" authors: ["OpenAI"] id: ../preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf type: article - title: "Randomized quasipolynomial-time mean-payoff games" authors: ["OpenAI"] id: ../preprints/Randomized-quasipolynomial-time-mean-payoff-games-September-25-2026/paper.pdf type: article - title: "Regular trajectories, pruning and quantum parity" authors: ["OpenAI"] id: ../preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf type: article - title: "Relative generation and the generator problem for finite factors" authors: ["OpenAI"] id: ../preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf type: article - title: "Replacing Gaussian observations in memory-constrained inference" authors: ["OpenAI"] id: ../preprints/Replacing-Gaussian-observations-in-memory-constrained-inference-September-27-2026/paper.pdf type: article - title: "Riesz transforms and uniform rectifiability in higher codimension" authors: ["OpenAI"] id: ../preprints/Riesz-transforms-and-uniform-rectifiability-in-higher-codimension-September-24-2026/paper.pdf type: article - title: "Rigidity of the Turing degrees" authors: ["OpenAI"] id: ../preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf type: article - title: "Routing densities and representation contraction for Thorp sweeps" authors: ["OpenAI"] id: ../preprints/Routing-densities-and-representation-contraction-for-Thorp-sweeps-September-26-2026/paper.pdf type: article - title: "Sharp binary-information contraction on the discrete cube" authors: ["OpenAI"] id: ../preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf type: article - title: "Sharp one-dimensional Lieb–Thirring constants" authors: ["OpenAI"] id: ../preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf type: article - title: "Short Egyptian fractions" authors: ["OpenAI"] id: ../preprints/Short-Egyptian-fractions-September-25-2026/Short-Egyptian-fractions-September-25-2026.pdf type: article - title: "Single-exponential recovery and bounded-price strictness for metric k-median" authors: ["OpenAI"] id: ../preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf type: article - title: "Single-fold Diophantine representations" authors: ["OpenAI"] id: ../preprints/Single-fold-Diophantine-representations-September-24-2026/paper.pdf type: article - title: "Smooth counterexamples to Yau's nodal upper bound in dimensions three and four" authors: ["OpenAI"] id: ../preprints/Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026/paper.pdf type: article - title: "Squarefree values of quartics and power-free values of polynomials" authors: ["OpenAI"] id: ../preprints/Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026/manuscript.pdf type: article - title: "Staggered extraction for exact matrix multiplication over every field" authors: ["OpenAI"] id: ../preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026.pdf type: article - title: "Strict convexity and differentiability of the planar exponential first-passage limit shape" authors: ["OpenAI"] id: ../preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf type: article - title: "Subpolynomial dimension reduction in $L_p$" authors: ["OpenAI"] id: ../preprints/Subpolynomial-dimension-reduction-in-Lp-September-23-2026/paper.pdf type: article - title: "Subpolynomial query complexity for well-conditioned log-concave sampling" authors: ["OpenAI"] id: ../preprints/Subpolynomial-query-complexity-for-well-conditioned-log-concave-sampling-September-26-2026/article.pdf type: article - title: "Subsphere methods for memory–sample lower bounds in noiseless Gaussian regression" authors: ["OpenAI"] id: ../preprints/Subsphere-methods-for-memory-sample-lower-bounds-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf type: article - title: "Symmetry of semialgebraic bounded domains with compact quotient" authors: ["OpenAI"] id: ../preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf type: article - title: "Symplectic Balls in Symmetric Polar Products" authors: ["OpenAI"] id: ../preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026/paper.pdf type: article - title: "Talagrand's discrete-convexity conjecture" authors: ["OpenAI"] id: ../preprints/Talagrands-discrete-convexity-conjecture-September-23-2026/paper.pdf type: article - title: "Taming implies compatibility on four-manifolds" authors: ["OpenAI"] id: ../preprints/Taming-implies-compatibility-on-four-manifolds-September-23-2026/paper.pdf type: article - title: "The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture" authors: ["OpenAI"] id: ../preprints/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026/The-Bass-trace-conjecture-for-complex-group-rings-September-24-2026.pdf type: article - title: "The circulant Hadamard conjecture" authors: ["OpenAI"] id: ../preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf type: article - title: "The complete Crouzeix theorem: optimal similarity and a common positive boundary representation" authors: ["OpenAI"] id: ../preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf type: article - title: "The cotype–cotype conjecture under the approximation property" authors: ["OpenAI"] id: ../preprints/The-cotype-cotype-conjecture-under-the-approximation-property-September-23-2026/paper.pdf type: article - title: "The crossing number of complete bipartite graphs" authors: ["OpenAI"] id: ../preprints/The-crossing-number-of-complete-bipartite-graphs-September-23-2026/paper.pdf type: article - title: "The crossing number of complete graphs" authors: ["OpenAI"] id: ../preprints/The-crossing-number-of-complete-graphs-September-23-2026/paper.pdf type: article - title: "The Deligne-Drinfeld conjecture" authors: ["OpenAI"] id: ../preprints/The-Deligne-Drinfeld-conjecture-September-23-2026/paper.pdf type: article - title: "The entropy-rate dimension formula for self-similar measures on the line" authors: ["OpenAI"] id: ../preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf type: article - title: "The Euclidean plane is not five-colorable" authors: ["OpenAI"] id: ../preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf type: article - title: "The Euclidean Steinitz–Bergström theorem" authors: ["OpenAI"] id: ../preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf type: article - title: "The Factor-Two Hardness Threshold for Vertex Cover" authors: ["OpenAI"] id: ../preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026/paper.pdf type: article - title: "The Falconer distance conjecture in all dimensions" authors: ["OpenAI"] id: ../preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf type: article - title: "The Gaussian propeller bound in every dimension" authors: ["OpenAI"] id: ../preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf type: article - title: "The Grothendieck homotopy hypothesis via elementary expansions" authors: ["OpenAI"] id: ../preprints/The-Grothendieck-homotopy-hypothesis-via-elementary-expansions-September-24-2026/paper.pdf type: article - title: "The Kirchberg–Rørdam character criterion" authors: ["OpenAI"] id: ../preprints/The-Kirchberg-Rordam-character-criterion-September-25-2026/paper.pdf type: article - title: "The logarithmic Brunn–Minkowski conjecture" authors: ["OpenAI"] id: ../preprints/The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026/paper.pdf type: article - title: "The maximal triangular Hilbert transform at the symmetric point" authors: ["OpenAI"] id: ../preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf type: article - title: "The Partition Principle does not imply Choice" authors: ["OpenAI"] id: ../preprints/The-Partition-Principle-does-not-imply-Choice-September-24-2026/partition-principle-without-choice.pdf type: article - title: "The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8" authors: ["OpenAI"] id: ../preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf type: article - title: "The second Kahn–Kalai conjecture" authors: ["OpenAI"] id: ../preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf type: article - title: "The sharp factor-of-IID threshold for the free Ising model on regular trees" authors: ["OpenAI"] id: ../preprints/The-sharp-factor-of-IID-threshold-for-the-free-Ising-model-on-regular-trees-September-26-2026/article.pdf type: article - title: "The strong thin tree conjecture" authors: ["OpenAI"] id: ../preprints/The-strong-thin-tree-conjecture-September-23-2026/paper.pdf type: article - title: "The Subcritical Hénon–Lane–Emden Conjecture" authors: ["OpenAI"] id: ../preprints/The-Subcritical-Henon-Lane-Emden-Conjecture-September-24-2026/paper.pdf type: article - title: "The symmetric Mahler conjecture and its equality cases" authors: ["OpenAI"] id: ../preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf type: article - title: "The Unique Games Theorem" authors: ["OpenAI"] id: ../preprints/The-Unique-Games-Theorem-September-23-2026/paper.pdf type: article - title: "The weak pinned planar distance theorem" authors: ["OpenAI"] id: ../preprints/The-weak-pinned-planar-distance-theorem-September-23-2026/paper.pdf type: article - title: "Thompson's group F is nonamenable" authors: ["OpenAI"] id: ../preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf type: article - title: "Three fixed points on the symplectic quadric threefold" authors: ["OpenAI"] id: ../preprints/A-degenerate-counterexample-to-the-critical-number-Arnold-bound-September-23-2026/paper.pdf type: article - title: "Threshold parallel repetition for finite-dimensional entangled games" authors: ["OpenAI"] id: ../preprints/Threshold-parallel-repetition-for-finite-dimensional-entangled-games-September-25-2026/paper.pdf type: article - title: "Tracial projection methods and uniform property Γ" authors: ["OpenAI"] id: ../preprints/Tracial-projection-methods-and-uniform-property-Gamma-September-23-2026/paper.pdf type: article - title: "Two limit cycles for quintic Liénard systems" authors: ["OpenAI"] id: ../preprints/two-limit-cycles-for-quintic-lienard-systems-September-24-2026/two-limit-cycles-for-quintic-lienard-systems-September-24-2026.pdf type: article - title: "Uniform Bi-Hölder Transport from Weak MTW" authors: ["OpenAI"] id: ../preprints/Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026/paper.pdf type: article - title: "Uniform exclusion of Landau–Siegel zeros" authors: ["OpenAI"] id: ../preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026/paper.pdf type: article - title: "Unitarizability implies amenability for discrete groups" authors: ["OpenAI"] id: ../preprints/Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026/paper.pdf type: article - title: "Universal-cover splitting for compact Kähler manifolds" authors: ["OpenAI"] id: ../preprints/Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026/paper.pdf type: article - title: "Weak Hessian bounds along every geodesic in RCD spaces" authors: ["OpenAI"] id: ../preprints/Weak-Hessian-bounds-along-every-geodesic-in-RCD-spaces-September-24-2026/weak-hessian-geodesics.pdf type: article related_formalizations: # Imported libraries, ordered by direct import count in project Lean sources. - id: https://github.com/leanprover-community/mathlib4 relationship: builds-on - id: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd relationship: builds-on - id: https://github.com/n-yamaguchi-0729/ClassFieldTheory relationship: builds-on - id: https://github.com/CBirkbeck/AINTLIB relationship: builds-on - id: https://github.com/math-inc/strongpnt relationship: builds-on - id: https://github.com/abenenson/rellich-kondrachov relationship: builds-on - id: https://github.com/harfe/fixed-point-theorems-lean4 relationship: builds-on - id: https://github.com/TauCetiProject/TauCeti relationship: builds-on - id: https://github.com/fpvandoorn/carleson relationship: builds-on - id: https://github.com/lana-agents/heights relationship: builds-on - id: https://github.com/Aaron1011/gromov relationship: builds-on - id: https://github.com/lana-agents/iut relationship: builds-on - id: https://github.com/alonamaloh/schoenflies-lean relationship: builds-on - id: https://github.com/leanprover-community/sphere-eversion relationship: builds-on - id: https://github.com/ahhwuhu/zeta_3_irrational relationship: builds-on - id: https://github.com/BennyAvelin/AbsorptionCutoff relationship: builds-on - id: https://github.com/lana-agents/belyi relationship: builds-on - id: https://github.com/PatrickMassot/checkdecls relationship: builds-on - id: https://github.com/leanprover/doc-gen4 relationship: builds-on - id: https://github.com/lana-agents/elliptic-curves relationship: builds-on - id: https://github.com/lana-agents/formal-schemes relationship: builds-on - id: https://github.com/lana-agents/genl relationship: builds-on - id: https://github.com/hanwenzhu/LeanArchitect relationship: builds-on - id: https://github.com/alerad/leancert relationship: builds-on - id: https://github.com/lana-agents/oka relationship: builds-on - id: https://github.com/lana-agents/orbicurve-cores relationship: builds-on - id: https://github.com/lana-agents/pi1 relationship: builds-on - id: https://github.com/b-mehta/PrimeCert relationship: builds-on - id: https://github.com/lana-agents/tate-curves-theta relationship: builds-on - id: https://github.com/lana-agents/tempered-fundamental-groups relationship: builds-on status: scope: "Partial progress." # Entries use source-qualified declaration names and the files containing them. main_results: - comparator_config: ComparatorChallenges/AbhyankarSathaye.json declaration: OAI.AbhyankarSathaye.exists_noncoordinate_polynomial file: OAI/AlgebraicGeometry/AbhyankarSathaye/Counterexample.lean - comparator_config: ComparatorChallenges/AmplitudeDamping.json declaration: OAI.GAD.main file: OAI/InformationTheory/AmplitudeDamping/Main.lean - comparator_config: ComparatorChallenges/ArnoldCounterexample.json declaration: OAI.ArnoldCounterexample.main file: OAI/Geometry/Arnold/Main.lean - comparator_config: ComparatorChallenges/ArtinCAT0.json declaration: OAI.ArtinCAT0.main file: OAI/GroupTheory/ArtinCAT0/Main.lean - comparator_config: ComparatorChallenges/AsymptoticallyMinimalLittlewood.json declaration: OAI.AsymptoticallyMinimalLittlewood.main file: OAI/Analysis/Littlewood/Main.lean - comparator_config: ComparatorChallenges/AuslanderReiten.json declaration: OAI.ArExplicit.Statement.main file: OAI/Algebra/AuslanderReiten/All.lean - comparator_config: ComparatorChallenges/BackwardIntertwiners.json declaration: OAI.BackwardIntertwiners.direct_algebra_corollary file: OAI/Analysis/BackwardIntertwiners/AlgebraCorollary.lean - comparator_config: ComparatorChallenges/BassTrace.json declaration: OAI.BassTrace.RightProjective.bassTraceModules_vanishing_and_support file: OAI/RingTheory/BassTrace/Main.lean - comparator_config: ComparatorChallenges/BiholderTransport.json declaration: OAI.WeakMTWTransport.uniform_biHolder_transport file: OAI/Analysis/BiholderTransport/Main.lean - comparator_config: ComparatorChallenges/BinPackingGap.json declaration: OAI.BinPackingGap.main_results file: OAI/Computability/BinPacking/Main.lean - comparator_config: ComparatorChallenges/BinaryMatching.json declaration: OAI.BinaryMatching.deterministic_approximate_counting file: OAI/Computability/MatchingCount/BinarySolve.lean - comparator_config: ComparatorChallenges/BinarySweep.json declaration: OAI.binary_sweep_contraction_and_mixing file: OAI/Probability/BinarySweep/Main.lean - comparator_config: ComparatorChallenges/BipartiteCrossing.json declaration: OAI.Zarankiewicz.mainTarget_proof file: OAI/Combinatorics/Crossing/Main.lean - comparator_config: ComparatorChallenges/BorsukNine.json declaration: OAI.BorsukNine.main_theorem file: OAI/Geometry/Borsuk/Counterexample.lean - comparator_config: ComparatorChallenges/BoundedRecovery.json declaration: OAI.BoundedRecovery.bounded_recovery file: OAI/Analysis/ModularRecovery/Recovery.lean - comparator_config: ComparatorChallenges/BoundedTreePotentials.json declaration: OAI.BoundedTreePotentials.TreeCalculus.main_counterexample file: OAI/Analysis/TreePotential/Main.lean - comparator_config: ComparatorChallenges/BoundedTreewidthL1.json declaration: OAI.BoundedTreewidthL1.main_theorem file: OAI/Combinatorics/TreewidthL1/Main.lean - comparator_config: ComparatorChallenges/Brennan.json declaration: OAI.Brennan.main_theorem file: OAI/Analysis/IntegralMeans/Main.lean - comparator_config: ComparatorChallenges/BrennanSharp.json declaration: OAI.Brennan.Sharp.sharp_endpoints file: OAI/Analysis/IntegralMeans/SharpEndpoints.lean - comparator_config: ComparatorChallenges/C0Absorption.json declaration: OAI.C0Absorption.main_result file: OAI/Analysis/C0Absorption/Main.lean - comparator_config: ComparatorChallenges/CHObstruction.json declaration: OAI.CHObstruction.main file: OAI/ModelTheory/Categoricity/Main.lean - comparator_config: ComparatorChallenges/CharacterCriterion.json declaration: OAI.KirchbergRordam.character_criterion file: OAI/Analysis/CharacterCriterion/Main.lean - comparator_config: ComparatorChallenges/ChoicelessPolynomialTime.json declaration: OAI.CPTSeparation.main file: OAI/ModelTheory/Choiceless/Separation.lean - comparator_config: ComparatorChallenges/CirculantHadamard.json declaration: OAI.CirculantHadamard.exists_iff_order_one_or_four file: OAI/LinearAlgebra/CirculantHadamard/Main.lean - comparator_config: ComparatorChallenges/ClassicalON.json declaration: OAI.ClassicalON.main file: OAI/Probability/ClassicalON/Main.lean - comparator_config: ComparatorChallenges/CliqueFreeLog.json declaration: OAI.CliqueFreeLog.logarithmic_independence_bound file: OAI/Combinatorics/CliqueFree/Main.lean - comparator_config: ComparatorChallenges/CommonBasesFPRAS.json declaration: OAI.common_bases_fpras file: OAI/Combinatorics/MatroidCounting/CommonBases.lean - comparator_config: ComparatorChallenges/CommutingDerivations.json declaration: OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_with_ordinary_extras file: OAI/AlgebraicGeometry/CommutingDerivations/OrdinaryExtraMain.lean - comparator_config: ComparatorChallenges/CompactBanach.json declaration: OAI.CompactBanach.main file: OAI/Geometry/DoublingHilbert/CompactBanach.lean - comparator_config: ComparatorChallenges/CompleteCrossing.json declaration: OAI.Paper170.complete_graph_crossing_number file: OAI/Combinatorics/CompleteCrossing/Main.lean - comparator_config: ComparatorChallenges/CompleteCrouzeix.json declaration: OAI.CompleteCrouzeix.main file: OAI/Analysis/NumericalRange/Main.lean - comparator_config: ComparatorChallenges/ComplexCancellation.json declaration: OAI.ComplexCancellation.main file: OAI/Algebra/AffineCancellation/Main.lean - comparator_config: ComparatorChallenges/Conductivity.json declaration: OAI.ScalarConductivity.main_nonuniqueness file: OAI/Analysis/Conductivity/Main.lean - comparator_config: ComparatorChallenges/ConjugatePoints.json declaration: OAI.ThreeManifold.main_theorem file: OAI/Geometry/ConjugatePoints/ThreeManifold.lean - comparator_config: ComparatorChallenges/ContinuumTransition.json declaration: OAI.ContinuumTemperature.main_theorem file: OAI/Probability/ContinuumTransition/Main.lean - comparator_config: ComparatorChallenges/CoordinateSweeps.json declaration: OAI.CoordinateSweeps.conditional_main file: OAI/Probability/CoordinateSweeps/Main.lean - comparator_config: ComparatorChallenges/Cotype.json declaration: OAI.Cotype.mainTarget_proved file: OAI/Analysis/Cotype/Main.lean - comparator_config: ComparatorChallenges/CoulombIonization.json declaration: OAI.CoulombAtom.generalized_ionization file: OAI/Analysis/CoulombIonization/Main.lean - comparator_config: ComparatorChallenges/CourtadeKumar.json declaration: OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment file: OAI/InformationTheory/BooleanNoise/Main.lean - comparator_config: ComparatorChallenges/CriticalSK.json declaration: OAI.CriticalSK.covariance_and_linear_tests file: OAI/MathematicalPhysics/CriticalSK/Rayleigh.lean - comparator_config: ComparatorChallenges/CriticalSKMixing.json declaration: OAI.CriticalSK.critical_mixing_bounds file: OAI/MathematicalPhysics/CriticalMixing/Main.lean - comparator_config: ComparatorChallenges/CriticalZ3.json declaration: OAI.CriticalZ3.critical_no_infinite file: OAI/Probability/CriticalZ3/Main.lean - comparator_config: ComparatorChallenges/CycleDecomposition.json declaration: OAI.ErdosGallai.erdos_gallai file: OAI/Combinatorics/CycleDecomposition/Main.lean - comparator_config: ComparatorChallenges/DaugavetModuli.json declaration: OAI.ExactModuli.exact_example file: OAI/Analysis/Daugavet/Main.lean - comparator_config: ComparatorChallenges/DegreeRigidity.json declaration: OAI.TuringRigidity.ManuscriptMain.rigidity file: OAI/Computability/DegreeRigidity/Main.lean - comparator_config: ComparatorChallenges/DeligneDrinfeld.json declaration: OAI.DeligneDrinfeld.main file: OAI/Algebra/Drinfeld/Completion.lean - comparator_config: ComparatorChallenges/DepthThree.json declaration: OAI.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound file: OAI/Computability/DepthThree/Main.lean - comparator_config: ComparatorChallenges/DiamondDistortion.json declaration: OAI.DiamondDistortion.headline_all_pairs file: OAI/Analysis/DiamondDistortion/Descent.lean - comparator_config: ComparatorChallenges/DirectCrouzeix.json declaration: OAI.DirectCrouzeix.complete_crouzeix file: OAI/Analysis/DirectCrouzeix/CompleteBound.lean - comparator_config: ComparatorChallenges/DirectionalBallisticity.json declaration: OAI.DirectionalTransience.directional_transience_implies_ballisticity file: OAI/Probability/Ballisticity/Main.lean - comparator_config: ComparatorChallenges/DirichletSevenEighths.json declaration: OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re file: OAI/NumberTheory/DirichletL/Nonvanishing.lean - comparator_config: ComparatorChallenges/DixmierAllDiscrete.json declaration: OAI.Dixmier.current_main_theorem file: OAI/Analysis/Unitarizability/AllDiscrete.lean - comparator_config: ComparatorChallenges/DoublingHilbert.json declaration: OAI.DoublingHilbert.main file: OAI/Geometry/DoublingHilbert/Main.lean - comparator_config: ComparatorChallenges/EgyptianFractions.json declaration: OAI.Problem337.main_double_log_order file: OAI/NumberTheory/EgyptianFractions/Main.lean - comparator_config: ComparatorChallenges/EgyptianFractions.json declaration: OAI.Problem337.counting_double_log_order file: OAI/NumberTheory/EgyptianFractions/Main.lean - comparator_config: ComparatorChallenges/EgyptianFractions.json declaration: OAI.Problem337.prescribed_denominator_corollary file: OAI/NumberTheory/EgyptianFractions/Main.lean - comparator_config: ComparatorChallenges/EntangledGames.json declaration: OAI.ThresholdParallelRepetition.threshold_parallel_repetition file: OAI/Probability/EntangledGames/Main.lean - comparator_config: ComparatorChallenges/EuclideanFiveColor.json declaration: OAI.EuclideanFiveColor.no_proper_five_coloring file: OAI/Geometry/PlaneColoring/Five.lean - comparator_config: ComparatorChallenges/EuclideanRamsey.json declaration: OAI.EuclideanRamsey.classification file: OAI/Combinatorics/EuclideanRamsey/Main.lean - comparator_config: ComparatorChallenges/ExactFourier.json declaration: OAI.ExactFourier.main_theorem file: OAI/Computability/FourierCircuit/Main.lean - comparator_config: ComparatorChallenges/FactorGeneration.json declaration: OAI.Generator.single_generation_of_II1_separable_predual file: OAI/Analysis/FactorGeneration/Main.lean - comparator_config: ComparatorChallenges/FinitisticAsymmetry.json declaration: OAI.LittleFinitistic.extreme_left_right_asymmetry file: OAI/Algebra/FinitisticAsymmetry/Main.lean - comparator_config: ComparatorChallenges/ForestSpace.json declaration: OAI.ForestSpace.main_theorem file: OAI/Analysis/ForestSpace/Main.lean - comparator_config: ComparatorChallenges/FoulkesHowe.json declaration: OAI.Problem346.canonical_foulkes_howe_surjective file: OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean - comparator_config: ComparatorChallenges/FreeIsing.json declaration: OAI.Problem367.free_ising_factor_iff_threshold file: OAI/Probability/FreeIsing/Main.lean - comparator_config: ComparatorChallenges/GaussianMoat.json declaration: OAI.GaussianMoat.fullMain file: OAI/NumberTheory/GaussianMoat/Main.lean - comparator_config: ComparatorChallenges/GaussianPropeller.json declaration: OAI.GaussianPropeller.all_partitions file: OAI/Probability/GaussianPropeller/Main.lean - comparator_config: ComparatorChallenges/GaussianReplacement.json declaration: OAI.CurrentProjection.hybridBlockMain file: OAI/Probability/GaussianReplacement/Hybrid.lean - comparator_config: ComparatorChallenges/GaussianReplacement.json declaration: OAI.CurrentProjection.fiberBlockMain file: OAI/Probability/GaussianReplacement/FiberBlock.lean - comparator_config: ComparatorChallenges/GotsmanLinial.json declaration: OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement file: OAI/Combinatorics/GotsmanLinial/Main.lean - comparator_config: ComparatorChallenges/GrahamSpherical.json declaration: OAI.GrahamSpherical.full_main file: OAI/Combinatorics/SphericalRamsey/Main.lean - comparator_config: ComparatorChallenges/GrothendieckElementaryExpansion.json declaration: OAI.Grothendieck.elementary_expansion file: OAI/CategoryTheory/Globular/ElementaryExpansion.lean - comparator_config: ComparatorChallenges/GroupRingDeterminant.json declaration: OAI.GroupRingDeterminant.main file: OAI/Analysis/GroupDeterminants/Main.lean - comparator_config: ComparatorChallenges/HarmonicArtin.json declaration: OAI.HarmonicArtin.salvetti_cover_contractible file: OAI/Topology/ArtinGroups/Realizations/SalvettiCoverContractible.lean - comparator_config: ComparatorChallenges/HarmonicGrowth.json declaration: OAI.HarmonicCounterexample.main file: OAI/Geometry/HarmonicGrowth/Main.lean - comparator_config: ComparatorChallenges/HeckeSevenEighths.json declaration: OAI.SevenEighths.HeckeFamily.LFunction_ne_zero_of_seven_eighths_lt_re file: OAI/NumberTheory/DirichletL/Hecke/Nonvanishing.lean - comparator_config: ComparatorChallenges/HenonEmden.json declaration: OAI.HenonLaneEmden.main_nonexistence file: OAI/Analysis/HenonEmden/Main.lean - comparator_config: ComparatorChallenges/HyperbolicCones.json declaration: OAI.Paper256.main_result file: OAI/Analysis/HyperbolicCones/Main.lean - comparator_config: ComparatorChallenges/HyperbolicObstruction.json declaration: OAI.HyperbolicObstruction.main file: OAI/Geometry/HyperbolicGroups/Main.lean - comparator_config: ComparatorChallenges/IndependentProducts.json declaration: OAI.IndependentProducts.main_general file: OAI/Analysis/ProductSpaces/WeakNullity.lean - comparator_config: ComparatorChallenges/IndependentProducts.json declaration: OAI.IndependentProducts.main_exponential file: OAI/Analysis/ProductSpaces/Main.lean - comparator_config: ComparatorChallenges/IndependentSets.json declaration: OAI.LargeIndependentSets.mainTheoremReal file: OAI/Combinatorics/IndependentSets/Main.lean - comparator_config: ComparatorChallenges/InfiniteMatroid.json declaration: OAI.InfiniteMatroidCounterexample.main file: OAI/Combinatorics/InfiniteMatroid/Main.lean - comparator_config: ComparatorChallenges/IsometricImmersion.json declaration: OAI.SmoothLocal.Geometry.exists_local_metric_without_local_immersion file: OAI/Geometry/IsometricImmersion/Main.lean - comparator_config: ComparatorChallenges/Jacobsthal.json declaration: OAI.Erdos970.Erdos970Final.erdos_970_quadratic file: OAI/NumberTheory/Jacobsthal/Conclusions/QuadraticBound.lean - comparator_config: ComparatorChallenges/KMedianRecovery.json declaration: OAI.MetricKMedianRecovery.global_application file: OAI/Combinatorics/KMedianRecovery/Main.lean - comparator_config: ComparatorChallenges/KahlerSplitting.json declaration: OAI.UniversalCoverSplitting.main file: OAI/Geometry/KahlerSplitting/Main.lean - comparator_config: ComparatorChallenges/KaplanskyFinitelyPresented.json declaration: OAI.KaplanskyCounterexample.finitelyPresented_counterexample file: OAI/RingTheory/DirectFiniteness/FinitelyPresented.lean - comparator_config: ComparatorChallenges/KaplanskyQuasitrace.json declaration: OAI.Kaplansky.kaplansky_quasitrace_counterexample file: OAI/Analysis/Kaplansky/Main.lean - comparator_config: ComparatorChallenges/Laughlin.json declaration: OAI.Laughlin.mainTarget_proved file: OAI/Analysis/Laughlin/Main.lean - comparator_config: ComparatorChallenges/LiebThirring.json declaration: OAI.SharpLiebThirring.sharp_lieb_thirring file: OAI/Analysis/LiebThirring/Main.lean - comparator_config: ComparatorChallenges/LipschitzEquivalence.json declaration: OAI.LipschitzCounterexample.main file: OAI/Analysis/LipschitzEquivalence/Main.lean - comparator_config: ComparatorChallenges/LittleFinitistic.json declaration: OAI.LittleFinitistic.Main.exists_counterexample file: OAI/Algebra/Finitistic/Main.lean - comparator_config: ComparatorChallenges/LogBrunnMinkowski.json declaration: OAI.LogBrunnMinkowski.main file: OAI/Geometry/LogVolume/BrunnMinkowski.lean - comparator_config: ComparatorChallenges/LogConcaveQuery.json declaration: OAI.LogConcaveSampling.exact_source_main file: OAI/Probability/LogConcave/Main.lean - comparator_config: ComparatorChallenges/MahlerConjecture.json declaration: OAI.SymmetricMahler.symmetric_mahler file: OAI/Analysis/Mahler/MainTheorem.lean - comparator_config: ComparatorChallenges/MarkovType.json declaration: OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm file: OAI/Analysis/MarkovType/Main.lean - comparator_config: ComparatorChallenges/MatchingEntropy.json declaration: OAI.MatchingEntropy.entropy_main file: OAI/Combinatorics/PerfectMatching/Main.lean - comparator_config: ComparatorChallenges/MatrixFields.json declaration: OAI.MatrixAllFields.MatrixMultiplication.AllFieldMain.omega_lt_source_constant file: OAI/LinearAlgebra/MatrixFields/Conclusions/AllFieldsBound.lean - comparator_config: ComparatorChallenges/MatrixMultiplication.json declaration: OAI.MatrixMultiplication.complex_omega_le_nine_quarters file: OAI/LinearAlgebra/MatrixMultiplication/Main.lean - comparator_config: ComparatorChallenges/MatrixMultiplication.json declaration: OAI.MatrixMultiplication.complex_alpha_gt_93_div_200 file: OAI/LinearAlgebra/MatrixMultiplication/Main.lean - comparator_config: ComparatorChallenges/MatrixMultiplication.json declaration: OAI.MatrixMultiplication.complex_rectangular_omega_lt_523_div_250 file: OAI/LinearAlgebra/MatrixMultiplication/Main.lean - comparator_config: ComparatorChallenges/MatrixRemoval.json declaration: OAI.Problem348.no_polynomial_removal_bound file: OAI/Combinatorics/MatrixRemoval/Main.lean - comparator_config: ComparatorChallenges/MaximalSeshadriConstants.json declaration: OAI.MaximalSeshadri.Geometry.maximalSeshadriConstants file: OAI/AlgebraicGeometry/Seshadri/Main.lean - comparator_config: ComparatorChallenges/MemoryPrecision.json declaration: OAI.MemoryPrecision.main file: OAI/Probability/MemoryPrecision/Main.lean - comparator_config: ComparatorChallenges/MetricEntropyDuality.json declaration: OAI.MetricEntropyDuality.exists_entropy_duality_counterexample_with_covers file: OAI/Analysis/MetricEntropy/Main.lean - comparator_config: ComparatorChallenges/MidpointLenses.json declaration: OAI.SegmentLenses.midpoint_lens_main file: OAI/Analysis/SegmentLenses/Main.lean - comparator_config: ComparatorChallenges/Nagata.json declaration: OAI.Nagata.nagata_conjecture file: OAI/AlgebraicGeometry/PlaneCurves/Nagata.lean - comparator_config: ComparatorChallenges/OddKaplansky.json declaration: OAI.OddKaplansky.main_theorem file: OAI/Algebra/OddKaplansky/Main.lean - comparator_config: ComparatorChallenges/OneWayLiveness.json declaration: OAI.OneWayLiveness.main_theorem file: OAI/Combinatorics/Automata/Main.lean - comparator_config: ComparatorChallenges/OptimalMaxCut.json declaration: OAI.OptimalMaxCut.main file: OAI/Computability/MaxCut/Main.lean - comparator_config: ComparatorChallenges/PartitionPrinciple.json declaration: OAI.PartitionPilot.Forcing.TransitiveGround.exists_model_partitionPrinciple_without_choice file: OAI/SetTheory/PartitionPrinciple/Models/Separation.lean - comparator_config: ComparatorChallenges/PerfectCompleteness.json declaration: OAI.PerfectCompleteness.Theorem11.exists_reduction file: OAI/Computability/PerfectCompleteness/Theorem11.lean - comparator_config: ComparatorChallenges/PeriodicTilingThree.json declaration: OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality file: OAI/Geometry/PeriodicTiling/Counterexample.lean - comparator_config: ComparatorChallenges/PettyProjectionVolume.json declaration: OAI.PettyProjection.petty_projection_volume file: OAI/Geometry/ProjectionBodies/Main.lean - comparator_config: ComparatorChallenges/PinchedKahler.json declaration: OAI.PinchedHartogs.main_theorem file: OAI/Geometry/Kahler/Main.lean - comparator_config: ComparatorChallenges/PinnedDistances.json declaration: OAI.WeakPinned.main file: OAI/Geometry/PinnedDistances/Main.lean - comparator_config: ComparatorChallenges/PlanarFalconer.json declaration: OAI.PlanarFalconer.mainTarget_proved file: OAI/MeasureTheory/Falconer/Main.lean - comparator_config: ComparatorChallenges/PlanarFirstPassage.json declaration: OAI.PlanarFPP.manuscriptMain file: OAI/Probability/FirstPassage/BoundaryCurve.lean - comparator_config: ComparatorChallenges/PlanarL1.json declaration: OAI.PlanarL1.planar_graph_metrics_embed_L1 file: OAI/Combinatorics/PlanarL1/Embedding.lean - comparator_config: ComparatorChallenges/PlaneColoring.json declaration: OAI.Problem160.properColoring_seven file: OAI/Geometry/PlaneColoring/Seven.lean - comparator_config: ComparatorChallenges/PosteriorReplicas.json declaration: OAI.PosteriorReplicas.source_main file: OAI/Probability/PosteriorReplicas/Main.lean - comparator_config: ComparatorChallenges/PowerFreeValues.json declaration: OAI.QuarticPowerFree.allDegrees file: OAI/NumberTheory/PowerFree/Main.lean - comparator_config: ComparatorChallenges/ProjectionCounterexample.json declaration: OAI.ProjectionCounterexample.universal_simplex_upper_bound_false file: OAI/Geometry/ProjectionBody/Counterexample.lean - comparator_config: ComparatorChallenges/ProjectionMoments.json declaration: OAI.ProjectionMoments.main file: OAI/Probability/ProjectionMoments/Main.lean - comparator_config: ComparatorChallenges/ProjectionVolume.json declaration: OAI.Paper092.product_counterexample file: OAI/Geometry/ProjectionVolume/ProductCounterexample.lean - comparator_config: ComparatorChallenges/QACParity.json declaration: OAI.QAC.parity_lower_bound file: OAI/InformationTheory/QuantumCircuit/Parity.lean - comparator_config: ComparatorChallenges/QuadricBundles.json declaration: OAI.QuadricCounterexample.main_theorem file: OAI/Geometry/QuadricBundles/Main.lean - comparator_config: ComparatorChallenges/QuantitativeVanDerWaerden.json declaration: OAI.QuantitativeVanDerWaerden.uniform_lower_bound file: OAI/Combinatorics/ProgressionColoring/Main.lean - comparator_config: ComparatorChallenges/QuasiRiemannHypothesis.json declaration: OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re file: OAI/NumberTheory/DirichletL/Nonvanishing.lean - comparator_config: ComparatorChallenges/QuinticLienard.json declaration: OAI.QuinticLienard.main file: OAI/Analysis/LienardCycles/Main.lean - comparator_config: ComparatorChallenges/RadialTransition.json declaration: OAI.RadialTransition.main file: OAI/Probability/RadialTransition/Main.lean - comparator_config: ComparatorChallenges/RandomizedMeanPayoff.json declaration: OAI.randomized_quasipolynomial_mean_payoff file: OAI/Computability/RandomMean/Main.lean - comparator_config: ComparatorChallenges/RationalHitting.json declaration: OAI.RationalHitting.main file: OAI/Computability/RationalHitting/Main.lean - comparator_config: ComparatorChallenges/RecursivePotentials.json declaration: OAI.ComparatorModel.RecursivePotentials.main file: OAI/Analysis/RecursivePotentials/Challenge.lean - comparator_config: ComparatorChallenges/ReflexiveFixedPoints.json declaration: OAI.ReflexiveFixedPoints.exists_fixedPoint_of_canonicallyReflexive file: OAI/Analysis/Nonexpansive/Main.lean - comparator_config: ComparatorChallenges/RegularParity.json declaration: OAI.QAC.parity_lower_bound_polynomial_size file: OAI/InformationTheory/QuantumCircuit/Main.lean - comparator_config: ComparatorChallenges/RieszQuantitative.json declaration: OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability file: OAI/Analysis/RieszRectifiability/Uniformity/Rectifiability.lean - comparator_config: ComparatorChallenges/RyserCovering.json declaration: OAI.RyserCoveringCounterexample.exists_prime_eventually_counterexampleRank file: OAI/Combinatorics/Ryser/Construction/Main.lean - comparator_config: ComparatorChallenges/RyserOddExtensions.json declaration: OAI.RyserOdd.eventualOddFailures_and_infinite file: OAI/Combinatorics/Ryser/OddExtensions.lean - comparator_config: ComparatorChallenges/Saxl.json declaration: OAI.Saxl.saxl_conjecture file: OAI/RepresentationTheory/Saxl/Main.lean - comparator_config: ComparatorChallenges/SecondKahnKalai.json declaration: OAI.LeanBlast.SecondKahnKalai.secondKahnKalaiBounds file: OAI/Combinatorics/GraphThreshold/Main.lean - comparator_config: ComparatorChallenges/SelfSimilar.json declaration: OAI.EntropyRateDimension.entropy_rate_dimension file: OAI/MeasureTheory/SelfSimilar/Main.lean - comparator_config: ComparatorChallenges/SensitivitySeparation.json declaration: OAI.Paper320.quantitative_separation file: OAI/Combinatorics/Sensitivity/Separation.lean - comparator_config: ComparatorChallenges/SeymourSecondNeighborhood.json declaration: OAI.SeymourSecondNeighborhood.exists_goodVertex file: OAI/Combinatorics/SecondNeighborhood/Main.lean - comparator_config: ComparatorChallenges/SiegelZeros.json declaration: OAI.SiegelZeros.WeightedTorusJets.exists_absolute_real_zero_gap file: OAI/NumberTheory/SiegelZeros/Conclusions/Theorem.lean - comparator_config: ComparatorChallenges/SignedFiniteBand.json declaration: OAI.SignedDisk.CenteredDiskEndpoint.main_signed_finite_band file: OAI/Analysis/SignedDisk/Main.lean - comparator_config: ComparatorChallenges/SimpleAmenable.json declaration: OAI.SimpleAmenable.main file: OAI/GroupTheory/SimpleAmenable/Main.lean - comparator_config: ComparatorChallenges/SingleFold.json declaration: OAI.SingleFold.main file: OAI/NumberTheory/SingleFold/Main.lean - comparator_config: ComparatorChallenges/SingleLatticeCovering.json declaration: OAI.SingleLatticeCovering.single_lattice_covering file: OAI/Geometry/LatticeCovering/Main.lean - comparator_config: ComparatorChallenges/SingletonLoopMatching.json declaration: OAI.LoopMatching.fullEndpoint file: OAI/Computability/LoopMatching/Main.lean - comparator_config: ComparatorChallenges/SmoothYau.json declaration: OAI.YauCounterexamples.sphere_three file: OAI/Geometry/SmoothYau/SphereMetric/ThreeSphere.lean - comparator_config: ComparatorChallenges/SmoothYau.json declaration: OAI.YauCounterexamples.sphere_two_torus_two file: OAI/Geometry/SmoothYau/ProductMetric/SphereProduct.lean - comparator_config: ComparatorChallenges/SteinitzBergstrom.json declaration: OAI.EuclideanSteinitzBergstrom.main file: OAI/Analysis/Steinitz/Main.lean - comparator_config: ComparatorChallenges/StrictMeans.json declaration: OAI.StrictInverseFirstPower.main file: OAI/Analysis/StrictMeans/Main.lean - comparator_config: ComparatorChallenges/StrongThinTree.json declaration: OAI.StrongThinTree.strongThinTree file: OAI/Combinatorics/ThinTrees/Main.lean - comparator_config: ComparatorChallenges/StructuralCrouzeix.json declaration: OAI.StructuralCrouzeixReference.challenge file: OAI/Analysis/StructuralCrouzeix/Endpoint.lean - comparator_config: ComparatorChallenges/SubpolynomialLp.json declaration: OAI.SubpolynomialLp.source_main file: OAI/Analysis/LpDimension/Main.lean - comparator_config: ComparatorChallenges/SubsphereCurrent.json declaration: OAI.SubsphereCurrent.full_current_main_scope file: OAI/Probability/Subsphere/Main.lean - comparator_config: ComparatorChallenges/Superstring.json declaration: OAI.Superstring.main file: OAI/Computability/Superstring/Main.lean - comparator_config: ComparatorChallenges/SymmetricDomains.json declaration: OAI.Release061.main file: OAI/Analysis/SymmetricDomains/Main.lean - comparator_config: ComparatorChallenges/SymmetricMahlerEquality.json declaration: OAI.SymmetricMahler.symmetric_mahler_equality file: OAI/Analysis/Mahler/Classification.lean - comparator_config: ComparatorChallenges/SymmetricPolar.json declaration: OAI.SymmetricPolar.symmetric_polar_main file: OAI/Geometry/PolarProducts/Main.lean - comparator_config: ComparatorChallenges/Tachikawa.json declaration: OAI.Tachikawa.main_theorem file: OAI/RingTheory/Tachikawa/Counterexample.lean - comparator_config: ComparatorChallenges/TalagrandDiscreteConvexity.json declaration: OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity file: OAI/Combinatorics/DiscreteConvexity/Main.lean - comparator_config: ComparatorChallenges/TalagrandExpectationThreshold.json declaration: OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence file: OAI/Combinatorics/ExpectationThreshold/Main.lean - comparator_config: ComparatorChallenges/TamingCompatibility.json declaration: OAI.TamingCompatibility.taming_implies_compatibility file: OAI/Geometry/TamingCompatibility/Main.lean - comparator_config: ComparatorChallenges/ThompsonNonamenability.json declaration: OAI.ThompsonNonamenability.thompson_F_nonamenable_composition file: OAI/GroupTheory/Thompson/Main.lean - comparator_config: ComparatorChallenges/ThorpRouting.json declaration: OAI.ThorpNine.main file: OAI/Probability/ThorpRouting/Main.lean - comparator_config: ComparatorChallenges/ThorpWeightedCompatibility.json declaration: OAI.ThorpCompatibility.weightedCompatibility_main file: OAI/Probability/ThorpCompatibility/Main.lean - comparator_config: ComparatorChallenges/TingleySphereIsometry.json declaration: OAI.Tingley.tingley_sphere_isometry_full file: OAI/Analysis/SphereIsometry/Extension.lean - comparator_config: ComparatorChallenges/TorsionFreeHyperbolic.json declaration: OAI.Release075.main file: OAI/GroupTheory/Hyperbolic/Main.lean - comparator_config: ComparatorChallenges/TorsionFreeZeroDivisors.json declaration: OAI.TorsionFreeZeroDivisors.main file: OAI/Algebra/GroupRing/Main.lean - comparator_config: ComparatorChallenges/TriangularHilbert.json declaration: OAI.TriangularHilbert.main_estimate file: OAI/Analysis/TriangularHilbert/Main.lean - comparator_config: ComparatorChallenges/TwoWayComplementation.json declaration: OAI.TwoWayComplementation.complementation_lower_bound_finite file: OAI/Combinatorics/TwoWayAutomata/Main.lean - comparator_config: ComparatorChallenges/TwoWayDeterminization.json declaration: OAI.TwoWayComplementation.explicit_family_main file: OAI/Combinatorics/TwoWayAutomata/ExplicitFamily.lean - comparator_config: ComparatorChallenges/UniformGamma.json declaration: OAI.ComparatorModel.CurrentMain.main file: OAI/Analysis/TracialSplitting/Challenge.lean - comparator_config: ComparatorChallenges/UniformSparsestCut.json declaration: OAI.UniformSparsestCut.mainGap file: OAI/Combinatorics/SparsestCut/Main.lean - comparator_config: ComparatorChallenges/UniqueGamesTheorem.json declaration: OAI.UniqueGamesTheorem.theorem11 file: OAI/Computability/UniqueGames/Theorem.lean - comparator_config: ComparatorChallenges/UniversalFInfinity.json declaration: OAI.UniversalFInfinity.universal_group_of_type_FInfinity file: OAI/GroupTheory/UniversalGroup/Main.lean - comparator_config: ComparatorChallenges/VertexCover.json declaration: OAI.VertexCover.every_fixed_factor_below_two file: OAI/Computability/VertexCover/Main.lean - comparator_config: ComparatorChallenges/VlasovMaxwell.json declaration: OAI.RVM.global_classical_solution file: OAI/Analysis/VlasovMaxwell/Main.lean - comparator_config: ComparatorChallenges/WeakHessian.json declaration: OAI.WeakHessian.every_geodesic file: OAI/Geometry/WeakHessian/Main.lean - comparator_config: ComparatorChallenges/WeakMTWGlobalSupport.json declaration: OAI.WeakMTWGlobalSupport.current_main_convexity file: OAI/Geometry/WeakMTW/Convexity.lean - comparator_config: ComparatorChallenges/YauCounterexample.json declaration: OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample file: OAI/Geometry/NodalSets/Main.lean automation: methods: - method: agent review: status: unchecked acknowledgements: >- Thank you very much to the authors of Lean 4, mathlib, and the other imported libraries listed above, as well as to the authors of Lake, Comparator, lean4export, and related tools.