Update math/cs papers, formalizations, and verification data

CONTENTS.md

@@ -1,6 +1,6 @@
 # Mathematics manuscript collection
 
-**719 manuscripts covering 372 result families.**
+**721 manuscripts covering 373 result families.**
 
 [**Read the overview PDF**](overview.pdf).
 
@@ -752,7 +752,7 @@ We prove Uchida's conjecture on open homomorphisms of Galois groups. Every conti
 <tbody><tr>
 <td>
 
-**032. The rational Hodge conjecture for CM abelian varieties.** Proves the rational Hodge conjecture for every complex CM abelian variety, in every dimension and codimension. Through Milne's theorems, this also gives the Tate conjecture for all abelian varieties over finite fields and the Hodge standard conjecture for abelian varieties in every characteristic.
+**032. The rational Hodge conjecture for CM abelian varieties.** Proves the rational Hodge conjecture for every complex CM abelian variety, in every dimension and codimension. Through Milne's theorems, this also gives the Tate conjecture for all abelian varieties over finite fields and the Hodge standard conjecture for abelian varieties in every characteristic. ([Lean](lean/docs/032.md))
 
 </td>
 </tr></tbody>
@@ -1960,7 +1960,16 @@ We prove the three-dimensional Bochner–Riesz conjecture in its strict-order fo
 <tbody><tr>
 <td>
 
-**079. Local smoothing in three dimensions.** Resolves Sogge's local smoothing conjecture for the Euclidean wave equation in three spatial dimensions. The estimate holds throughout the full strict range $`2\lt p\lt \infty`$, with Sobolev regularity above $`\max\{0,1-3/p\}`$. In particular, the critical <i>L</i><sup>3</sup> estimate holds with every positive Sobolev loss.
+**079. Local smoothing for the Euclidean wave equation.** Proves Sogge’s local smoothing conjecture in every spatial dimension $`n\ge2`$, with arbitrarily small loss above the sharp Sobolev threshold. The wave estimate yields the Bochner–Riesz conjecture and, for $`2\le p\lt\infty`$, maximal bounds for these means and sharp bounds for Stein’s square function. It also gives Fourier restriction throughout the interior of the conjectured range for the sphere, compact paraboloid, and truncated cone, and local smoothing for the Schrödinger equation. The Kakeya and Nikodym maximal conjectures follow. In particular, every Euclidean Kakeya set has full Hausdorff dimension. ([Lean](lean/docs/079.md))
+
+</td>
+</tr></tbody>
+<tbody><tr>
+<td>
+
+&emsp;[Local smoothing for the Euclidean wave equation](preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf)
+
+We prove Sogge’s local smoothing conjecture for the Euclidean wave equation in every spatial dimension at least two. We deduce the Bochner–Riesz conjecture, maximal estimates for these means, and sharp bounds for Stein’s square function. We obtain Fourier restriction estimates for the sphere, the compact paraboloid, and the truncated cone throughout the interior of the conjectured range, as well as local smoothing for the Schrödinger equation. We also prove the Kakeya and Nikodym maximal conjectures. In particular, every Euclidean Kakeya set has full Hausdorff dimension.
 
 </td>
 </tr></tbody>
@@ -9137,6 +9146,22 @@ We realize finite positive diagonal affine maps of determinant one by effective
 
 We prove a uniform interior $`C^{1,\alpha_d}`$ estimate for bounded infinity-harmonic functions in every dimension <i>d</i> ≥ 3. For some $`\alpha_d\in(0,1/3]`$ depending only on the dimension, the gradient's supremum norm and <i>α</i><sub><i>d</i></sub>-Hölder seminorm on <i>B</i><sub>1/2</sub> are bounded by a dimension-dependent constant times the oscillation on <i>B</i><sub>1</sub>. The exponent is not explicit, and no endpoint or boundary regularity claim is made. In particular, infinity-harmonic functions are locally <i>C</i><sup>1</sup> on every open subset of ℝ<sup><i>d</i></sup>, for <i>d</i> ≥ 3.
 
