Combinatorics
Green72.green_72
**Green's Open Problem 72 / No-three-in-line problem**: The no-k-in-line conjecture holds for .References
- [GK2025] Grebennikov, A. Kwan, M. No $(k + 1)$-in-line problem for large constant $k$. https://arxiv.org/abs/2510.17743
No one has attempted this yet.
Formal statement
Lean type
∀ {N : ℕ}, 3 ≤ N → Green72.NoKInLineFor 3 NWhat you must prove
import FormalConjectures.GreensOpenProblems.«72»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green72.green_72" := by
sorry
end Bounty
Pinned source: FormalConjectures/GreensOpenProblems/72.lean
- Source type SHA-256
- sha256:89e65e952fc8e9f8c7344e71a61043775a01fbe01bc01c718c389ecc2775f101
- Task id
- fc-379fc029-green72-green-72-00559620fa-formalized-v1
- Task commitment
- sha256:a8dca2b3cac151afddd1c5dce8791c2de6df03c3dbb23d433a90e5e78c238a18
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.