Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 48
claims/: The 2 claim pages of Problem 48, one per claimant's result; the problem's standing derives from them.
Statement. Are there infinitely many integers such that ?
Status. PROVED (LEAN). The site's label is PROVED (LEAN). The answer is yes: Ford, Luca and Pomerance proved in 2010 that and have infinitely many common values (refereed; the accepted claim page is Ford–Luca–Pomerance 2010), and Garaev's refereed sharpening of the count in 2011 is a second accepted claim page (Garaev 2011). The site's Lean marker refers to a community Lean formalization of the Ford–Luca–Pomerance argument, linked from their claim page; this corpus has not built or audited it.
Source. erdosproblems.com/48, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #48, https://www.erdosproblems.com/48.
References.
- [FLP10] Ford, Kevin and Luca, Florian and Pomerance, Carl, Common values of the arithmetic functions and . Bull. Lond. Math. Soc. (2010), 478-488.
- [Ga11] Garaev, Moubariz Z., On the number of common values of arithmetic functions and below . Mosc. J. Comb. Number Theory 1 (2011), no. 3, 42-49.
- [Gu04] Guy, Richard K., Unsolved problems in number theory, third edition, Problem Books in Mathematics, Springer (2004), xviii+437 pp.; B38 "Solutions of ", printed p. 144: the question as stated here, answered affirmatively by infinitely many twin primes or infinitely many Mersenne primes, with sporadic solutions such as . Library home: guy_2004_unsolved_problems_number_theory.
Formalization. The statement file
ErdosProblems/48.lean
of formal-conjectures (pinned at its commit of 2026-09-18) states the
question as erdos_48, answer(True), category research solved, with a
sorry body and a formal_proof attribute naming the community Lean file
linked from the claim page; see "Formalization and the Lean label" below.
Current assessment
The question (site formulation of 2026-09-04). Whether infinitely many pairs satisfy . PROVED (LEAN). The site's commentary records that the answer is yes by Ford, Luca and Pomerance [FLP10], that their count of common values up to was improved by Garaev [Ga11], and that the question is B38 of Guy's collection [Gu04]; it also notes that infinitely many twin primes would give the answer at once.
Standing. Two accepted full claims. The first, Ford–Luca–Pomerance 2010, is a refereed paper (Bull. Lond. Math. Soc. 42 (2010), 478–488) whose Theorem 1 gives infinitely many solutions and at least common values up to for some . The second, Garaev 2011, is a refereed paper (Mosc. J. Comb. Number Theory 1 (2011), no. 3, 42–49) whose Theorem 1 gives at least common values up to for every ; its proof refines Konyagin's alternative route together with the argument of the first paper, and the curator credits it in the commentary under the PROVED (LEAN) label. The problem's standing follows from either accepted claim.
Formalization and the Lean label. The site's label is PROVED (LEAN),
and the community database records a Lean formal status dated 2026-08-23.
The statement file of formal-conjectures names, in its formal_proof
attribute, the file src/latest/ErdosProblems/Erdos48.lean
of the repository plby/lean-proofs, whose header declares it a
formalization of a solution with Ford, Luca and Pomerance as informal authors
and Codex and GPT-5.6 Sol as formal authors; the file and its flattened copy
in Jayyhk/erdos-lean are formalization links on the Ford–Luca–Pomerance
claim page. They formalize that paper's argument and are not an independent
proof. This corpus has not built, kernel-checked or audited either file, so
no formalized evidence is listed.
Search scope and read depth. Search scope, 2026-10-07: the site's problem page and its empty proof-claims thread; the community database's entry (2026-10-06); the digests of the two source cards; the arXiv record of [FLP10] and the Crossref records of its journal version, for dates; the formal-conjectures statement file and the headers, theorem statements and axiom lines of the two community Lean files. Proof coverage: none; neither paper's proof is reconstructed in this corpus, and both results stand on their refereeing and the curator's credit.
Progress
The question is settled by Ford, Luca and Pomerance 2010 and sharpened by Garaev 2011. Both constructions take over sets of primes with smooth and certify as a totient value through the implication $\phi(\operatorname{rad}(m))\mid m\Rightarrow m=\phi(m\operatorname{rad}(m)/\phi(\operatorname{rad}(m)))$; Garaev's refinement combines a refined form of Konyagin's alternative route, which avoids Heath-Brown's Siegel-zero theorem, with the argument of the earlier paper.
Known Results
- Ford–Luca–Pomerance, Theorem 1: has infinitely many solutions, and for some at least integers are common values of and for all large . Their Theorem 2 gives infinitely many that are values of and of more than times each.
- Garaev, Theorem 1: for every and , at least integers are common values of and .
- Sporadic solutions such as are listed in Guy's B38 [Gu04], together with the observation that infinitely many twin primes or infinitely many Mersenne primes would each give the answer.
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.
- ford_2010_common_values_arithmetic_functions
- ford_2010_common_values_arithmetic_functions / theorem_1
- ford_2010_common_values_arithmetic_functions / theorem_2
- garaev_2011_number_common_values_arithmetic_functions_below
- garaev_2011_number_common_values_arithmetic_functions_below / theorem_1
- guy_2004_unsolved_problems_number_theory