Wikipedia · test · AMS 11
easyknown result, no worker yet
Hall's conjecture
Exercise · elkies_bound
Elkies' example shows that such must be
less than . Note that simple linarith does not work here.
Formal statement · Lean 4.lean
theorem elkies_bound (C : ℝ) : HallIneq C 2⁻¹ → C < 0.0215 := by
sorryProof. sorry
Nobody has tried yet.