Conjectures.io

Combinatorics

Green40.green_40.variants.arbitrary_subsets

Does f~(r)→∞\tilde{f}(r) \to \infty? [Gr24]

References

  • [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 ↔ Filter.Tendsto Green40.f_tilde Filter.atTop (nhds ⊤)

What you must prove

import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/40.lean

Source type SHA-256
sha256:d29e1e3a808151f496305c306c2123be6ea34e5e51aecc88b175e0e4a6ade912
Task id
fc-379fc029-variants-arbitrary-subsets-b8ad71f7bc-formalized-v1
Task commitment
sha256:a34486afbf4d282e6b0521fdf0209813c4376740e0c3449915eaeef14f6d7a84

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.