Combinatorics
Approved
The asymptotic constant gamma equals 1/3. The submission completes the upper bound and credits the earlier lower-bound contribution. This establishes the asymptotic target, not the separate finite-size statement.
Submitted by JenW1N
Formal statement
Proof target
import Mathlib
import FormalConjectures.GreensOpenProblems.«24»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green24.variants.conjecture" := by
sorry
end Bounty
Original conjecture (Lean type)
Green24.variants.gamma = 1 / 3Original conjecture source: FormalConjectures/GreensOpenProblems/24.lean
References
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.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.
3 pieces · 89 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
19 Sept 2026
Green 24: cyclic profile bounds by support peeling and the coefficient-invertible cases
5E7uWL…uzcwd3 · 50 lemmas
17 Sept 2026
Sharp lower bound gamma ≥ 1/3 and limsup reduction of Green 24 to a finite-n upper bound
5DAnjv…241SGH · 30 lemmas
1 Sept 2026
Lower bound gamma >= 1/12 for 3-term affine translates
5FqLp5…FfZZiK · 9 lemmas
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-variants-conjecture-219bf0a1394dccdfb334f0ec-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/green-24-variants-conjecture →