Erdős Problem 393 to Erdős Problem 399
TheoremErdős Problem 393#
References: - erdosproblems.com/393 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [BeOs92] Berend, Daniel and Osgood, Charles F., On the equation \(P(x)=n!\) and a question of Erdős. J. Number Theory 42 (1992), 189-193. - [BPZ23] Bui, Hung M. and Pratt, Kyle and Zaharescu, Alexandru, Power savings for counting solutions to polynomial-factorial equations. Adv. Math. 422 (2023), Paper No. 109021, 32 pp. arXiv:2204.08423 - [Lu02] Luca, Florian, The Diophantine equation \(P(x)=n!\) and a result of M. Overholt. Glas. Mat. Ser. III 37 (2002), 269-273. - OEIS A388302: the values \(f(n)\) for \(n \geq 2\).
Quoted from FormalConjectures/ErdosProblems/393.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/393.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 5 test statements, counted here but not shown.
Erdos393.erdos_393
Open: stated without proof.
Let \(f(n)\) denote the minimal \(m\geq 1\) such that
\[n! = a_1\cdots a_t\]with \(a_1\lt \cdots \lt a_t=a_1+m\). What is the behaviour of \(f(n)\)?
We formalise the question as: does \(f(n) \to \infty\)? A result of Luca [Lu02] implies a positive answer, conditional on the \(abc\) conjecture (see
Erdos393.erdos_393.variants.luca).
theorem erdos_393 : Tendsto f atTop atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/393.lean, line 117.
Erdos393.erdos_393.variants.infinitely_often_one
Open: stated without proof.
Erdős and Graham [ErGr80, p. 76] write that they do not even know whether \(f(n) = 1\) for infinitely many \(n\), that is, whether a factorial is the product of two consecutive integers infinitely often.
theorem erdos_393.variants.infinitely_often_one :
{n : ℕ | f n = 1}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/393.lean, line 126.
Erdos393.erdos_393.variants.berend_osgood
Solved: stated here without proof.
Let \(F_m(N)\) count the number of \(n \leq N\) such that \(f(n) = m\). A theorem of Berend and Osgood [BeOs92] implies that, for each fixed \(m\), \(F_m(N) = o(N)\), that is, \(\{n : f(n) = m\}\) has natural density \(0\).
They proved that, for every \(P \in \mathbb{Z}[x]\) of degree at least \(2\), the set of \(n\) such that \(P(x) = n!\) has an integer solution has density \(0\). For \(m \geq 1\) this applies because \(f(n) = m\) gives \(n! = P(a_1)\) for one of the finitely many polynomials \(P(x) = \prod_{j \in S} (x + j)\) with \(\{0, m\} \subseteq S \subseteq \{0, \ldots, m\}\). For \(m = 0\) the set is \(\{0, 1\}\) (the junk values), so the statement is trivial.
theorem erdos_393.variants.berend_osgood (m : ℕ) :
{n : ℕ | f n = m}.HasDensity 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/393.lean, line 142.
Erdos393.erdos_393.variants.bui_pratt_zaharescu
Solved: stated here without proof.
A theorem of Bui, Pratt, and Zaharescu [BPZ23] implies that, for each fixed \(m\),
\[F_m(N) \ll_m N^{33/34},\]where \(F_m(N)\) is the number of \(n \leq N\) such that \(f(n) = m\).
They proved that, for every \(P \in \mathbb{Z}[x]\) of degree at least \(2\), the number of \(N \leq n < 2N\) such that \(P(x) = n!\) has an integer solution is \(\ll_P N^{33/34}\). Summing over the finitely many polynomials in
Erdos393.erdos_393.variants.berend_osgoodand over the dyadic ranges \([2^i, 2^{i+1})\) gives the bound for \(n \leq N\).
theorem erdos_393.variants.bui_pratt_zaharescu (m : ℕ) :
(fun N : ℕ ↦ (({n : ℕ | f n = m} ∩ Set.Iic N).ncard : ℝ)) =O[atTop]
(fun N : ℕ ↦ (N : ℝ) ^ (33 / 34 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/393.lean, line 157.
Erdos393.erdos_393.variants.luca
Solved: stated here; a Lean proof is at https://palomar-registry.org/entry.html?id=PALOMAR-2026-11-02-000011.
Luca [Lu02] proved that the \(abc\) conjecture implies that, for every \(P \in \mathbb{Z}[x]\) of degree at least \(2\), the equation \(P(x) = n!\) has only finitely many solutions. As remarked on erdosproblems.com, this implies that \(f(n) \to \infty\), conditional on the \(abc\) conjecture (
ABC.abc).
theorem erdos_393.variants.luca (habc : type_of% ABC.abc) : Tendsto f atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/393.lean, line 170.
Sources
TheoremErdős Problem 394#
References: - erdosproblems.com/394 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [ErHa78] Erdős, P. and Hall, R. R., On some unconventional problems on the divisors of integers. J. Austral. Math. Soc. Ser. A (1978), 479--485.
Quoted from FormalConjectures/ErdosProblems/394.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/394.
The file states 7 research or textbook statements: 2 open and 5 solved. It also has 2 API statements, counted here but not shown.
Erdos394.erdos_394.parts.i
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-394/Research/FirstQuestion.lean.
Is it true that \(\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log x)^c}\) for some \(c>0\)?
theorem erdos_394.parts.i :
∃ c > (0 : ℝ), (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
(t 2 n : ℝ)) ≪ (fun x ↦ x ^ 2 / (Real.log x) ^ c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 70.
Erdos394.erdos_394.parts.ii
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-394/Research/DenseHierarchyLittleO.lean.
Is it true that, for \(k\geq 2\), \(\sum_{n\leq x}t_{k+1}(n) =o\left(\sum_{n\leq x}t_k(n)\right)?\)
theorem erdos_394.parts.ii :
∀ k ≥ 2, (fun (x : ℝ) ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
(t (k + 1) n : ℝ)) =o[atTop]
(fun (x : ℝ) ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
(t k n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 80.
Erdos394.erdos_394.variants.hall_bound
Solved: stated here without proof.
In [ErGr80] they mention a conjecture of Erdős that the sum is \(o(x^2)\). This was proved by Erdős and Hall [ErHa78], who proved that in fact \(\sum_{n\leq x}t_2(n)\ll \frac{\log\log\log x}{\log\log x}x^2.\)
theorem erdos_394.variants.hall_bound :
(fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, (t 2 n : ℝ)) ≪
(fun x ↦ x ^ 2 * (Real.log (Real.log (Real.log x)) / Real.log (Real.log x)))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 93.
Erdos394.erdos_394.variants.hall_conjecture
Open: stated without proof.
Erdős and Hall conjecture that the sum is \(o(x^2/(\log x)^c)\) for any \(c\lt \log 2\).
theorem erdos_394.variants.hall_conjecture :
∀ c < Real.log 2, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
(t 2 n : ℝ)) =o[atTop]
(fun x ↦ x ^ 2 / (Real.log x) ^ c)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 102.
Erdos394.erdos_394.variants.lower_bound
Solved: stated here without proof.
Since \(t_2(p)=p-1\) for prime \(p\) it is trivial that \(\sum_{n\leq x}t_2(n)\gg \frac{x^2}{\log x}\).
theorem erdos_394.variants.lower_bound :
(fun x ↦ x ^ 2 / Real.log x) ≪
(fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, (t 2 n : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 112.
Erdos394.erdos_394.variants.factorial_gap_conjecture
Open: stated without proof.
They ask about the behaviour of \(t_{n-3}(n!)\) and also ask whether, for infinitely many \(n\), \(t_k(n!)< t_{k-1}(n!)-1\) for all \(1\leq k < n\).
theorem erdos_394.variants.factorial_gap_conjecture :
Set.Infinite { n : ℕ | ∀ k, 2 ≤ k → k < n →
t k (n !) < t (k - 1) (n !) - 1 }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 122.
Erdos394.erdos_394.variants.factorial_gap_10
Proved here.
They proved (with Selfridge) that this holds for \(n=10\).
theorem erdos_394.variants.factorial_gap_10 :
∀ (k : ℕ), 2 ≤ k → k < 10 →
t k (10 !) <
t (k - 1) (10 !) - 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/394.lean, line 132.
Sources
TheoremErdős Problem 395#
References: - erdosproblems.com/395 - [Er45] Erdős, P., On a lemma of Littlewood and Offord. Bull. Amer. Math. Soc. (1945), 898--902. - [CaCa11] Carnielli, Walter and Carolino, Pietro K., Adjusting a conjecture of Erdős. Contrib. Discrete Math. (2011), 154--159. - [HJNS24] X. He, T. Juškevičius, B. Narayanan, and S. Spiro, The Reverse Littlewood-Offord problem of Erdős. arXiv:2408.11034 (2024).
Quoted from FormalConjectures/ErdosProblems/395.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/395.
The file states 3 research or textbook statements: 3 solved.
Erdos395.erdos_395
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos395.lean#L4058.
If \(z_1,\ldots,z_n\in \mathbb{C}\) with \(\lvert z_i\rvert=1\) then is it true that the probability that
\[\lvert \epsilon_1z_1+\cdots+\epsilon_nz_n\rvert \leq \sqrt{2},\]where \(\epsilon_i\in \{-1,1\}\) uniformly at random, is \(\gg 1/n\)?
A reverse Littlewood-Offord problem. Erdős originally asked this with \(\sqrt{2}\) replaced by \(1\), but Carnielli and Carolino [CaCa11] observed that this is false, choosing \(z_1=1\) and \(z_k=i\) for \(2\leq k\leq n\), where \(n\) is even, since then the sum is at least \(\sqrt{2}\) always.
Solved in the affirmative by He, Juškevičius, Narayanan, and Spiro [HJNS24]. The bound of \(1/n\) is the best possible, as shown by taking \(z_k=1\) for \(1\leq k\leq n/2\) and \(z_k=i\) otherwise.
See also 498.
theorem erdos_395 : ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 0 < n → ∀ z : Fin n → ℂ,
(∀ i, ‖z i‖ = 1) → c / n ≤ (signedSumCount z √2 : ℝ) / 2 ^ n
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/395.lean, line 60.
Erdos395.erdos_395.variants.one
Solved: stated here without proof.
Erdős originally asked erdős_395 with \(\sqrt{2}\) replaced by \(1\), but Carnielli and Carolino [CaCa11] observed that this is false, choosing \(z_1=1\) and \(z_k=i\) for \(2\leq k\leq n\), where \(n\) is even, since then the sum is at least \(\sqrt{2}\) always.
theorem erdos_395.variants.one : ¬ ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 0 < n →
∀ z : Fin n → ℂ, (∀ i, ‖z i‖ = 1) → c / n ≤ (signedSumCount z 1 : ℝ) / 2 ^ n
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/395.lean, line 70.
Erdos395.erdos_395.variants.sharp
Solved: stated here without proof.
The bound of \(1/n\) in erdős_395 is the best possible, as shown by taking \(z_k=1\) for \(1\leq k\leq n/2\) and \(z_k=i\) otherwise.
theorem erdos_395.variants.sharp : ∃ C : ℝ, ∀ n : ℕ, 0 < n → ∃ z : Fin n → ℂ,
(∀ i, ‖z i‖ = 1) ∧ (signedSumCount z √2 : ℝ) / 2 ^ n ≤ C / n
Category research solved; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/395.lean, line 79.
Sources
TheoremErdős Problem 396#
Reference: erdosproblems.com/396
Quoted from FormalConjectures/ErdosProblems/396.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/396.
The file states 1 research or textbook statement: 1 open.
Erdos396.erdos_396
Open: stated without proof.
Is it true that for every \(k\) there exists \(n\) such that
\[\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?\]
theorem erdos_396 : ∀ k : ℕ, ∃ n : ℕ, descFactorial n (k + 1) ∣ centralBinom n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/396.lean, line 37.
Sources
TheoremErdős Problem 397#
References: - erdosproblems.com/397 - [MathOverflow] (https://mathoverflow.net/questions/138209/product-of-central-binomial-coefficients)
Quoted from FormalConjectures/ErdosProblems/397.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/397.
The file states 1 research or textbook statement: 1 solved.
Erdos397.erdos_397
Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/llllvvuu/40d68cfa9de9f43eece07ff4fdc3b0ef/raw/966750065320fe126fbe5a8a7ea50439d7519c6c/397.lean; a Lean proof is at https://github.com/XC0R/formal-conjectures/blob/3c356a50a21bcbf3543f960b0c92d7fb26228cb6/FormalConjectures/ErdosProblems/397.lean#L147.
Are there only finitely many solutions to
\[ \prod_i \binom{2m_i}{m_i}=\prod_j \binom{2n_j}{n_j} \]with the \(m_i,n_j\) distinct?
Somani, using ChatGPT, has given a negative answer. In fact, for any \(a\geq 2\), if \(c=8a^2+8a+1\), \(\binom{2a}{a}\binom{4a+4}{2a+2}\binom{2c}{c}= \binom{2a+2}{a+1}\binom{4a}{2a}\binom{2c+2}{c+1}.\) Further families of solutions are given in the comments by SharkyKesa.
This was earlier asked about in a [MathOverflow] question, in response to which Elkies also gave an alternative construction which produces solutions - at the moment it is not clear whether Elkies' argument gives infinitely many solutions (although Bloom believes that it can).
This was formalized in Lean by Wu using Aristotle.
theorem erdos_397 :
¬ {(M, N) : Finset ℕ × Finset ℕ | Disjoint M N ∧
∏ i ∈ M, centralBinom i = ∏ j ∈ N, centralBinom j}.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/397.lean, line 55.
Sources
TheoremErdős Problem 398#
References: - erdosproblems.com/398 - Wikipedia: Brocard's problem
Quoted from FormalConjectures/ErdosProblems/398.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/398.
The file states 1 research or textbook statement: 1 open.
Erdos398.erdos_398
Open: stated without proof.
Brocard's Problem Does \(n! + 1 = m^2\) have integer solutions other than \(n = 4, 5, 7\)?
theorem erdos_398 : {n | ∃ m, n ! + 1 = m ^ 2} = {4, 5, 7}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/398.lean, line 39.
Sources
TheoremErdős Problem 399#
Is it true that there are no solutions to \(n! = x^k \pm y^k\) with \(x,y,n \in \mathbb{N}\), with \(xy > 1\) and \(k > 2\)?
References: - erdosproblems.com/399 - [Br32] Breusch, Robert, Zur Verallgemeinerung des Bertrandschen Postulates, da\ss zwischen \(x\) und 2 \(x\) stets Primzahlen liegen. Math. Z. (1932), 505--526. - [ErOb37] Erdős, P. and Obláth, R., \"Über diophantische Gleichungen der Form \(n!=x^p+y^p\) und \(n!\pmd m!=x^p\). Acta Litt. ac Sci. Reg. Univ. Hung. Fr.-Jos., Sect. Sci. Math. (1937), 241-255. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [PoSh73] Pollack, Richard M. and Shapiro, Harold N., The next to last case of a factorial diophantine equation. Comm. Pure Appl. Math. (1973), 313-325.
Quoted from FormalConjectures/ErdosProblems/399.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The problem's page on erdosproblems.com: https://www.erdosproblems.com/399.
The file states 5 research or textbook statements: 5 solved.
Erdos399.erdos_399
Proved here.
Is it true that there are no solutions to
n! = x^k ± y^kwithx,y,n ∈ ℕ,x*y > 1, andk > 2?The answer is no: Jonas Barfield found the counterexample
10! = 48^4 - 36^4(equivalently,10! + 36^4 = 48^4).This is discussed in problem D2 of Guy's collection [Gu04].
This was formalized in Lean by Lu using Codex.
theorem erdos_399 :
∃ (n x y k : ℕ), 1 < x * y ∧ 2 < k ∧ (n ! = x ^ k + y ^ k ∨ n ! + y ^ k = x ^ k)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/399.lean, line 55.
Erdos399.erdos_399.variants.erdos_oblath
Solved: stated here without proof.
Erdős and Obláth [ErOb37] proved this is true when \((x,y)=1\) and \(k\neq 4\).
theorem erdos_399.variants.erdos_oblath {n x y k : ℕ} :
x.Coprime y → 1 < x * y → 2 < k → k ≠ 4 →
n ! ≠ x ^ k + y ^ k ∧ n ! + y ^ k ≠ x ^ k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/399.lean, line 61.
Erdos399.erdos_399.variants.pollack_shapiro
Solved: stated here without proof.
Pollack and Shapiro [PoSh73] proved there are no solutions to \(n!=x^4-1\).
theorem erdos_399.variants.pollack_shapiro (n x : ℕ) : n ! + 1 ≠ x ^ 4
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/399.lean, line 68.
Erdos399.erdos_399.variants.cambie
Proved here.
Cambie has also observed that considerations modulo \(8\) rule out any solutions to \(n!=x^4+y^4\) with \((x,y)=1\) and \(xy>1\).
theorem erdos_399.variants.cambie {n x y : ℕ} :
x.Coprime y → 1 < x * y → n ! ≠ x ^ 4 + y ^ 4
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/399.lean, line 76.
Erdos399.erdos_399.variants.sum_two_squares
Solved: stated here without proof.
Erdős and Obláth observed that the Bertrand-style fact (first proved by Breusch [Br32]) that, if \(q_i\) is the sequence of primes congruent to \(3\pmod{4}\) then \(q_{i+1}<2q_i\) except for \(q_1=3\), together with Fermat's theorem on the sums of two squares implies that the only solution to \(n!=x^2+y^2\) is \(6!=12^2+24^2\).
theorem erdos_399.variants.sum_two_squares :
∀ {n x y : ℕ}, 1 < x * y → n ! = x ^ 2 + y ^ 2 →
n = 6 ∧ (x = 12 ∧ y = 24 ∨ x = 24 ∧ y = 12)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/399.lean, line 130.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.