Open Research Index

williamjblair/lean-proofs

Will Blair

Palomar Registrypalomar/PALOMAR-2026-08-22-000001Aug 22, 2026math.NTscore 0

Machine-checked Lean 4 proofs of solved research problems from the Erdős problems collection, hosted as stable formal_proof targets for Google DeepMind's Formal Conjectures. The principal result is an affirmative answer to Erdős Problem #730 (Erdős, Graham, Ruzsa and Straus, 1975): the set of pairs n < m for which binom(2n, n) and binom(2m, m) have the same set of prime divisors is infinite, and in fact contains infinitely many consecutive pairs (n, n + 1). The proof formalises the argument posted informally by Liam Price on the problem's discussion page on 24 June 2026: Kummer's theorem…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-22-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-22-000001/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-08-22-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'