formalization.yaml

# 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 Complete Local Domain without a Small Cohen–Macaulay Module"
    authors: ["OpenAI"]
    id: ../preprints/A-Complete-Local-Domain-Without-a-Small-Cohen-Macaulay-Module-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 Hadwiger's conjecture"
    authors: ["OpenAI"]
    id: ../preprints/A-counterexample-to-Hadwigers-conjecture-September-23-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 stable coordinate that is not a coordinate in four variables"
    authors: ["OpenAI"]
    id: ../preprints/A-stable-coordinate-that-is-not-a-coordinate-in-four-variables-October-5-2026/stable-coordinate-four-variables.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: "Almost-everywhere Fourier convergence in L log L"
    authors: ["OpenAI"]
    id: ../preprints/Almost-everywhere-Fourier-convergence-in-L-log-L-September-23-2026/paper.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 explicit power saving for the exact discrete Fourier transform"
    authors: ["OpenAI"]
    id: ../preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026/main.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 honeycomb chords with prescribed boundary endpoints"
    authors: ["OpenAI"]
    id: ../preprints/Critical-honeycomb-chords-with-prescribed-boundary-endpoints-September-26-2026/main.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: "Exact derandomization of logarithmic space: L = RL = BPL"
    authors: ["OpenAI"]
    id: ../preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.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: "Integral points on character varieties of curves"
    authors: ["OpenAI"]
    id: ../preprints/Integral-points-on-character-varieties-of-curves-September-25-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: "Local smoothing for the Euclidean wave equation"
    authors: ["OpenAI"]
    id: ../preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-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: "Simulating One-Tape Time in Two-Fifths-Power Space"
    authors: ["OpenAI"]
    id: ../preprints/Simulating-One-Tape-Time-in-Two-Fifths-Power-Space-September-25-2026/article.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 Exponential Time Hypothesis is False"
    authors: ["OpenAI"]
    id: ../preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.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 rational Hodge conjecture for CM abelian varieties"
    authors: ["OpenAI"]
    id: ../preprints/The-rational-Hodge-conjecture-for-CM-abelian-varieties-October-6-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 trace cone classifies Razak–Jacelon stabilizations"
    authors: ["OpenAI"]
    id: ../preprints/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026/The-trace-cone-classifies-Razak-Jacelon-stabilizations-September-25-2026.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 Cartier sections for Fano type contractions"
    authors: ["OpenAI"]
    id: ../preprints/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026.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/google-deepmind/formal-conjectures
    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/CartierChartCompactnessSupport.json
      declaration: OAI.CartierSections.isCompact_closedChartFieldRetraction_cone
      file: OAI/AlgebraicGeometry/CartierSections/ChartCompactness.lean

    - comparator_config: ComparatorChallenges/CharacterCriterion.json
      declaration: OAI.KirchbergRordam.character_criterion
      file: OAI/Analysis/CharacterCriterion/Main.lean

    - comparator_config: ComparatorChallenges/CharacterVarietiesAllSeamsSupport.json
      declaration: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.producedMarkedValues_allSeams
      file: OAI/AlgebraicGeometry/CharacterVarieties/Seams/ProducedSolution.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/FourierLLogL.json
      declaration: OAI.FourierLLogL.paperMain
      file: OAI/Analysis/FourierLLogL/PaperMain.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/HadwigerCounterexample.json
      declaration: OAI.HadwigerCounterexample.not_hadwiger_conjecture
      file: OAI/Combinatorics/HadwigerCounterexample/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/HodgeConjectureCMAbelianVarieties/main.json
      declaration: HodgeCM.hodge_conjecture_for_cm_abelian_varieties
      file: ComparatorChallenges/HodgeConjectureCMAbelianVarieties/Solution.lean

    - comparator_config: ComparatorChallenges/HoneycombBridgeMassSupport.json
      declaration: OAI.CriticalHoneycomb.finiteBridgeMassEstimate
      file: OAI/Combinatorics/HoneycombChords/BridgeMass.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/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.euclidean_local_smoothing
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean

    - comparator_config: ComparatorChallenges/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.bochner_riesz
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean

    - comparator_config: ComparatorChallenges/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.spherical_restriction
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean

    - comparator_config: ComparatorChallenges/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.kakeya_maximal
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean

    - comparator_config: ComparatorChallenges/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.kakeya
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean

    - comparator_config: ComparatorChallenges/LocalSmoothing.json
      declaration: OAI.Analysis.Fourier.LocalSmoothing.Comparator.stein_square
      file: OAI/Analysis/Fourier/LocalSmoothing/Comparator.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/LogspaceEquality.json
      declaration: OAI.ExactDerandomization.exact_logarithmic_space_derandomization
      file: OAI/Computability/Logspace/Equality.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/OneTapeSpace.json
      declaration: OAI.Fifths.Single.capped
      file: OAI/Computability/SpaceSimulation/Main.lean

    - comparator_config: ComparatorChallenges/OneTapeSpace.json
      declaration: OAI.Fifths.Single.unknown
      file: OAI/Computability/SpaceSimulation/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/StableCoordinateFour.json
      declaration: OAI.StableCoordinate.principal_package
      file: OAI/AlgebraicGeometry/StableCoordinate/Principal.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/SubexponentialSAT.json
      declaration: OAI.Algorithms.SubexponentialSAT.SqrtLogSpace.exact_count_and_sat
      file: OAI/Algorithms/SubexponentialSAT/SqrtLogSpace/Final.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/SurfaceConeCandidateSupport.json
      declaration: OAI.SmallCM.candidate_ring_properties
      file: OAI/AlgebraicGeometry/SurfaceCones/CandidateRing.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/TraceIdealTransportSupport.json
      declaration: OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_finIdeal
      file: OAI/Analysis/TraceCone/IdealTransport.lean

    - comparator_config: ComparatorChallenges/TraceIdealTransportSupport.json
      declaration: OAI.TraceConeClassification.TraceConeEquiv.idealOrderIso_zeroIdeal
      file: OAI/Analysis/TraceCone/IdealTransport.lean

    - comparator_config: ComparatorChallenges/TraceIdealTransportSupport.json
      declaration: OAI.TraceConeClassification.closed_ideal_weight_exists
      file: OAI/Analysis/TraceCone/FiniteIdeal.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/UniformFourier.json
      declaration: OAI.PowerSaving.transform_main
      file: OAI/Computability/FourierTransform/Main.lean

    - comparator_config: ComparatorChallenges/UniformFourier.json
      declaration: OAI.PowerSaving.convolution_main
      file: OAI/Computability/FourierTransform/Main.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.