+</td>
+</tr></tbody>
+<tbody><tr>
+<td>
+
+**378. Disproof of the Exponential Time Hypothesis.** For every fixed $`k\ge2`$, a deterministic algorithm counts the satisfying assignments of a $`k`$-CNF with $`n`$ variables and $`m`$ clauses in time $`(n+m)^{O_k(1)}2^{n/(\log n)^{1/2+o(1)}}`$. This yields superlinear circuit lower bounds for a language in $`\mathsf{E}^{\mathsf{NP}}`$ on infinitely many input lengths. ([Lean](lean/docs/378.md))
+
+</td>
+</tr></tbody>
+<tbody><tr>
+<td>
+
+&emsp;[The Exponential Time Hypothesis is False](preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf)
+
+We give a deterministic algorithm for exactly counting the satisfying assignments of an arbitrary $`k`$-CNF formula. For every fixed $`k\ge2`$, on a formula with $`n`$ variables and $`m`$ clauses, our algorithm uses space polynomial in $`n`$ and $`m`$ and runs in time $`(n+m)^{O_k(1)}2^{n/(\log n)^{1/2+o(1)}}`$. Our algorithm refutes the Exponential Time Hypothesis (ETH), which postulates that deciding 3-SAT on $`n`$ variables requires $`2^{\Omega(n)}`$ time in the worst case.
+
 </td>
 </tr></tbody>
 </table>

README.md

@@ -1,6 +1,6 @@
 # Readme
 
-This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model. 
+This repository contains mathematical manuscripts and supporting proof artifacts produced by an unnamed internal OpenAI model. 
 
 As part of model development, we evaluate our models on open research problems. We expanded these evaluations after performance on our existing mathematical evaluations saturated. Some outputs build upon earlier results produced by the models.
 
@@ -9,9 +9,11 @@ This collection includes results at different stages of verification. Not all ha
 Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly.
 We are also exploring community-hosted repositories for these materials. 
 
+In our view, these manuscripts are best understood as a form of raw research data, rather than polished academic papers. We defer to the math community completely on matters of credit, precedence, and concurrent work.
+
 ## Navigating the collection
 
-The current catalogue contains 719 manuscripts organized into 372 families. A family groups related papers, which may include a principal result, companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.
+The current catalogue contains 721 manuscripts organized into 373 families. A family groups related papers, which may include a principal result, companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.
 
 - Start with the [overview](overview.pdf) for descriptions of the families.
 - Use the [manuscript map](CONTENTS.md) to find individual papers and their supporting materials.

history.md

@@ -2,6 +2,25 @@
 
 For any withdrawn papers, their README files explain the gap and link to the retracted manuscript. For any updated papers, previously published editions remain accessible through the version notes in their README.
 
+## October 26, 2026
+
+**New Results Added**
+
+We have added two new manuscripts with accompanying Lean formalizations:
+
+- *Local smoothing for the Euclidean wave equation.* The proof uses an auxiliary partial differential equation to establish Sogge's local smoothing for waves in every spatial dimension at least two. It also yields the Kakeya maximal and dimension conjectures and Stein’s spherical restriction estimates throughout the interior of the conjectured range. We are releasing the model output directly, as we did in our October 6 release.
+- *The Exponential Time Hypothesis is False.* The paper gives a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space. The case of 3-SAT refutes the Exponential Time Hypothesis. An independent working group of computer scientists led by Russell Impagliazzo, Ramamohan Paturi, and Ryan Williams will examine and explain the proof. At the group’s request, we are making the materials public immediately so others can examine them as well.
+
+**Formalization Additions and Improvements**
+
+- *The rational Hodge conjecture for CM abelian varieties.* A Lean formalization was added.
+- Some Comparator configurations were fixed, and some Lean formalizations were improved. 
+
+**Auxiliary Files Included**
+
+- *The maximum number of mutually unbiased bases in dimension six.* We restored the C++ source and saved numerical records for the computation that excludes a fourth mutually unbiased basis. A Python checker verifies the consistency and coverage of the saved records.
+
+
 ## October 7, 2026
 
 **Withdrawals**

lean/ComparatorChallenges/Brenier.json

@@ -5,20 +5,7 @@
     "OAI.Problem358.one_third_stability",
     "OAI.Problem358.one_third_exponent_is_sharp"
   ],
-  "definition_names": [
-    "OAI.Problem358.E",
-    "OAI.Problem358.uniformMeasure",
-    "OAI.Problem358.IsSupported",
-    "OAI.Problem358.IsCoupling",
-    "OAI.Problem358.quadraticPlanCost",
-    "OAI.Problem358.wasserstein2",
-    "OAI.Problem358.graphPlan",
-    "OAI.Problem358.IsQuadraticOptimalMap",
-    "OAI.Problem358.IsUniqueQuadraticOptimalMap",
-    "OAI.Problem358.mapL2Dist",
-    "OAI.Problem358.cube",
-    "OAI.Problem358.HasExactlyThreeAtoms"
-  ],
+  "definition_names": [],
   "permitted_axioms": [
     "propext",
     "Quot.sound",

lean/ComparatorChallenges/DefocusingNLS.json

@@ -6,11 +6,7 @@
     "OAI.DefocusingNLS.gaussian_blowup",
     "OAI.DefocusingNLS.gaussian_not_almost_sure_global"
   ],
