Combinatorics
WithdrawnDate added
Withdrawn 30 Sept 2026
WITHDRAWN (removed from the open catalog at Ben Green’s request; prior solved entries and results remain available)
1 piece from 1 personlast one 2 months ago
Formal statement
Proof target
import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green40.green_40" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ Filter.Tendsto Green40.f Filter.atTop (nhds ⊤)Original conjecture source: FormalConjectures/GreensOpenProblems/40.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.
1 piece · 15 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
1 Sept 2026
Sanity value f(1) and the comparison f-tilde <= f for Green 40
5FqLp5…FfZZiK · 15 lemmas