HEXAGONbeta

Bounds for Erdős Problem #188: 7≤k≤607\le k\le 60

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatorics

Contributed by Carson Crocker ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

Let ℓk\ell_k denote kk collinear points with consecutive distances 11. Erdős Problem #188 asks for the least kk such that the plane can be colored red and blue with no two red points at distance 11 and no blue copy of ℓk\ell_k. Previous work gives 6≤k≤63306\le k\le 6330, with the lower bound due to Tsaturian and the upper bound due to Currier, Mody, Xie and Zhang. We prove 7≤k≤607\le k\le 60. For the lower bound we show that every red/blue coloring of the plane contains two red points at distance 11 or a blue ℓ6\ell_6, following the skeleton of Arman and Tsaturian's proof in three dimensions; four distance lemmas are reduced to explicit unsatisfiable propositional formulas, certified by DRAT proofs. For the upper bound we give an explicit periodic coloring whose red set consists of 9090 closed regular 2424-gons of 4848 different sizes, all of diameter less than 0.9990.999, in each period, with rational centers and sizes. Any two cells are either far apart (all distances between their points exceed 11) or close together (all distances are less than 11), which is checked in exact arithmetic for all periodic translates and rules out red unit pairs. That every ℓ60\ell_{60} contains a red point is proved by a computer-assisted verification: for every unit direction uu, the sets R−juR-ju, j=0,…,59j=0,\dots,59, cover the period torus, with every inclusion checked in rigorous ball arithmetic. A second, separately written program, based on a reduction to one-dimensional covering problems solved in outward-rounded interval arithmetic, confirms this. The computations, the verification code and drafts of the text were produced with AI tools under the author's direction; all proof certificates and verification programs are public (doi:10.5281/zenodo.23405962).

Provenance statement

I am not a professional mathematician; I work full time in corporate strategy. The search, certificate generation, verification programs and drafts of the text were produced by Claude (Anthropic, via Claude Code) under my direction; ChatGPT (OpenAI) was used for adversarial review. The two upper-bound checkers were written by Claude in separate sessions without shared code, using different verification methods (they may still share mathematical assumptions). The lower-bound SAT certificates are DRAT proofs checked with drat-trim; this checks unsatisfiability, and the geometric encoding is checked separately by the package scripts. I understand and can explain the two main reductions (why the far/close property of the cells rules out red unit pairs, and why covering the torus by 60 translates forces every blue l_60 to hit red), but not every technical step. No human expert has checked the proof; Gabriel Currier commented on an earlier draft and suggested the mixed-size cell idea, but did not check the proof. Code, certificates and logs: doi:10.5281/zenodo.23405962 (v5).

References

  1. A. Arman and S. Tsaturian, Equally spaced collinear points in E uclidean R amsey theory , 2017, arXiv:1705.04640.arXiv
  2. — , A result in asymmetric E uclidean R amsey theory , Discrete Math. 341 (2018), no. 5, 1502--1508, arXiv:1702.04799.arXiv
  3. A. Biere, K. Fazekas, M. Fleury, and M. Heisinger, CaDiCaL , K issat, P aracooba, P lingeling and T reengeling entering the SAT C ompetition 2020 , Proc. of SAT Competition 2020 -- Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1, University of Helsinki, 2020, pp. 51--53.
  4. T. F. Bloom, Erd ő s P roblem #188 , https://www.erdosproblems.com/188, accessed 2026-09-27.link
  5. D. Conlon and J. Fox, Lines in E uclidean R amsey theory , Discrete Comput. Geom. 61 (2019), no. 1, 218--225.
  6. D. Conlon and Y.-H. Wu, More on lines in E uclidean R amsey theory , C. R. Math. Acad. Sci. Paris 361 (2023), 897--901, arXiv:2208.13513.arXiv
  7. C. Crocker, Certificates for E rd ő s P roblem #188: 7k7 k , Zenodo, 2026, .
  8. L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt, Jr., M. Kaufmann, and P. Schneider-Kamp, Efficient certified RAT verification , Automated Deduction -- CADE 26, Lecture Notes in Comput. Sci., vol. 10395, Springer, 2017, pp. 220--236.
  9. G. Csizmadia and G. T ó th, Note on a R amsey-type problem in geometry , J. Combin. Theory Ser. A 65 (1994), no. 2, 302--306.
  10. G. Currier, P. Mody, Z. Xie, and J. Zhang, Improved bounds for lines and 1-separated sets in E uclidean R amsey theory , 2026, arXiv:2606.17194.arXiv
