Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«51»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green51.green_51.one_half" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (k : ℝ),
    0 < k → ∃ c, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ α > 1 / 2 - k / √↑n, α ≤ 1 → n ≤ Green51.guaranteedMaxCosetDim n α + c

Original conjecture source: FormalConjectures/GreensOpenProblems/51.lean

Source type SHA-256: sha256:1ee955eab2652fc3b13aa3a43d36344759718a27f818afde66c86c13befbb67d
Task id: fc-8432eac9-green-51-one-half-c1068fe73b-formalized-v1
Task commitment: sha256:9e80ef6216da982ff582d20419ed0b0393952ef9fa1c197726f891246db4d327

References

Green's open problem 51 - one half · Conjectures.io

Every problem here was open when it entered the pool.

Green's open problem 51 - one half

What has been built

Where this lives