Combinatorics
Approved
The limiting lower covering density of radius-two linear codes is f(2) = 1. This establishes the radius-two target, not the separate question about growing covering radius.
Submitted by JenW1N
Formal statement
Proof target
import Mathlib
import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green40.green_40.f_two_eq_one" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ Green40.f 2 = 1Original 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 · 6 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
1 Sept 2026
Sphere-covering lower bound and equality reduction for Green 40 at radius two
5EyGbW…7GEFVR · 6 lemmas
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-green-40-f-two-eq-one-2398632669e94a0434102d7a-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/green-40-f-two-eq-one →