Erdős Problem 678 to Erdős Problem 698
TheoremErdős Problem 678#
References: - erdosproblems.com/678 - [Ca24] S. Cambie, Resolution of an Erdős' problem on least common multiples. arXiv:2410.09138 (2024). - [Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70. - [Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48.
Quoted from FormalConjectures/ErdosProblems/678.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/678.
The file states 3 research or textbook statements: 3 solved. It also has 4 test statements, counted here but not shown.
Erdos678.erdos_678
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos678.lean.
Write \(M(n, k)\) be the least common multiple of \(\{n+1, \dotsc, n+k\}\). Let \(k\) be sufficiently large. Are there infinitely many \(m, n\) with \(m \geq n + k\) such that
\[ M(n, k) > M(m, k + 1) \]? The answer is yes, as proved in a strong form by Cambie [Ca24]. [Ca24] S. Cambie, Resolution of an Erdős' problem on least common multiples. arXiv:2410.09138 (2024).
This was formalized in Lean by Alexeev using Aristotle, on top of the PNT+ project.
For a fixed \(k\) there are only finitely many such pairs, so "infinitely many" is read here as ranging over \(k\) as well: for every sufficiently large \(k\) at least one pair \((m, n)\) occurs. See
erdos_678.variants.infinitely_many_triplesfor the reading in which the infinitude is stated directly, anderdos_678.variants.not_infinitely_many_pairsfor why it cannot be asked of a single \(k\).
theorem erdos_678 :
∀ᶠ k in atTop, {(m, n) | n + k ≤ m ∧ lcmInterval m (k + 1) < lcmInterval n k}.Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/678.lean, line 86.
Erdos678.erdos_678.variants.infinitely_many_triples
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos678.lean.
The pairs \((m, n)\) with \(m \geq n + k\) and \(M(n, k) > M(m, k + 1)\) are infinite in number once \(k\) is allowed to vary, which is the sense in which Cambie's result answers the question.
theorem erdos_678.variants.infinitely_many_triples :
{(k, m, n) | 3 ≤ k ∧ n + k ≤ m ∧ lcmInterval m (k + 1) < lcmInterval n k}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/678.lean, line 96.
Erdos678.erdos_678.variants.not_infinitely_many_pairs
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/68da20b96673899166e94638f5a7fffeb7231d35/src/latest/ErdosProblems/Erdos678.lean.
For a fixed sufficiently large \(k\) only finitely many pairs occur: \(M(m, k + 1) \geq m + 1\) bounds \(m\) by \(M(n, k)\), and for large \(n\) the inequality reverses. So the question cannot be read as asking for infinitely many pairs at a single \(k\).
theorem erdos_678.variants.not_infinitely_many_pairs :
¬ ∀ᶠ k in atTop, {(m, n) | n + k ≤ m ∧ lcmInterval m (k + 1) < lcmInterval n k}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/678.lean, line 107.
Sources
TheoremErdős Problem 679#
References: - erdosproblems.com/679 - [Er79d] P. Erdős, Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. 33 (1979), 71–80.
Quoted from FormalConjectures/ErdosProblems/679.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/679.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos679.erdos_679.parts.i
Open: stated without proof.
Let \(\epsilon>0\) and \(\omega(n)\) count the number of distinct prime factors of \(n\). Are there infinitely many values of \(n\) such that
\[\omega(n-k) < (1+\epsilon)\frac{\log k}{\log\log k}\]for all \(k\lt n\) which are sufficiently large depending on \(\epsilon\) only?
theorem erdos_679.parts.i :
∀ ε : ℝ, 0 < ε → ∃ K : ℕ, ∃ᶠ n : ℕ in atTop,
∀ k : ℕ, K < k → k < n →
(ArithmeticFunction.cardDistinctFactors (n - k) : ℝ) <
(1 + ε) * log k / log (log k)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/679.lean, line 42.
Erdos679.erdos_679.parts.ii
Solved: stated here; a Lean proof is at https://github.com/AItoBit/erdos-679-additive-refutation/blob/4a53d358d1b7ade35d6f696f501c99b4d88c9e4c/Solution.lean.
Can one show the stronger version with
\[\omega(n-k) < \frac{\log k}{\log\log k}+O(1)\]is false?
DottedCalculator disproved this strengthening. For every additive constant \(C\) and cutoff \(K\), all sufficiently large \(n\) admit \(K\lt k\lt n\) violating the bound.
theorem erdos_679.parts.ii (C : ℝ) (K : ℕ) :
∀ᶠ n : ℕ in atTop, ∃ k < n, K < k ∧
log (k : ℝ) / log (log k) + C ≤
(ArithmeticFunction.cardDistinctFactors (n - k) : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/679.lean, line 60.
Sources
TheoremErdős Problem 680#
Reference: erdosproblems.com/680
Quoted from FormalConjectures/ErdosProblems/680.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/680.
The file states 2 research or textbook statements: 2 open.
Erdos680.erdos_680.parts.i
Open: stated without proof.
Is it true that, for all sufficiently large \(n\), there exists some \(k\) such that
\[ p(n+k)>k^2+1, \]where \(p(m)\) denotes the least prime factor of \(m\)?
theorem erdos_680.parts.i :
∀ᶠ (n : ℕ) in .atTop, ∃ k ≠ 0, (n + k).minFac > k^2 + 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/680.lean, line 41.
Erdos680.erdos_680.parts.ii
Open: stated without proof.
Can one prove this is false if we replace \(k^2+1\) by \(e^{(1+\epsilon)\sqrt{k}}+C_\epsilon\), for all \(\epsilon>0\), where \(C_\epsilon>0\) is some constant?
theorem erdos_680.parts.ii : ∀ ε > 0, ∃ C > 0,
¬ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k ≠ 0,
Nat.minFac (n + k) > exp ((1 + ε) * √k) + C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/680.lean, line 50.
Sources
TheoremErdős Problem 681#
Reference: erdosproblems.com/681
Quoted from FormalConjectures/ErdosProblems/681.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/681.
The file states 1 research or textbook statement: 1 open.
Erdos681.erdos_681
Open: stated without proof.
Erdős problem 681. Is it true that for all large \(n\) there exists \(k\) such that \(n + k\) is composite and \(p(n+k) > k^2\), where \(p(m)\) is the least prime factor of \(m\) ?
theorem erdos_681 :
∀ᶠ n in .atTop, ∃ k > 0, (n + k).Composite ∧ ∀ p, IsLPF p (n + k) → p > k ^ 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/681.lean, line 40.
Sources
TheoremErdős Problem 682#
References: - erdosproblems.com/682 - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80. - [GaTa25] A. Gafni and T. Tao, Rough numbers between consecutive primes. arXiv:2508.06463 (2025).
Quoted from FormalConjectures/ErdosProblems/682.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/682.
The file states 3 research or textbook statements: 2 solved and 1 textbook result.
Erdos682.erdos_682
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos682.lean#L5018.
Is it true that for almost all \(n\) there exists some \(m\in (p_n,p_{n+1})\) such that
\[p(m) \geq p_{n+1}-p_n,\]where \(p(m)\) denotes the least prime factor of \(m\)?
This was solved in the affirmative by Gafni and Tao [GaTa25].
This was formalized in Lean by Codex and GPT-5.6 Sol.
theorem erdos_682 :
{n | ∃ m ∈ Set.Ioo (p n) (p (n + 1)), p (n + 1) - p n ≤ m.minFac}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/682.lean, line 50.
Erdos682.erdos_682.variants.exceptional_count
Solved: stated here without proof.
Gafni and Tao [GaTa25, Theorem 1.1] proved that the number of exceptional gaps \((p_n,p_{n+1})\) with \(p_n\in [X,2X]\) is
\[\ll \frac{X}{(\log X)^2}.\]
theorem erdos_682.variants.exceptional_count :
(fun X : ℕ ↦ ({n | p n ∈ Set.Icc X (2 * X) ∧
∀ m ∈ Set.Ioo (p n) (p (n + 1)), m.minFac < p (n + 1) - p n}.ncard : ℝ)) =O[atTop]
fun X : ℕ ↦ (X : ℝ) / Real.log X ^ 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/682.lean, line 60.
Erdos682.erdos_682.variants.dickson_counterexample
Textbook result, stated without proof. A Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos682.lean#L5222.
Erdős first thought this should be true for all large \(n\), but found a (conditional) counterexample: Dickson's conjecture says there are infinitely many \(d\) such that
\[2183+30030d\textrm{ and }2201+30030d\]are both prime, and then they must necessarily be consecutive primes. These give a counterexample since \(30030=2\cdot 3 \cdot 5\cdot 7\cdot 11\cdot 13\) and every integer in \([2184,2200]\) is divisible by at least one of these primes.
This was formalized in Lean by Codex and GPT-5.6 Sol.
theorem erdos_682.variants.dickson_counterexample (d : ℕ) (h₁ : (2183 + 30030 * d).Prime)
(h₂ : (2201 + 30030 * d).Prime) : ∃ n, p n = 2183 + 30030 * d ∧ p (n + 1) = 2201 + 30030 * d ∧
∀ m ∈ Set.Ioo (p n) (p (n + 1)), m.minFac < p (n + 1) - p n
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/682.lean, line 77.
Sources
TheoremErdős Problem 683#
References: - erdosproblems.com/683 - [Er34] Erdős, Paul, A Theorem of Sylvester and Schur. J. London Math. Soc. (1934), 282--288. - [Er55d] Erdős, P., On consecutive integers. Nieuw Arch. Wisk. (3) (1955), 124--128. - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.
Quoted from FormalConjectures/ErdosProblems/683.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/683.
The file states 4 research or textbook statements: 2 open and 2 solved.
Erdos683.erdos_683
Open: stated without proof.
Let \(P(n, k)\) be the largest prime factor of \(\binom{n}{k}\). There exists \(c > 0\) such that \(P(n, k) \ge \min(n - k + 1, k^{1 + c})\) for all \(0 < k \le n/2\).
Erdős stated this for \(1 \le k \le n\) with the bound \(\min(n-k+1, k^{1+c})\) [Er79d]. The minimum is needed even for \(k \le n/2\): at \(n = 2k\) every prime factor of \(\binom{2k}{k}\) is at most \(2k\), so \(P(n, k) \ge k^{1+c}\) fails for large \(k\). The range \(k \le n/2\) is natural (cf. #961 and the discussion).
theorem erdos_683 :
∃ c > (0 : ℝ), ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 →
(P n k : ℝ) ≥ min (↑(n - k + 1) : ℝ) ((k : ℝ) ^ (1 + c))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/683.lean, line 54.
Erdos683.erdos_683.variant.sylvester_schur
Solved: stated here without proof.
Sylvester and Schur [Er34] proved that \(P(n, k) > k\) for \(k \le n/2\).
theorem erdos_683.variant.sylvester_schur :
∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k > k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/683.lean, line 63.
Erdos683.erdos_683.variant.erdos_log
Solved: stated here without proof.
Erdős [Er55d] improved this to \(P(n, k) \gg \min(n - k + 1, k \log k)\) for \(k \le n/2\). The minimum cannot be dropped: at \(n = 2k\) one has \(P(n, k) \le 2k\).
theorem erdos_683.variant.erdos_log :
∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 →
(P n k : ℝ) ≥ min (↑(n - k + 1) : ℝ) (c * k * Real.log k)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/683.lean, line 72.
Erdos683.erdos_683.variant.exp_sqrt
Open: stated without proof.
Standard heuristics suggest that \(P(n, k) > \min(n - k + 1, e^{c\sqrt{k}})\) for some constant \(c > 0\).
theorem erdos_683.variant.exp_sqrt :
∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 →
(P n k : ℝ) > min (↑(n - k + 1) : ℝ) (Real.exp (c * Real.sqrt k))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/683.lean, line 82.
Sources
TheoremErdős Problem 684#
References: - erdosproblems.com/684 - [APSSV26] Alexeev, B., Putterman, M., Sawhney, M., Sellke, M., and Valiant, G., Short proofs in combinatorics and number theory. arXiv:2603.29961 (2026), Theorem 2.1.
Quoted from FormalConjectures/ErdosProblems/684.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/684.
The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.
Erdos684.erdos_684.upper_bound
Solved: stated here; a Lean proof is at https://github.com/AItoBit/erdos-684-elementary-bounds/blob/a59cf65171b19dc7785b767d3b88ad8ef754f3eb/Solution.lean.
Let \(f(n)\) be the smallest \(0 \leq k \leq n\) for which the factor of \(\binom{n}{k}\) supported on primes at most \(k\) exceeds \(n^2\). Give bounds for \(f(n)\).
An internal OpenAI model [APSSV26] has given an elementary argument which shows \(f(n) \ll (\log n)^2\). This statement gives the nonoptimal constant \(514\). The existence formulation avoids defining the minimum for small inputs.
theorem erdos_684.upper_bound :
∀ᶠ n : ℕ in atTop, ∃ k ≤ n,
(k : ℝ) ≤ 514 * (log (n : ℝ)) ^ 2 ∧ n ^ 2 < smallPrimePart n k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/684.lean, line 52.
Erdos684.erdos_684.lower_bound
Solved: stated here; a Lean proof is at https://github.com/AItoBit/erdos-684-elementary-bounds/blob/a59cf65171b19dc7785b767d3b88ad8ef754f3eb/Erdos684/Lower.lean.
The elementary argument of an internal OpenAI model [APSSV26] constructs arbitrarily large \(n\) such that \(f(n) \geq (1/2-o(1))\log n\). The following weaker form has coefficient \(1/8\): for arbitrarily large \(n>1\), the small-prime part equals one for every \(k \leq (\log n)/8\).
theorem erdos_684.lower_bound :
∃ᶠ n : ℕ in atTop, 1 < n ∧
∀ k : ℕ, (k : ℝ) ≤ log (n : ℝ) / 8 → smallPrimePart n k = 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/684.lean, line 64.
Sources
TheoremErdős Problem 685#
References: - erdosproblems.com/685 - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.
Quoted from FormalConjectures/ErdosProblems/685.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/685.
The file states 3 research or textbook statements: 2 open and 1 textbook result. It also has 1 test statement, counted here but not shown.
Erdos685.erdos_685.parts.i
Open: stated without proof.
Let \(\epsilon > 0\) and let \(n\) be large depending on \(\epsilon\). Is it true that for all \(n^{\epsilon} < k \leq n^{1-\epsilon}\) the number of distinct prime divisors of \(\binom{n}{k}\) is
\[(1+o(1))\, k \sum_{k < p < n} \frac{1}{p}?\]The \(o(1)\) is uniform in \(k\).
theorem erdos_685.parts.i :
∀ ε > (0 : ℝ), ∀ δ > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ k : ℕ,
(n : ℝ) ^ ε < (k : ℝ) → (k : ℝ) ≤ (n : ℝ) ^ (1 - ε) →
|(ω (n.choose k) : ℝ) - (k : ℝ) * primeRecipSum k n| ≤
δ * ((k : ℝ) * primeRecipSum k n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/685.lean, line 54.
Erdos685.erdos_685.parts.ii
Open: stated without proof.
Is it true that, for some constant \(c > 0\), the number of distinct prime divisors of \(\binom{n}{k}\) is
\[(1+o(1))\, k \sum_{k < p < n} \frac{1}{p}\]even for all \((\log n)^c \leq k \leq n^{1-\epsilon}\)?
Here \(\epsilon > 0\) is as in the first question, and the \(o(1)\) is uniform in \(k\).
theorem erdos_685.parts.ii :
∃ c > (0 : ℝ), ∀ ε > (0 : ℝ), ∀ δ > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ k : ℕ,
Real.log (n : ℝ) ^ c ≤ (k : ℝ) → (k : ℝ) ≤ (n : ℝ) ^ (1 - ε) →
|(ω (n.choose k) : ℝ) - (k : ℝ) * primeRecipSum k n| ≤
δ * ((k : ℝ) * primeRecipSum k n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/685.lean, line 70.
Erdos685.erdos_685.variants.trivial_lower_bound
Textbook result, proved here.
For \(1 \leq k \leq n - 1\) the number of distinct prime divisors of \(\binom{n}{k}\) satisfies
\[\omega\left(\binom{n}{k}\right) \geq \frac{\log \binom{n}{k}}{\log n}.\]
theorem erdos_685.variants.trivial_lower_bound :
∀ n k : ℕ, 0 < k → k < n →
Real.log (n.choose k : ℝ) / Real.log (n : ℝ) ≤ (ω (n.choose k) : ℝ)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/685.lean, line 82.
Sources
TheoremErdős Problem 686#
References: - erdosproblems.com/686 - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.
Quoted from FormalConjectures/ErdosProblems/686.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/686.
The file states 8 research or textbook statements: 4 open and 4 solved.
Erdos686.erdos_686
Open: stated without proof.
Can every integer \(N≥2\) be written as
\[N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686 :
∀ N ≥ (2 : ℕ), ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 39.
Erdos686.erdos_686.variants.square
Open: stated without proof.
Can every square \(N≥2\) be written as
\[N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686.variants.square :
∀ N ≥ (2 : ℕ), (IsSquare N) → ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 50.
Erdos686.erdos_686.variants.four
Open: stated without proof.
Can \(4\) be written as
\[4=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686.variants.four :
∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(4 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 61.
Erdos686.erdos_686.variants.four_two
Proved here.
The number \(4\) cannot be written as
\[4=\frac{\prod_{1\leq i\leq 2}(m+i)}{\prod_{1\leq i\leq 2}(n+i)}\]for \(m≥n+2\)!
theorem erdos_686.variants.four_two :
¬ ∃ᵉ (n : ℕ) (m ≥ n + 2),
(4 : ℚ) = (∏ i ∈ Finset.Icc 1 2, (m + i)) / (∏ i ∈ Finset.Icc 1 2, (n + i))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 72.
Erdos686.erdos_686.variants.four_three
Solved: stated here without proof.
The number \(4\) cannot be written as
\[4=\frac{\prod_{1\leq i\leq 3}(m+i)}{\prod_{1\leq i\leq 3}(n+i)}\]for \(m≥n+3\)!
theorem erdos_686.variants.four_three :
¬ ∃ᵉ (n : ℕ) (m ≥ n + 3),
(4 : ℚ) = (∏ i ∈ Finset.Icc 1 3, (m + i)) / (∏ i ∈ Finset.Icc 1 3, (n + i))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 93.
Erdos686.erdos_686.variants.nine
Proved here.
Can \(9\) be written as
\[9=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686.variants.nine :
∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(9 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 104.
Erdos686.erdos_686.variants.twenty_five
Open: stated without proof.
Can \(25\) be written as
\[25=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686.variants.twenty_five :
∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(25 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 117.
Erdos686.erdos_686.variants.non_square
Proved here.
Can every non-square \(N≥2\) be written as
\[N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}\]for some \(k≥2\) and \(m≥n+k\)?
theorem erdos_686.variants.non_square :
∀ N ≥ (2 : ℕ), (¬ IsSquare N) → ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/686.lean, line 128.
Sources
TheoremErdős Problem 687#
References: - erdosproblems.com/687 - Ben Green's Open Problem 46: the same question; see
Green46inFormalConjectures.GreensOpenProblems.«46». - OEIS A058989: the values \(Y(p_n)\), where \(p_n\) is the \(n\)-th prime. - OEIS A048670: Jacobsthal's function of \(\prod_{p \leq p_n} p\), which is \(Y(p_n) + 1\). - [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. 33 (1979), 71-80. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89-115. - [Er96b] Erdős, Paul, Some problems I presented or planned to present in my short talk. Analytic number theory, Vol. 1 (Allerton Park, IL, 1995), Progr. Math. 138 (1996), 333-335. - [Iw78] Iwaniec, Henryk, On the problem of Jacobsthal. Demonstratio Math. 11 (1978), 225-232. doi:10.1515/dema-1978-0121 - [MaPo90] Maier, Helmut and Pomerance, Carl, Unusually large gaps between consecutive primes. Trans. Amer. Math. Soc. 322 (1990), 201-237. - [FGKMT18] Ford, Kevin and Green, Ben and Konyagin, Sergei and Maynard, James and Tao, Terence, Long gaps between primes. J. Amer. Math. Soc. 31 (2018), 65-105. arXiv:1412.5029 - [OAI26a] OpenAI, A quadratic bound for Jacobsthal's function. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/687.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/687.
The file states 6 research or textbook statements: 3 open and 3 solved. It also has 4 test statements, counted here but not shown.
Erdos687.erdos_687.parts.i
Open: stated without proof.
Let \(Y(x)\) be the maximal \(y\) such that there exists a choice of congruence classes \(a_p\) for all primes \(p\leq x\) such that every integer in \([1,y]\) is congruent to at least one of the \(a_p\pmod{p}\). Give good estimates for \(Y(x)\).
We formalise this as determining \(Y(x)\) up to constant factors.
theorem erdos_687.parts.i :
(fun x : ℕ ↦ (Y x : ℝ)) =Θ[atTop] erdos_687.parts.i.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 164.
Erdos687.erdos_687.parts.ii
Solved: stated here; a Lean proof is at https://github.com/30k30/scholia/blob/b072c89c3edac06521868e32cc15b2bc91bd8533/erdos-687/glue/JacobsthalTo687.lean#L325.
In particular, can one prove that \(Y(x)=o(x^2)\)?
Yes: an internal OpenAI model proved \(h(k) \ll k^2\) for Jacobsthal's function \(h\) [OAI26a] (see
Erdos970.erdos_970). Since \(Y(x) + 1\) is Jacobsthal's function of \(\prod_{p \leq x} p\), which has \(\pi(x) \ll x/\log x\) prime factors, this gives \(Y(x) \ll x^2/(\log x)^2\). The linked Lean proof is by 30k30, from the bound of [OAI26a].
theorem erdos_687.parts.ii :
(fun x : ℕ ↦ (Y x : ℝ)) =o[atTop] (fun x : ℕ ↦ (x : ℝ) ^ 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 179.
Erdos687.erdos_687.parts.iii
Open: stated without proof.
Or, even stronger, can one prove that \(Y(x)\ll x^{1+o(1)}\)?
We read \(Y(x)\ll x^{1+o(1)}\) as \(Y(x) = O(x^{1+\varepsilon})\) for every fixed \(\varepsilon > 0\).
theorem erdos_687.parts.iii :
∀ ε > (0 : ℝ), (fun x : ℕ ↦ (Y x : ℝ)) =O[atTop] (fun x : ℕ ↦ (x : ℝ) ^ (1 + ε))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 190.
Erdos687.erdos_687.variants.iwaniec
Solved: stated here without proof.
Iwaniec's upper bound for Jacobsthal's function [Iw78] gives \(Y(x) \ll x^2\).
theorem erdos_687.variants.iwaniec :
(fun x : ℕ ↦ (Y x : ℝ)) =O[atTop] (fun x : ℕ ↦ (x : ℝ) ^ 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 198.
Erdos687.erdos_687.variants.fgkmt
Solved: stated here without proof.
Ford, Green, Konyagin, Maynard and Tao [FGKMT18] proved
\[Y(x) \gg \frac{x \log x \log\log\log x}{\log\log x}.\]
theorem erdos_687.variants.fgkmt :
(fun x : ℕ ↦ (x : ℝ) * Real.log x * Real.log (Real.log (Real.log x)) /
Real.log (Real.log x)) =O[atTop] (fun x : ℕ ↦ (Y x : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 207.
Erdos687.erdos_687.variants.maier_pomerance
Open: stated without proof.
Maier and Pomerance [MaPo90] conjectured that \(Y(x) \ll x(\log x)^{2+o(1)}\) (in this form it is stated in [FGKMT18]).
We read this as \(Y(x) = O(x(\log x)^{2+\varepsilon})\) for every fixed \(\varepsilon > 0\).
theorem erdos_687.variants.maier_pomerance :
∀ ε > (0 : ℝ), (fun x : ℕ ↦ (Y x : ℝ)) =O[atTop]
(fun x : ℕ ↦ (x : ℝ) * Real.log x ^ (2 + ε))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/687.lean, line 219.
Sources
TheoremErdős Problem 688#
Reference: - erdosproblems.com/688 - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
Quoted from FormalConjectures/ErdosProblems/688.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/688.
The file states 3 research or textbook statements: 2 open and 1 solved.
Erdos688.erdos_688.parts.i
Open: stated without proof.
Estimate \(\epsilon_n\).
theorem erdos_688.parts.i :
epsilonFunction =Θ[atTop] erdos_688.parts.i.answer
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/688.lean, line 51.
Erdos688.erdos_688.parts.ii
Open: stated without proof.
In particular, is it true that \(\epsilon_n = o(1)\)?
theorem erdos_688.parts.ii :
epsilonFunction =o[atTop] (fun (n : ℕ) ↦ (1 : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/688.lean, line 59.
Erdos688.erdos_688.variants.lglglg_over_lglg_is_big_o
Solved: stated here without proof.
Erdős claims in [Er80] (p. 106) that it is not difficult to prove \(\epsilon_n \gg \frac{\log\log\log n}{\log\log n}\).
theorem erdos_688.variants.lglglg_over_lglg_is_big_o :
(fun (n : ℕ) ↦ (log (log (log (n : ℝ)))) / (log (log (n : ℝ))))
=O[atTop] epsilonFunction
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/688.lean, line 68.
Sources
TheoremErdős Problem 689#
References: - erdosproblems.com/689 - Ben Green's Open Problem 45 - [Ch26] Chojecki, P., A greedy matching proof of Erdős's two-fold residue-class problem. ulam.ai/research/erdos689.pdf (April 2026). - PALOMAR-2026-09-20-000002
Quoted from FormalConjectures/ErdosProblems/689.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/689.
The file states 1 research or textbook statement: 1 solved.
Erdos689.erdos_689
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/54f272582dd71321ab9d458663d675edd3d0a463/erdos-689/Solution.lean#L18.
Let
nbe sufficiently large. Is there some choice of congruence classa_pfor all primes2 ≤ p ≤ nsuch that every integer in[1,n]satisfies at least two of the congruences≡ a_p (mod p)?Yes: this follows from the greedy-matching reduction of Chojecki [Ch26] combined with an unconditional Fourier-analytic proof of the required three-prime counting estimate.
theorem erdos_689 :
∀ᶠ n in .atTop, ∃ a : ℕ → ℕ, ∀ m ∈ Finset.Icc 1 n,
2 ≤ (Finset.Icc 1 n |>.filter fun p => p.Prime ∧ a p ≡ m [MOD p]).card
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/689.lean, line 44.
Sources
TheoremErdős Problem 690#
References: - erdosproblems.com/690 - [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82. - [Ca25] S. Cambie, Resolution of Erdős' problems about unimodularity. arXiv:2501.10333 (2025). - [WC26] S. Wang and D. Crapis, A Complete Answer to Erdős Problem 690. arXiv:2605.08542 (2026).
Quoted from FormalConjectures/ErdosProblems/690.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/690.
The file states 5 research or textbook statements: 5 solved.
Erdos690.erdos_690
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos690.lean#L2162.
Let \(d_k(p)\) be the density of those integers whose \(k\)th smallest prime factor is \(p\) (i.e. if \(p_1\lt p_2\lt \cdots\) are the primes dividing \(n\) then \(p_k=p\)).
For fixed \(k\geq 1\) is \(d_k(p)\) unimodular in \(p\)? That is, it first increases in \(p\) until its maximum then decreases.
The answer is no in general: Cambie [Ca25] has shown that \(d_k(p)\) is unimodular for \(1\leq k\leq 3\) and is not unimodular for \(4\leq k\leq 20\).
The densities \(d_k(p)\) exist (see
erdos_690.variants.hasDensity), so the statement quantifies over any functiondrecording them.
theorem erdos_690 :
¬ ∀ k ≥ 1, ∀ d : ℕ → ℝ,
(∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) → IsUnimodalOnPrimes d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/690.lean, line 63.
Erdos690.erdos_690.variants.hasDensity
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos690.lean#L2162.
For every \(k\geq 1\) and prime \(p\), the set of integers whose \(k\)th smallest prime factor is \(p\) has a natural density.
theorem erdos_690.variants.hasDensity (k p : ℕ) (hk : 1 ≤ k) (hp : p.Prime) :
∃ δ : ℝ, (kthPrimeFactorSet k p).HasDensity δ
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/690.lean, line 73.
Erdos690.erdos_690.variants.cambie_unimodal
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos690.lean#L2162.
Cambie [Ca25] has shown that \(d_k(p)\) is unimodular for \(1\leq k\leq 3\).
theorem erdos_690.variants.cambie_unimodal (k : ℕ) (hk : 1 ≤ k) (hk' : k ≤ 3)
(d : ℕ → ℝ) (hd : ∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) :
IsUnimodalOnPrimes d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/690.lean, line 81.
Erdos690.erdos_690.variants.cambie_not_unimodal
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos690.lean#L2162.
Cambie [Ca25] has shown that \(d_k(p)\) is not unimodular for \(4\leq k\leq 20\).
theorem erdos_690.variants.cambie_not_unimodal (k : ℕ) (hk : 4 ≤ k) (hk' : k ≤ 20)
(d : ℕ → ℝ) (hd : ∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) :
¬ IsUnimodalOnPrimes d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/690.lean, line 90.
Erdos690.erdos_690.variants.large_k
Solved: stated here without proof.
Is \(d_k(p)\) unimodular for any \(k\geq 21\)?
The answer is no: \(d_k(p)\) is not unimodal for any \(k \geq 4\) [WC26] (arXiv preprint).
theorem erdos_690.variants.large_k :
¬ ∃ k ≥ 21, ∀ d : ℕ → ℝ,
(∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) → IsUnimodalOnPrimes d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/690.lean, line 99.
Sources
TheoremErdős Problem 691#
Reference: erdosproblems.com/691
Quoted from FormalConjectures/ErdosProblems/691.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/691.
The file states 1 research or textbook statement: 1 open.
Erdos691.erdos_691
Open: stated without proof.
Given \(A \subseteq \mathbb{N}\), let \(M_A = \{n \geq 1 : a \mid n \text{ for some } a \in A\}\). Find a necessary and sufficient condition on \(A\) for \(M_A\) to have density \(1\).
theorem erdos_691 :
erdos_691.answer = fun A ↦ (multiples A).HasDensity 1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/691.lean, line 41.
Sources
TheoremErdős Problem 692#
References: - erdosproblems.com/692 - [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73-82. - [Ob1] Erdős, P., Oberwolfach Mathematical Problems, Volume 1. Mathematisches Forschungsinstitut Oberwolfach (Various). - [Fo08] Ford, Kevin, The distribution of integers with a divisor in a given interval. Ann. of Math. (2) (2008), 367-433. - [Ca25] Cambie, S., Resolution of Erdős' problems about unimodularity. arXiv:2501.10333 (2025).
Quoted from FormalConjectures/ErdosProblems/692.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/692.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos692.erdos_692.parts.i
Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/pitmonticone/96516af9100a37a1da81908dc0b0410c/raw/a1d6ca7f3835c58b257e5e715c8fdf3a224e1bd0/Erdos692.lean.
Let \(\delta_1(n,m)\) be the density of the set of integers with exactly one divisor in \((n,m)\). Is \(\delta_1(n,m)\) unimodular for \(m>n+1\) (i.e. increases until some \(m\) then decreases thereafter)?
Cambie has calculated that unimodularity fails even for \(n=2\) and \(n=3\).
This was formalized in Lean by Monticone using Aristotle.
theorem erdos_692.parts.i :
¬ ∀ δ : ℕ → ℕ → ℝ, (∀ a b, IsDelta₁ a b (δ a b)) → ∀ n, UnimodularOn (δ n) (n + 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/692.lean, line 72.
Erdos692.erdos_692.parts.ii
Open: stated without proof.
Let \(\delta_1(n,m)\) be the density of the set of integers with exactly one divisor in \((n,m)\). For fixed \(n\), where does \(\delta_1(n,m)\) achieve its maximum?
theorem erdos_692.parts.ii (n : ℕ) :
∀ δ : ℕ → ℕ → ℝ, (∀ a b, IsDelta₁ a b (δ a b)) →
IsGreatest (δ n '' Set.Ioi (n + 1)) (δ n erdos_692.parts.ii.answer)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/692.lean, line 83.
Erdos692.erdos_692.variants.erdos_upper_bound
Solved: stated here without proof.
Erdős proved that
\[\delta_1(n,m) \ll \frac{1}{(\log n)^c}\]for all \(m\), for some constant \(c>0\).
theorem erdos_692.variants.erdos_upper_bound :
∀ δ : ℕ → ℕ → ℝ, (∀ a b, IsDelta₁ a b (δ a b)) →
∃ c > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ m, δ n m ≤ C / Real.log n ^ c
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/692.lean, line 94.
Erdos692.erdos_692.variants.cambie_three
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/b8e7531a14cbe5c18ea1ae2e9e85b811bc3c7a46/erdos-692/Solution.lean#L26.
Cambie has calculated that unimodularity fails even for \(n=2\) and \(n=3\). For example,
\[\delta_1(3,6)= 0.35\quad \delta_1(3,7)\approx 0.33\quad \delta_1(3,8)\approx 0.3619.\]
theorem erdos_692.variants.cambie_three :
∀ δ : ℕ → ℕ → ℝ, (∀ a b, IsDelta₁ a b (δ a b)) →
δ 3 7 < δ 3 6 ∧ δ 3 7 < δ 3 8
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/692.lean, line 106.
Erdos692.erdos_692.variants.cambie_local_maxima
Solved: stated here without proof.
Cambie [Ca25] has shown that, for fixed \(n\), the sequence \(\delta_1(n,m)\) has superpolynomially many local maxima \(m\). A local maximum is a maximal run of equal values of the sequence that is strictly larger than the values just before and just after the run.
theorem erdos_692.variants.cambie_local_maxima (k : ℕ) :
∀ δ : ℕ → ℕ → ℝ, (∀ a b, IsDelta₁ a b (δ a b)) →
∀ᶠ n : ℕ in atTop, (n : ℕ∞) ^ k ≤ (localMaxima (δ n) (n + 1)).encard
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/692.lean, line 117.
Sources
TheoremErdős Problem 694#
Reference: erdosproblems.com/694
Quoted from FormalConjectures/ErdosProblems/694.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/694.
The file states 3 research or textbook statements: 1 open and 2 solved.
Erdos694.erdos_694
Solved: stated here without proof.
Let \(f_\max(n)\) be the largest \(m\) such that \(\phi(m) = n\), and \(f_\min(n)\) be the smallest such \(m\), where \(\phi\) is Euler's totient function. Investigate
\[ \max_{n\leq x}\frac{f_\max(n)}{f_\min(n)}. \]GPT-5.5 Pro (prompted by Price) has proved (see also the comments for a summary) that
\[ \max_{n\leq x}\frac{f_{\max}(n)}{f_{\min}(n)}=(e^\gamma+o(1))\log\log x. \]A Lean formalisation of the reduction exists, conditional on Mertens' product theorem and Linnik's theorem; see the formal proof.
The extrema are only required on nonempty fibres of the totient (values such as \(3\) have no preimage), and the identity is asked for sufficiently large \(x\): at \(x = 1\) the maximum is \(f_\max(1) / f_\min(1) = 2\) while \(\log \log 1 = 0\).
theorem erdos_694 : ∀ᵉ (fmax : ℕ → ℕ) (fmin : ℕ → ℕ),
(∀ n, (∃ m, Nat.totient m = n) → IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) →
(∀ n, (∃ m, Nat.totient m = n) → IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) →
∃ o : ℕ → ℝ, Tendsto o atTop (𝓝 0) ∧
∀ᶠ x : ℕ in atTop,
sSup { (fmax n : ℝ) / fmin n | (n : ℕ) (_ : n ≤ x) (_ : ∃ m, Nat.totient m = n) } =
(exp eulerMascheroniConstant + o x) * log (log (x : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/694.lean, line 54.
Erdos694.erdos_694.variants.carmichael
Open: stated without proof.
Carmichael has asked whether there is an integer \(n\) for which \(\phi(m) = n\) has exactly one solution, that is \(\frac{f_\max(n)}{f_\min(n)} = 1\).
theorem erdos_694.variants.carmichael :
∃ n > 0, ∃! m, Nat.totient m = n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/694.lean, line 68.
Erdos694.erdos_694.variants.inf_unique
Solved: stated here without proof.
Erdős has proved that if there exists an integer \(n\) for which \(\phi(m) = n\) has exactly one solution, then there must be infinitely many such \(n\).
theorem erdos_694.variants.inf_unique (h : ∃ n > 0, ∃! m, Nat.totient m = n) :
{ n | ∃! m, Nat.totient m = n }.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/694.lean, line 77.
Sources
TheoremErdős Problem 695#
Reference: erdosproblems.com/695
Quoted from FormalConjectures/ErdosProblems/695.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/695.
The file states 2 research or textbook statements: 2 open.
Erdos695.erdos_695
Open: stated without proof.
Let \(q_1 < q_2 < \cdots\) be a sequence of primes such that \(q_{i + 1} \equiv 1 \pmod{q_i}\). Is it true that
\[ \lim_{k \to \infty} q_k^{1/k} = \infty? \]
theorem erdos_695 :
∀ {q : ℕ → ℕ},
StrictMono q →
(∀ i, (q i).Prime) →
(∀ i, q (i + 1) % q i = 1) →
Tendsto (fun k => (q k : ℝ) ^ (1 / k : ℝ)) atTop atTop
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/695.lean, line 39.
Erdos695.erdos_695.variants.upperBound
Open: stated without proof.
Is there a sequence of primes \(q_1 < q_2 < \cdots\) such that \(q_{i + 1} \equiv 1 \pmod{q_i}\) and
\[ q(k) \leq \exp(k (\log k)^{1 + o(1)})? \]
theorem erdos_695.variants.upperBound :
∃ q : ℕ → ℕ,
StrictMono q ∧
(∀ i, (q i).Prime) ∧
(∀ i, q (i + 1) % q i = 1) ∧
∃ o : ℕ → ℝ,
(o =o[atTop] (1 : ℕ → ℝ)) ∧
-- We use `(k + 1)` here as the informal statement is 1-indexed.
∀ k, q k ≤ exp ((k + 1) * log (k + 1) ^ (1 + o k))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/695.lean, line 54.
Sources
TheoremErdős Problem 696#
References: * erdosproblems.com/696 * Lean proof, assuming the Siegel-Walfisz theorem, the Brun-Titchmarsh inequality, and Mertens' theorem as custom axioms.
Quoted from FormalConjectures/ErdosProblems/696.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/696.
The file states 1 research or textbook statement: 1 solved. It also has 1 test statement, counted here but not shown.
Erdos696.erdos_696
Solved: stated here without proof.
Is it true that \(H(n)/h(n)\to \infty\) for almost all \(n\)?
Formalised as: for every threshold \(M\), the set of \(n\) with \(h(n) > 0\) and \(H(n)/h(n) > M\) has natural density \(1\). This is false: in fact, \(H(n)/h(n) = 2 + o(1)\) for almost all \(n\).
theorem erdos_696 :
¬ ∀ M : ℝ,
{n : ℕ | (h n : ℝ) > 0 ∧ (H n : ℝ) / (h n : ℝ) > M}.HasDensity 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/696.lean, line 78.
Sources
TheoremErdős Problem 697#
Reference: - erdosproblems.com/697 - [Ha92] Hall, R. R., On some conjectures of Erdős in Astérisque. I. J. Number Theory (1992), 313--319.
Quoted from FormalConjectures/ErdosProblems/697.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/697.
The file states 4 research or textbook statements: 4 solved.
Erdos697.density_exists
Solved: stated here without proof.
For each \(m\) and \(\alpha\), the density of the set of integers which are divisible by some \(d \equiv 1 \pmod{m}\) with \(1 < d < \exp (m ^ \alpha)\) exists.
theorem density_exists (m : ℕ) (α : ℝ) : ∃ δ, HasDensity
{n : ℕ | ∃ d, d ≡ 1 [MOD m] ∧ (d : ℝ) ∈ Set.Ioo 1 (exp (m ^ α)) ∧ d ∣ n} δ
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/697.lean, line 39.
Erdos697.erdos_697.variants.delta_lt
Solved: stated here without proof.
\(\delta < \frac{m ^ \alpha + 1}{m}\). This shows that \(lim_{m\rightarrow\infty} \delta (m, \alpha) = 0\) for \(\alpha < 1\). At \(m = 0\), both sides are 0, so the strict bound requires \(m > 0\).
TODO: prove this theorem.
TODO: prove this theorem.
theorem erdos_697.variants.delta_lt (m : ℕ) (α : ℝ) (hm : 0 < m) : δ m α < (m ^ α + 1) / m
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/697.lean, line 52.
Erdos697.erdos_697.parts.i
Solved: stated here without proof.
Let \(\beta = \frac{1}{\log 2}\). Then \(lim_{m\rightarrow\infty} \delta (m, \alpha) = 0\) if \(\alpha < \beta\). This is proved in [Ha92].
theorem erdos_697.parts.i {α : ℝ} (hα : α < 1 / log (2 : ℝ)) : Tendsto (δ · α) atTop (𝓝 0)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/697.lean, line 58.
Erdos697.erdos_697.parts.ii
Solved: stated here without proof.
\(lim_{m\rightarrow\infty} \delta (m, \alpha) = 1\) if \(\beta < \alpha\). This is proved in [Ha92].
theorem erdos_697.parts.ii {α : ℝ} (hα : 1 / log (2 : ℝ) < α) : Tendsto (δ · α) atTop (𝓝 1)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/697.lean, line 64.
Sources
TheoremErdős Problem 698#
References: - erdosproblems.com/698 - [ErSz78] Erdős, P. and Szekeres, G., Some number theoretic problems on binomial coefficients. Austral. Math. Soc. Gaz. (1978), 97-99. - [Be11] Bergman, George M., On common divisors of multinomial coefficients. Bull. Aust. Math. Soc. (2011), 138--157.
Quoted from FormalConjectures/ErdosProblems/698.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/698.
The file states 4 research or textbook statements: 4 solved.
Erdos698.erdos_698
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos698.lean#L452.
Is there some \(h(n)\to \infty\) such that for all \(2\leq i\lt j\leq n/2\)
\[\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \geq h(n)?\]This was resolved by Bergman [Be11], who proved that for any \(2\leq i\lt j\leq n/2\)
\[\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \gg n^{1/2}\frac{2^i}{i^{3/2}},\]where the implied constant is absolute.
The linked formal proof (van Doorn and Aristotle, see
erdos_698.variants.bergman) gives the explicit bound \(\gcd > \frac{2^i \sqrt n}{4 i \sqrt{i - 1}}\), so \(h(n) = \lfloor \sqrt n / 4 \rfloor\) works since \(i \sqrt{i - 1} \le 2^i\) for \(i \ge 2\).
theorem erdos_698 :
∃ h : ℕ → ℕ, Tendsto h atTop atTop ∧
∀ n i j : ℕ, 2 ≤ i → i < j → j ≤ n / 2 →
h n ≤ Nat.gcd (n.choose i) (n.choose j)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/698.lean, line 52.
Erdos698.erdos_698.variants.erdos_szekeres
Proved here.
A problem of Erdős and Szekeres, who observed that
\[\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \geq \frac{\binom{n}{i}}{\binom{j}{i}} \geq 2^i\](in particular the greatest common divisor is always \(>1\)).
theorem erdos_698.variants.erdos_szekeres (n i j : ℕ) (hi : 1 ≤ i) (hij : i < j)
(hj : j ≤ n / 2) :
(n.choose i : ℝ) / (j.choose i : ℝ) ≤ (Nat.gcd (n.choose i) (n.choose j) : ℝ) ∧
(2 : ℝ) ^ i ≤ (n.choose i : ℝ) / (j.choose i : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/698.lean, line 65.
Erdos698.erdos_698.variants.erdos_szekeres_sharp
Proved here.
This inequality is sharp for \(i=1\), \(j=p\), and \(n=2p\).
theorem erdos_698.variants.erdos_szekeres_sharp (p : ℕ) (hp : p.Prime) (hp2 : 2 < p) :
(Nat.gcd ((2 * p).choose 1) ((2 * p).choose p) : ℝ) =
((2 * p).choose 1 : ℝ) / (p.choose 1 : ℝ) ∧
((2 * p).choose 1 : ℝ) / (p.choose 1 : ℝ) = (2 : ℝ) ^ 1
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/698.lean, line 114.
Erdos698.erdos_698.variants.bergman
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos698.lean.
This was resolved by Bergman [Be11], who proved that for any \(2\leq i\lt j\leq n/2\)
\[\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \gg n^{1/2}\frac{2^i}{i^{3/2}},\]where the implied constant is absolute.
theorem erdos_698.variants.bergman :
∃ c : ℝ, 0 < c ∧ ∀ n i j : ℕ, 2 ≤ i → i < j → j ≤ n / 2 →
c * (Real.sqrt (n : ℝ) * (2 : ℝ) ^ i / ((i : ℝ) * Real.sqrt (i : ℝ))) ≤
(Nat.gcd (n.choose i) (n.choose j) : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/698.lean, line 164.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.