Combinatorics

Green9.green_9_iii

Problem 9 (iii): is

r_4(\mathbf{F}_5^n) \ll N^{1-c}

, where

N=5^n

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 => ↑(Finset.maxAPFreeCard 4 Finset.univ)) =O[Filter.atTop] fun n => (5 ^ n) ^ (1 - c)

What you must prove

import FormalConjectures.GreensOpenProblems.«9»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/9.lean

Source type SHA-256: sha256:52c06f9eeccbf6b3e1a76212d62eb73abb1935bd716c73681a6a23350c52fe36
Task id: fc-379fc029-green9-green-9-iii-1fd1f237fe-formalized-v1
Task commitment: sha256:d36fdd7b136dc879d28c5cf630316acaf324d10dbb289f62af1a0de139afce0c

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.