Conjectures.io

Combinatorics

Green40.green_40

Does f(r)→∞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 Filter.atTop (nhds ⊤)

What you must prove

import FormalConjectures.GreensOpenProblems.«40»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/40.lean

Source type SHA-256
sha256:baa8efc094db058dc4acdf7d60097c3c89aca17590aa37de890584a421e820a2
Task id
fc-379fc029-green40-green-40-c4a54910ce-formalized-v1
Task commitment
sha256:bb62bc75edf4ee41729792663186920b4dff11f915140805670b0fb621348ac4

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.