Combinatorics

Green9.green_9_ii

Problem 9 (ii): is

r_5(N) \ll N(\log N)^{-c}

References

Gr24] [Green, Ben. "100 open problems." (2024).

[BlSi20] Bloom, Thomas F., and Olof Sisask. "Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions." arXiv preprint arXiv:2007.03528 (2020).

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ c > 0, (fun N => ↑(Green9.r 5 N)) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ (-c)

What you must prove

import FormalConjectures.GreensOpenProblems.«9»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green9.green_9_ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/9.lean

Source type SHA-256: sha256:829f0d1be13f178ae390df671362b0071ce3bd5b442d5e6a799cfede4f1780b5
Task id: fc-379fc029-green9-green-9-ii-94611b915b-formalized-v1
Task commitment: sha256:72e936ad5be3d1697dd47009eb2ac2e9a8897c99c675596bf006501be80c3344

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.