Skip to content

feat: Add Unconditional Odlyzko Bound problem #477

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
bixbyr wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: Add Unconditional Odlyzko Bound problem #477

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions LeanEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,3 +16,4 @@ import LeanEval.NumberTheory.SmallHouse
import LeanEval.Topology.CerfGammaFour
import LeanEval.Topology.HomotopyGroups
import LeanEval.Topology.SmaleConjecture
import LeanEval.NumberTheory.OdlyzkoBound
23 changes: 23 additions & 0 deletions LeanEval/NumberTheory/OdlyzkoBound.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Comment on lines +14 to +19

@alreadydone alreadydone Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is equivalent to

Suggested change
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
theorem odlyzko_bound_unconditional :
∃ (c : ℝ), c < 1 ∧
∀ (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) * c := by

and I think it's better to use Real.eulerMascheroniConstant and Real.pi in the bases of the exponentiation.
Image
(formula from ImperialCollegeLondon/FLT#458 (comment))

sorry

end NumberTheory
end LeanEval
9 changes: 9 additions & 0 deletions manifests/problems/odlyzko_bound.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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."
Loading