Combinatorics

Green24.variants.conjecture

Conjecture p.579 in [Aa19]:

\left({1}{3} + o(1)\right) n^2

References

Green, Ben. "100 open problems." (2024).

[Aa19] Aaronson, James. "Maximising the number of solutions to a linear equation in a set of integers." Bulletin of the London Mathematical Society 51.4 (2019): 577-594.
[HaL28] Hardy, G. H., and J. E. Littlewood. "Notes on the theory of series (VIII): an inequality." Journal of the London Mathematical Society 1.2 (1928): 105-110.

No one has attempted this yet.

Formal statement

Lean type

Green24.variants.gamma = 1 / 3

What you must prove

import FormalConjectures.GreensOpenProblems.«24»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green24.variants.conjecture" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/24.lean

Source type SHA-256: sha256:d9eac933e6ce242245030c7e03c096589f73a436c49d93ddc28b4e3b4561a808
Task id: fc-379fc029-variants-conjecture-8897bace5c-formalized-v1
Task commitment: sha256:6db070cfe96bdfc7eb7802ba5624087c94bb7860311d6289b254d48bcb09e629

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.