Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. With the least prime and the least integer with (so always), the claimant answers the three questions of Problem 456 no, no and yes, unconditionally. First and second questions: the equality set has positive lower density, that is, for some and all large , so fails on a positive proportion of and , equal to there, does not tend to infinity for almost all . The argument, as the claim's summary describes it, combines a weighted logarithmic tightness estimate for an auxiliary cofactor sum with sieve bounds and a second-moment count; the earlier manuscript described below counts base triples with , prime and , so that any smaller totient cover of would contain a prime (its Definition 4.1). Third question: call a uniqueness prime when is the only with ; the claim is that , through explicit totient identities for a family of linear forms, a multidimensional sieve with one rough composite auxiliary value, and a count over disjoint fibers of . The claim was registered on the site's proof-claims page on 2026-09-23 by David Turturean, who names GPT-6-Astra Pro as the system used, with earlier work by ChatGPT-5.5-Pro and Claude; the write-up is the Overleaf document linked above.
An earlier manuscript of the same author, posted to the problem's thread on 4 May 2026 and recorded on its claim page (71 pages, digested on its card), proves the positive-density theorem and the first two answers (its Theorem 1.1 and Corollary 1.2) and answers the third question only under Dickson's conjecture for the triple (its Theorem 1.4); the claimant's note on the site says that their earlier comment settled the first two questions and that the new manuscript removes the prime-tuple hypothesis from the third. The card's digest is author-recorded and is not an acceptance.
Submission note. Posted to erdosproblems.com as a proof claim by David Turturean (account DavidTurturean) on 23 September 2026, giving "GPT-6-Astra Pro; earlier work: ChatGPT-5.5-Pro and Claude" as the AI used:
I claim unconditional answers to all three questions: no, no, and yes. The equality set has positive lower density: for some ,
for all sufficiently large . This refutes the first two assertions, which have now been autoformalized down to results from literature. The argument, which I had posted in Spring of 2026, combines weighted logarithmic tightness for an auxiliary cofactor sum with sieve estimates and a second-moment count. For the third question, call a uniqueness prime when is the unique positive integer satisfying . We(?) prove
The proof combines explicit totient identities for a family of 54 linear forms, a multidimensional sieve with one rough composite auxiliary value, and a count using disjoint fibers of . No prime-tuple conjecture is required anymore, as my previous solution in the comments did. Notes: My earlier comment solved the first two questions. The full manuscript now proves the third unconditionally. Three fresh simple Pro audits of the corrected proof: 1, 2, 3. The Lean repository formalizes the first two answers with ten stated literature assumptions. The unconditional third is coming soon. The remaining question took a few hours with GPT-6-Astra Pro in a harness.
Formalization. The repository linked above, at its head commit of
2 September 2026, formalizes the Dickson-conditional manuscript first posted
on 4 May 2026, not this write-up. By its README, the first two answers
(erdos_456_questions_one_two) rest on ten cited literature results stated
as axioms. The third question is proved only under the Dickson-triple
hypothesis (erdos_456_question_three_of_dickson). The unconditional third
answer claimed here is not formalized. No build, axiom audit or statement
audit of the repository was made in this corpus.
Depends on. For the first two answers, the positive-density theorem of the earlier manuscript.
Standing. A manuscript statement, pending, with no formalization of its own: the site's label is OPEN (page last edited 7 October 2025), the proof-claims tab carries this one full claim with no comments, no referee report or arXiv record exists, and no outside reviewer has accepted the argument.