{"id":"palomar/PALOMAR-2026-08-22-000001","url":"https://github.com/williamjblair/lean-proofs/tree/03729c9cbb0b602f5a828bb850c85e84c5a6d460","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000001-v1.json","repo":"https://github.com/williamjblair/lean-proofs","tags":["math.NT","math.CO","msc:11B65","msc:11N13","msc:11A41","msc:11B13","number-theory","erdos-problems","lean-formalization","binomial-coefficients"],"score":0,"title":"williamjblair/lean-proofs","trust":"high","domain":"math.NT","source":"palomar","authors":["Will Blair"],"reviews":0,"subject":"math.NT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"Comment on Erdős Problem #730 asserting, with a one-paragraph gist, that GPT Pro proves infinitely many consecutive pairs (n, n+1)","identifier":"https://www.erdosproblems.com/forum/thread/730","relationship":"formalizes"},{"title":"Closing derivation ('Proof Route Mapping') linked as a follow-up, reproducing the algebraic skeleton of the argument; the analytic sections exist only in a private document and are reconstructed in this formalisation","identifier":"https://chatgpt.com/share/6a3c7e81-cab8-83eb-a247-cd10b62e80fb","relationship":"adapts"},{"title":"Bernt Lindström, 'Well distribution of Sidon sets in residue classes', J. Number Theory 69 (1998), 197–200","identifier":"https://doi.org/10.1006/jnth.1997.2212","relationship":"adapts"}]}