∑ Math Proof Playground › Checkerboard no-three-in-line

Defect moments and four-direction asymptotics for checkerboard no-three-in-line sets

A research package built around Thomas Prellberg's 2026 checkerboard-restricted no-three-in-line problem.

Research draft · external review required Exact symbolic and solver checks included Partial sorry-free Lean 4 formalization Full all-slope NTIL lower bound remains open

Abstract

For one color class of an n×n checkerboard, every no-three-in-line set obeys capacity two on rows, columns and diagonals of slopes ±1. The project develops a defect-moment identity for these four direction families, derives finite upper bounds, and studies Prellberg's finite and continuum linear programs. The strongest current research-draft claims are a proof of the finite bound Dmono(n) ≤ 2n−4, matching upper and lower certificates for the four-direction LP limit α = 1.576823396873808…, and an asymptotic rounding argument for the integral four-direction packing problem. The classical all-slope no-three-in-line construction problem is not solved.

Claim map

StatementStatus in this repository
Dmono(n) ≤ 2n−4 for n ≥ 6Complete paper proof; exact symbolic, SMT/SAT and MIP corroboration; Lean formalizes the final algebraic contradictions.
Dmono(n) ≤ ceil(2^(2/3)n)Research-draft finite strengthening; exact algebraic certificates formalized, with the capacity majorization still paper-level.
Three four-direction LP limits equal αExact continuum primal/dual certificate plus continuum-to-finite transfer; independently checkable Python algebra.
Integral four-direction optimum equals αn+o(n)Paper-level argument using bounded-rank hypergraph edge coloring; not yet formalized in Lean.
Actual checkerboard NTIL limit equals αOpen. This requires controlling every rational slope simultaneously.

Core formulas

Dmono(n) ≤ 2n − 4 (n ≥ 6) Dmono(n) ≤ min(2n − 4, ceil(2^(2/3)n)) α = 2(1 − p) = 1.576823396873808… 401p³ − 331p² + 19p + 7 = 0 401α³ − 1744α² + 2240α − 768 = 0

The exact checkerboard conjectures are not currently entries in Google DeepMind's Formal Conjectures repository. The repository does contain the classical unrestricted no-three-in-line problem, which is stronger and remains unsolved here.

Proof architecture

  1. Encode unused row, column and principal-diagonal capacity as defect measures.
  2. Compute the same centered second moment from the row/column side and the diagonal side.
  3. Use weighted Cauchy–Schwarz to obtain the master defect-moment inequality.
  4. At deficit one, compare the forced diagonal second moment with the largest geometrically possible offsets, ruling out size 2n−3.
  5. Match Prellberg's continuum dual certificate by an exact algebraic primal transport certificate.
  6. Transfer continuum certificates to finite LPs by exact sampling, smoothing and Riemann-sum arguments.
  7. For the four fixed directions only, round diffuse fractional solutions using bounded-rank small-codegree hypergraph edge coloring.

Verification boundary

Machine checked

  • cubic transformations and parity contradiction inequalities in Lean;
  • exact polynomial reductions;
  • finite SAT/SMT/MIP instances;
  • exact algebraic continuum-certificate identities;
  • selected exact rational all-line LP certificates.

Not yet fully formalized

  • capacity-profile derivation and complete master identity;
  • measure smoothing and continuum-to-finite lower transfer;
  • Kahn's hypergraph edge-coloring theorem and its application;
  • the full all-slope NTIL lower bound, which remains open.
“Partial Lean formalization” is intentional. No page or badge should describe the whole checkerboard result as Lean-verified until the combinatorial, analytic and hypergraph components are also formalized.

Files

HUMAN_PROOF.mdReadable theorem chain and proof sketch
VERIFICATION_REPORT.mdClaim-by-claim verification audit
PRIOR_ART.mdWhat comes from Prellberg and what appears new
FORMALIZATION_STATUS.mdExact Lean scope
Checkerboard.leanLean project entry point
Formal Conjectures issue draftProposal to add the checkerboard-specific statements

Reproduce the Lean checks

cd proofs/lean/Checkerboard lake update lake build # Guard against unfinished proof markers grep -RnE '\bsorry\b|\badmit\b' .

GitHub Actions workflow: .github/workflows/verify-checkerboard.yml.

What remains open

The major missing theorem is a correlated multiscale rounding or direct construction producing (α−o(1))n actual checkerboard points with at most two points on every Euclidean line. Fixed-direction rounding does not solve this, because the number of relevant primitive directions grows with n.

Source problem: T. Prellberg, “No-three-in-line sets on the checkerboard grid”. Classical formal entry: Formal Conjectures Green 72.