Erdős Problem 699: every counterexample has n ≤ j²
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-27-000020
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000020/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000020/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'