Combinatorics

Green40.green_40.f_two_eq_one

It is not known whether f(2) = 1 [Gr24]

References

Gr24] [Ben Green's Open Problem 40

[Da90] Davydov, Alexander Abramovich. "Construction of linear covering codes." Problemy Peredachi Informatsii 26.4 (1990): 38-55.
[CHL97] Cohen, G., Honkala, I., Litsyn, S., & Lobstein, A. (1997). Covering codes (Vol. 54). Elsevier.
[St94] R. Struik, Covering codes, PhD Thesis, Eindhoven University of Technology, the Netherlands, 106 pp, 1994.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Green40.f 2 = 1

What you must prove

import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green40.green_40.f_two_eq_one" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/40.lean

Source type SHA-256: sha256:dd9ab9a1a25d01d3421a1597a6377fd04c2a56fbd1800ba539e89034ddbb8ec4
Task id: fc-379fc029-green-40-f-two-eq-one-1e4757c2b3-formalized-v1
Task commitment: sha256:897235bf5120aa2a01468719e4de29d5c15f6c69028ecf4a93b0100cc6217a61

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.