Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 730
claims/: The 1 claim page of Problem 730, one per claimant's result; the problem's standing derives from them.
Statement. Are there infinitely many pairs of integers such that and have the same set of prime divisors?
Status. Solved. The site labels the problem SOLVED (page last edited 1
September 2026) and credits GPT Pro, prompted by Price, for a proof that
infinitely many have and with the
same prime divisors, at least a constant times of them below
for all large ; the result is recorded on the claim page
Price 2026,
and the site's proof-claim entry states that the proof has been accepted as
correct. The question is a yes-or-no question answered yes, so the claim
value is proved. A third-party Lean formalization of the argument is
registered with the Palomar registry and copied into Boris Alexeev's
repository of formalized Erdős problems; this corpus has built neither, and
nothing is refereed. The standing in the frontmatter derives from the claim
page.
Source. erdosproblems.com/730, accessed 2026-09-04 and, with its discussion thread, its proof-claims page and the community database, 2026-10-07. Cite as: T. F. Bloom, Erdős Problem #730, https://www.erdosproblems.com/730.
References.
- [EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of . Math. Comp. (1975), 83-92. Library home: erdos_1975_prime_factors.
Formalization. Statement in formal-conjectures (as of 2026-10-07), tagged solved, with the pair set written as pairs ; it names as the problem's formal proof Will Blair's Lean development, which the Palomar registry verified against that statement on 2026-08-22, and it records the pairs and and the non-consecutive pair as checked variants. The development is linked, at pinned commits, from the claim page. This corpus has not built it.
Current assessment
The question, as the site states it (page last edited 1 September 2026): are there infinitely many pairs such that and have the same set of prime divisors? It comes from the concluding remarks of [EGRS75], whose authors were sure the answer is yes, gave the examples and , that is the consecutive pairs and , and had no proof. The answer is yes.
Examples and data. The site records the consecutive pairs and , the OEIS sequence A129515 of those for which some larger works, and the triple whose three central binomial coefficients share one set of prime divisors; the pair , found by AlphaProof and already implicit in the OEIS table, was the first recorded example with . The thread reports computer searches with two tools, and their reports agree where their ranges overlap. Firsching's search repository lists pairs that arise from no run of consecutive values: with neither nor a pair, the smallest at (then , , and ), where the middle coefficient differs from the outer two at the prime alone, a case its notes prove requires ; at and , where is a pair, and at , where and are pairs but is not (the repository's notes describe this example the other way round, but Kummer's criterion shows that of the four coefficients only is divisible by , and no other prime separates them); and at . A 2026 verification repository, announced in the thread, classified every pair it found: below for every and below for (the first run of four consecutive values starts at ), below for (the first run of five consecutive values starts at ) and below for (the first run of six at ), every pair arises from a run, and the posting asks where the other repository's examples appear. Those examples lie above the heights the classification searched for their distances, so the two reports do not conflict. Whether pairs exist for every is a question the thread raises and nothing settles.
Proof. The accepted claim page Price 2026 records the result the site credits: an argument of the AI system GPT Pro, posted by Liam Price to the thread on 2026-06-24 and submitted as the problem's proof claim on 2026-07-15, proving that infinitely many consecutive pairs work, with at least a constant times such below for all large . Kummer's theorem turns the entry or exit of a prime between and into a base- digit condition on the quotients of and by their prime-power divisors; an explicit quadratic family with and splits the obstructions into four branches, on each of which a Fourier estimate for incomplete quadratic sums bounds the proportion of parameters with restricted digits by about at depth , and a count over the obstruction primes finishes. Will Blair's Lean development, formalized with the AI systems Codex and Claude Code and registered with the Palomar registry on 2026-08-22, proves the pair set infinite by way of a positive lower density for the family; its record says it reconstructs the analytic sections from the public summary and a route mapping posted by another forum user, and that no independent human review of the mathematics was performed. The site's acceptance of the proof claim is the independent review on record.
Search scope, 2026-10-07: the site's problem page, its discussion thread (7 comments), its proof-claims page (one claim, accepted), the community database, the formal-conjectures file, the Palomar registry record and the two Lean repositories. The community database's row records the status solved (last update 2025-08-31) and the formal status unformalized, which the claim page notes.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.