Show all 27 referencesShow fewer references
  1. G. Currier, K. Moore, and C. H. Yip, Any two-coloring of the plane contains monochromatic 3-term arithmetic progressions , Combinatorica 44 (2024), no. 6, 1367--1380.
  2. — , Avoiding short progressions in E uclidean R amsey theory , J. Combin. Theory Ser. A 217 (2026), Paper No. 106080, arXiv:2404.19233.arXiv
  3. A. D. N. J. de Grey, The chromatic number of the plane is at least 5 , Geombinatorics 28 (2018), no. 1, 18--31.
  4. P. Erd ő s and R. L. Graham, Old and new problems and results in combinatorial number theory , Monographies de L'Enseignement Math é matique, vol. 28, L'Enseignement Math é matique, Geneva, 1980.
  5. P. Erd ő s, R. L. Graham, P. Montgomery, B. L. Rothschild, J. Spencer, and E. G. Straus, Euclidean R amsey theorems I , J. Combin. Theory Ser. A 14 (1973), 341--363.
  6. — , Euclidean R amsey theorems II , Infinite and Finite Sets (Colloq., Keszthely, 1973), Colloq. Math. Soc. J á nos Bolyai, vol. 10, North-Holland, Amsterdam, 1975, pp. 529--557.
  7. — , Euclidean R amsey theorems III , Infinite and Finite Sets (Colloq., Keszthely, 1973), Colloq. Math. Soc. J á nos Bolyai, vol. 10, North-Holland, Amsterdam, 1975, pp. 559--583.
  8. P. Frankl and R. M. Wilson, Intersection theorems with geometric consequences , Combinatorica 1 (1981), 357--368.
  9. J. F ü hrer and G. T ó th, Progressions in E uclidean R amsey theory , European J. Combin. 125 (2025), Paper No. 104105, arXiv:2402.12567.arXiv
  10. A. Ignatiev, A. Morgado, and J. Marques-Silva, PySAT : A P ython toolkit for prototyping with SAT oracles , Theory and Applications of Satisfiability Testing -- SAT 2018, Lecture Notes in Comput. Sci., vol. 10929, Springer, 2018, pp. 428--437.
  11. L. Iv á n, Monochromatic point sets in the plane and in space , Master's thesis, University of Szeged, 1979.
  12. F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic , IEEE Trans. Comput. 66 (2017), no. 8, 1281--1292.
  13. R. Juh á sz, Ramsey type theorems in the plane , J. Combin. Theory Ser. A 27 (1979), no. 2, 152--160.
  14. A. M. Raigorodskii, On the chromatic number of a space , Russian Math. Surveys 55 (2000), no. 2, 351--352.
  15. A. D. Szlam, Monochromatic translates of configurations in the plane , J. Combin. Theory Ser. A 93 (2001), no. 1, 173--176.
  16. S. Tsaturian, A E uclidean R amsey result in the plane , Electron. J. Combin. 24 (2017), no. 4, Paper 4.35, arXiv:1703.10723.arXiv
  17. N. Wetzler, M. J. H. Heule, and W. A. Hunt, Jr., DRAT-trim : Efficient checking and trimming using expressive clausal proofs , Theory and Applications of Satisfiability Testing -- SAT 2014, Lecture Notes in Comput. Sci., vol. 8561, Springer, 2014, pp. 422--429.

Version history

  1. v1Submitted by Carson CrockerInitial depositCurrentOct 17, 2026