A kernel-checked exclusion certificate for Erdős Problem 647, to 10^8
Erdős Problem 647 asks whether there is any n > 24 with max_{m 10^8. The exclusion is certified rather than searched at check time. A witness at a cover position is an offset together with prime-power pairs dividing m, certifying tau(m) >= prod (e + 1); every prime in a pair is below 1024 and is checked prime by eleven trial divisions, so no primality certificates appear anywhere. A chain of witnesses covers the interval and each certificate chunk is discharged by a single decide against the chain checker, so the Lean kernel certifies the arithmetic and the generator that produced it is…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-04-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-04-000003/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-09-04-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'