-  "definition_names": [
-    "OAI.DefocusingNLS.sobolevProduct",
-    "OAI.DefocusingNLS.schrodingerFlow",
-    "OAI.DefocusingNLS.sobolevOddPower"
-  ],
+  "definition_names": [],
   "permitted_axioms": [
     "propext",
     "Quot.sound",

lean/ComparatorChallenges/DefocusingNLS.lean

@@ -102,9 +102,12 @@ noncomputable def sobolevProductCoefficient (k : ℝ) (f g : FourierL2)
     (n : frequencyLattice) : ℂ :=
   ∑' m, sobolevFourierCoefficient k f m * sobolevFourierCoefficient k g (n - m)
 
-noncomputable def sobolevProduct (k : ℝ) (_hk : 6 < k) (f g : FourierL2) : FourierL2 :=
-  ⟨fun n => (sobolevProductWeight k n : ℂ) * sobolevProductCoefficient k f g n,
-    by sorry⟩
+noncomputable def sobolevProduct (k : ℝ) (_hk : 6 < k) (f g : FourierL2) : FourierL2 := by
+  classical
+  exact if h : Memℓp (fun n => (sobolevProductWeight k n : ℂ) *
+      sobolevProductCoefficient k f g n) ((2 : ℕ) : ℝ≥0∞) then
+    ⟨fun n => (sobolevProductWeight k n : ℂ) * sobolevProductCoefficient k f g n, h⟩
+  else 0
 
 run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}
 
@@ -117,7 +120,8 @@ noncomputable def fourierConjugate (f : FourierL2) : FourierL2 :=
 
 run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}
 
-noncomputable def sobolevOddPower (k : ℝ) (hk : 6 < k) : ℕ → FourierL2 → FourierL2
+noncomputable def sobolevOddPower (k : ℝ) (hk : ((6 : ℕ) : ℝ) < k) :
+    ℕ → FourierL2 → FourierL2
   | 0, f => f
   | m + 1, f => sobolevProduct k hk
       (sobolevProduct k hk (sobolevOddPower k hk m f) (fourierConjugate f)) f

lean/ComparatorChallenges/ElementaryPositivity.json

