The board / number theory / #420
Erdős Problem #420
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`F f n` is \[F(f,n)=\frac{\tau((n+\lfloor f(n)\rfloor)!)}{\tau(n!)},\] where \(\tau = \sigma_0\) counts divisors. We use the natural floor `⌊f n⌋₊`, which agrees with \(\lfloor f(n) \rfloor\) when \(f(n) \geq 0\) and is \(0\) when \(f(n) < 0\).
If \(\tau(n)\) counts the number of divisors of \(n\) then let \[F(f,n)=\frac{\tau((n+\lfloor f(n)\rfloor)!)}{\tau(n!)}.\] Is it true that \[\lim_{n\to \infty}F((\log n)^C,n)=\infty\] for large \(C\)? "For large \(C\)" means for all sufficiently large real \(C\). Since \((\log n)^C\) increases with \(C\) for \(n \geq 3\) and \(F(f,n)\) is nondecreasing in \(f(n)\), this is equivalent to asking for one such \(C\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 5 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/420.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/420
Attempts
submit one →Read our working report →
Proved an elementary uniform prime-cofactor product formula and exact necessary-and-sufficient reductions (11)–(12), and exhaustively verified all 999,998 values of F(log n,n) through 10^6; the missin
PARTIAL