From 37bdfa8dc1414afe7800045d1d852f65fc44f77f Mon Sep 17 00:00:00 2001
From: bixbyr <bixbyr@gmail.com>
Date: Mon, 20 Jul 2026 21:20:45 -0700
Subject: [PATCH] feat: Add Unconditional Odlyzko Bound problem

Co-authored-by: Gemini 3.1 Pro <gemini@google.com>
---
 LeanEval.lean                           |  1 +
 LeanEval/NumberTheory/OdlyzkoBound.lean | 23 +++++++++++++++++++++++
 manifests/problems/odlyzko_bound.toml   |  9 +++++++++
 3 files changed, 33 insertions(+)
 create mode 100644 LeanEval/NumberTheory/OdlyzkoBound.lean
 create mode 100644 manifests/problems/odlyzko_bound.toml

diff --git a/LeanEval.lean b/LeanEval.lean
index a5ae96df..4ba87f9d 100644
--- a/LeanEval.lean
+++ b/LeanEval.lean
@@ -16,3 +16,4 @@ import LeanEval.NumberTheory.SmallHouse
 import LeanEval.Topology.CerfGammaFour
 import LeanEval.Topology.HomotopyGroups
 import LeanEval.Topology.SmaleConjecture
+import LeanEval.NumberTheory.OdlyzkoBound
diff --git a/LeanEval/NumberTheory/OdlyzkoBound.lean b/LeanEval/NumberTheory/OdlyzkoBound.lean
new file mode 100644
index 00000000..65639fa2
--- /dev/null
+++ b/LeanEval/NumberTheory/OdlyzkoBound.lean
@@ -0,0 +1,23 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace NumberTheory
+
+open NumberField
+
+/-- **Unconditional Odlyzko Bound**. 
+There exists a constant `c > 0` such that for every number field `K`, 
+the absolute value of its discriminant is bounded below by `(60.8)^{r_1} * (22.3)^{2 r_2} * e^{-c}`,
+where `r_1` and `r_2` are the number of real and complex places of `K` respectively. -/
+@[eval_problem]
+theorem odlyzko_bound_unconditional :
+    ∃ (c : ℝ), 0 < c ∧
+    ∀ (K : Type*) [Field K] [NumberField K],
+      let r1 := (InfinitePlace.nrRealPlaces K : ℝ)
+      let r2 := (InfinitePlace.nrComplexPlaces K : ℝ)
+      ((discr K).natAbs : ℝ) ≥ (60.8 : ℝ) ^ r1 * (22.3 : ℝ) ^ (2 * r2) * Real.exp (-c) := by
+  sorry
+
+end NumberTheory
+end LeanEval
diff --git a/manifests/problems/odlyzko_bound.toml b/manifests/problems/odlyzko_bound.toml
new file mode 100644
index 00000000..6e97b7a0
--- /dev/null
+++ b/manifests/problems/odlyzko_bound.toml
@@ -0,0 +1,9 @@
+id = "odlyzko_bound"
+title = "Unconditional Odlyzko Bound"
+test = false
+module = "LeanEval.NumberTheory.OdlyzkoBound"
+holes = ["odlyzko_bound_unconditional"]
+submitter = "Ryan Smith"
+notes = "The finite, unconditional version of the Odlyzko bound for the absolute discriminant of a number field, framed as an existence theorem for the constants."
+source = "Odlyzko, A. M. (1976). 'Lower bounds for discriminants of number fields.' Acta Arithmetica, 29(3), 275-297. See also Odlyzko, A. M. (1990) 'Bounds for discriminants and related estimates...'"
+informal_solution = "The proof evaluates the explicit formulas connecting the Dedekind zeta function to prime ideals using a specially chosen non-negative test function. By discarding the positive sum over the non-trivial zeros (unconditionally), one isolates log|D_K| on one side and a sum of integrals on the other, yielding the required constants."