@@ -1,7 +1,9 @@
 {
   "challenge_module": "ComparatorChallenges.ElementaryPositivity",
   "solution_module": "OAI.Combinatorics.Chromatic.Main",
-  "theorem_names": [],
+  "theorem_names": [
+    "OAI.elementaryPositivityExpansion"
+  ],
   "definition_names": [
     "OAI.elementaryPositivityWitness"
   ],

lean/ComparatorChallenges/ElementaryPositivity.lean

@@ -60,4 +60,13 @@ def elementaryPositivityWitness (n : ℕ)
     G.PermutationWitness := by
   sorry
 
+theorem elementaryPositivityExpansion (n : ℕ)
+    (G : ElementaryPositivity.NaturalUnitIntervalGraph n) (r : ℕ) :
+    G.chromatic r =
+      ∑ σ : {σ : Equiv.Perm (Fin n) // G.Nondescent σ},
+        MvPolynomial.C (Polynomial.X ^ G.graphInversions σ.val) *
+          MvPolynomial.esymmPart (Fin r) (Polynomial ℕ)
+            ((elementaryPositivityWitness n G).theta σ) := by
+  sorry
+
 end OAI

lean/ComparatorChallenges/EuclideanFiveColor.json

@@ -4,9 +4,7 @@
   "theorem_names": [
     "OAI.EuclideanFiveColor.no_proper_five_coloring"
   ],
-  "definition_names": [
-    "OAI.EuclideanFiveColor.ProperColoring"
-  ],
+  "definition_names": [],
   "permitted_axioms": [
     "propext",
     "Quot.sound",

lean/ComparatorChallenges/HarmonicGrowth.lean

@@ -95,11 +95,7 @@ def MainClaim : Prop :=
     ∃ u : Fin (euclideanDimension n k + 1) → (Space n → ℝ),
       LinearIndependent ℝ u ∧ ∀ i, HarmonicGrowth g k (u i)
 
-
-
-axiom mainStatement : MainClaim
-
-theorem main : MainClaim := mainStatement
+theorem main : MainClaim := by sorry
 
 end HarmonicCounterexample
 

lean/ComparatorChallenges/HodgeConjectureCMAbelianVarieties/CM.lean

@@ -0,0 +1,57 @@
+module
+
+public import HodgeConjecture.Variants
+public import Mathlib.NumberTheory.NumberField.CMField
+public import Mathlib.LinearAlgebra.TensorProduct.Tower
+
+/-!
+# Complex multiplication on geometric rational H¹
+
+The Hodge filtration and cohomology are those of `HodgeConjecture`.
+Each CM-field factor acts on its own rank-one summand of rational H¹.
+-/
+
+@[expose] public noncomputable section
+
+open CategoryTheory AlgebraicGeometry ComplexPoint
+open scoped TensorProduct
+
+namespace HodgeCM
+
+/-- Coordinatewise multiplication, transported to a rational vector space. -/
+def diagonalAction {V : Type*} [AddCommGroup V] [Module ℚ V]
+    {ι : Type*} (K : ι → Type) [∀ i, Field (K i)] [∀ i, Algebra ℚ (K i)]
+    (e : V ≃ₗ[ℚ] ((i : ι) → K i)) (a : (i : ι) → K i) : Module.End ℚ V :=
+  e.symm.toLinearMap ∘ₗ LinearMap.mul ℚ ((i : ι) → K i) a ∘ₗ e.toLinearMap
+
+variable (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom]
+
+/-- The geometric rational-to-de Rham comparison extended to complex coefficients. -/
+def h1Comparison : ℂ ⊗[ℚ] H^1(X; ℚ) →ₗ[ℚ] H_dR^1(X) :=
+  TensorProduct.lift
+    ((Algebra.lsmul ℚ ℚ H_dR^1(X)).toLinearMap.compl₂
+      (fieldToDeRhamCohomologyLinear ℚ X 1))
+
+/-- Complex multiplication means that rational H¹ is a finite direct sum of
+rank-one spaces over CM number fields, whose diagonal action preserves the
+geometric holomorphic Hodge filtration. The fields may differ between factors. -/
+structure CMH1Data where
+  factors : ℕ
+  field : Fin factors → Type
+  [fieldStructure : ∀ i, Field (field i)]
+  [numberField : ∀ i, NumberField (field i)]
+  [cmField : ∀ i, NumberField.IsCMField (field i)]
+  model : H^1(X; ℚ) ≃ₗ[ℚ] ((i : Fin factors) → field i)
+  preserves_hodgeFiltration : ∀ (a : (i : Fin factors) → field i)
+      (z : ℂ ⊗[ℚ] H^1(X; ℚ)),
+    h1Comparison X z ∈ hodgeFiltrationComplexSubmodule X 1 1 →
+    h1Comparison X
+        (TensorProduct.map LinearMap.id (diagonalAction field model a) z) ∈
+      hodgeFiltrationComplexSubmodule X 1 1
+
+attribute [instance] CMH1Data.fieldStructure CMH1Data.numberField CMH1Data.cmField
+
+/-- The existence of geometric H¹ complex-multiplication data. -/
+def HasComplexMultiplication : Prop := Nonempty (CMH1Data X)
+
+end HodgeCM

lean/ComparatorChallenges/HodgeConjectureCMAbelianVarieties/Challenge.lean

@@ -0,0 +1,45 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+
+This file has been modified.
+-/
+module
+
+public import ComparatorChallenges.HodgeConjectureCMAbelianVarieties.CM
+
+/-!
+# Comparator challenge: the Hodge conjecture for CM abelian varieties
+
+The conclusion is the literal conclusion of the upstream abelian-variety
+special case. The only added condition is complex multiplication on H¹.
+-/
+
+@[expose] public section
+
+open CategoryTheory AlgebraicGeometry ComplexPoint
+
+namespace HodgeCM
+
+set_option warningAsError false in
+/-- Every rational Hodge class on a complex CM abelian variety is a rational
+linear combination of classes of algebraic subvarieties. -/
+theorem hodge_conjecture_for_cm_abelian_varieties
+    (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom]
+    [IsProjective X.hom] [GrpObj X]
+    (hCM : HasComplexMultiplication X) (p : ℕ) :
+    Hdg^p(X; ℚ) ≤ algebraicCycleClassSpan X p := by
+  sorry
+
+end HodgeCM