{"id":"palomar/PALOMAR-2026-10-27-000020","url":"https://github.com/Paulee314/erdos699-lean/tree/814f545f5f6475786aa5a04e4e795a25cda3670c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000020-v1.json","repo":"https://github.com/Paulee314/erdos699-lean","tags":["math.NT","msc:11B65","msc:11A05"],"score":0,"title":"Erdős Problem 699: every counterexample has n ≤ j²","trust":"high","domain":"math.NT","source":"palomar","authors":["Paul Lee"],"reviews":0,"subject":"math.NT","summary":"Erdős Problem 699 (Erdős and Szekeres 1978) asks whether for every 1 ≤ i < j ≤ n/2 there is a prime p ≥ i dividing gcd(C(n, i), C(n, j)). The problem is open. Using the statement from google-deepmind/formal-conjectures with the single extra hypothesis j² < n, this project proves in Lean 4 with Mathlib that the answer is yes whenever j² < n; equivalently, every counterexample (n, i, j) has n ≤ j². The proof combines the Erdős–Szekeres inequality gcd(C(n, i), C(n, j)) ≥ C(n, i)/C(j, i) ≥ (n/j)^i, which follows from the identity C(n, j) C(j, i) = C(n, i) C(n − i, j − i), with an upper bound for…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Erdős Problem 699: search to 10^12 and the bound n ≤ j²","identifier":"","relationship":"formalizes"}]}