Erdős Problem 1 to Erdős Problem 21
TheoremErdős Problem 1#
Reference: erdosproblems.com/1
Quoted from FormalConjectures/ErdosProblems/1.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/1.
The file states 9 research or textbook statements: 6 solved and 3 textbook results.
Erdos1.erdos_1
Solved: stated here; a Lean proof is at https://github.com/tadamcz/erdos1/blob/0e395153306f34b3829d118b85bdd704136f2843/Erdos1/Resolutions/Erdos1_219usd_38h.lean#L2419.
If \(A\subseteq\{1, ..., N\}\) with \(|A| = n\) is such that the subset sums \(\sum_{a\in S}a\) are distinct for all \(S\subseteq A\) then
\[ N \gg 2 ^ n. \]This conjecture is false. A machine-checked disproof constructs sum-distinct sets for which \(N / 2^n\) tends to zero.
theorem erdos_1 : ¬ ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ) (_ : IsSumDistinctSet A N),
N ≠ 0 → C * 2 ^ A.card < N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 54.
Erdos1.erdos_1.variants.weaker
Textbook result, proved here.
The trivial lower bound is \(N \gg 2^n / n\).
theorem erdos_1.variants.weaker : ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ)
(_ : IsSumDistinctSet A N), N ≠ 0 → C * 2 ^ A.card / A.card < N
Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 62.
Erdos1.erdos_1.variants.lb
Solved: stated here without proof.
Erdős and Moser [Er56] proved
\[ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. \][Er56] Erdős, P., Problems and results in additive number theory. Colloque sur la Th\'{E}orie des Nombres, Bruxelles, 1955 (1956), 127-137.
theorem erdos_1.variants.lb : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N),
(1 / 4 - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 91.
Erdos1.erdos_1.variants.lb_strong
Solved: stated here; a Lean proof is at https://github.com/MyTH-zyxeon/formal-conjectures/blob/362eed1a8864d142ae65f51af7981a7c7530956e/FormalConjectures/Scratch/HarperCompression.lean#L2174.
A number of improvements of the constant \(\frac{1}{4}\) have been given, with the current record \(\sqrt{2 / \pi}\) first provided in unpublished work of Elkies and Gleason.
theorem erdos_1.variants.lb_strong : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N),
(√(2 / π) - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 104.
Erdos1.erdos_1.variants.real
Proved here.
A generalisation of the problem to sets \(A \subseteq (0, N]\) of real numbers, such that the subset sums all differ by at least \(1\) is proposed in [Er73] and [ErGr80].
The positive statement is false: every natural-number counterexample to
erdos_1embeds into \(\mathbb{R}\), and distinct integer subset sums differ by at least one.[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
theorem erdos_1.variants.real : ¬ ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℝ)
(_ : IsSumDistinctRealSet A N), N ≠ 0 → C * 2 ^ A.card < N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 129.
Erdos1.erdos_1.variants.least_N_3
Textbook result, proved here.
The minimal value of \(N\) such that there exists a sum-distinct set with three elements is \(4\).
https://oeis.org/A276661
theorem erdos_1.variants.least_N_3 :
IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4
Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 230.
Erdos1.erdos_1.variants.least_N_4
Textbook result, proved here.
The minimal value of \(N\) such that there exists a sum-distinct set with four elements is \(7\).
https://oeis.org/A276661
theorem erdos_1.variants.least_N_4 :
IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 4 } 7
Category textbook; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 261.
Erdos1.erdos_1.variants.least_N_5
Proved here.
The minimal value of \(N\) such that there exists a sum-distinct set with five elements is \(13\).
https://oeis.org/A276661
theorem erdos_1.variants.least_N_5 :
IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 5 } 13
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 282.
Erdos1.erdos_1.variants.least_N_9
Solved: stated here without proof.
The minimal value of \(N\) such that there exists a sum-distinct set with nine elements is \(161\).
https://oeis.org/A276661
theorem erdos_1.variants.least_N_9 :
IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 9 } 161
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1.lean, line 303.
Sources
TheoremErdős Problem 2#
References: - erdosproblems.com/2 - [Ho15] Hough, B., Solution of the minimum modulus problem for covering systems. Ann. of Math. (2) 181 (2015), 361-382. - [BBMST22] Balister, P., Bollobás, B., Morris, R., Sahasrabudhe, J. and Tiba, M., On the Erdős Covering Problem: the density of the uncovered set. Invent. Math. 228 (2022), 377-414. - PALOMAR-2026-10-05-000002
Erdős asked whether the smallest modulus in a distinct covering system can be arbitrarily large. Hough [Ho15] proved that the answer is no, and Balister, Bollobás, Morris, Sahasrabudhe, and Tiba [BBMST22] later gave a simpler proof with an improved explicit upper bound.
Quoted from FormalConjectures/ErdosProblems/2.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/2.
The file states 1 research or textbook statement: 1 solved.
Erdos2.erdos_2
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/7caa4144741e10f96cf79d6f7313a0efd9a18b67/erdos-2/Solution.lean#L44.
Can the smallest modulus of a covering system be arbitrarily large?
This problem has a negative answer: there is a universal bound on the least modulus of any distinct covering system.
theorem erdos_2 :
¬ ∀ B : ℕ, ∃ c : StrictCoveringSystem ℤ, ∀ i, ∃ m : ℕ,
c.moduli i = Ideal.span {(m : ℤ)} ∧ B < m
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/2.lean, line 48.
Sources
TheoremErdős Problem 3#
References: - erdosproblems.com/3 - [BlSi20] Bloom, Thomas F. and Sisask, Olof, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions. arXiv:2007.03528 (2020). - [Go01] Gowers, W. T., A new proof of Szemerédi's theorem. Geom. Funct. Anal. (2001), 465-588. - [GrTa17] Green, Ben and Tao, Terence, New bounds for Szemerédi's theorem, III: a polylogarithmic bound for \(r_4(N)\). Mathematika (2017). - [KeMe23] Kelley, Zander and Meka, Raghu, Strong bounds for 3-progressions. 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS) (2023). - [LSS24] Leng, James, Sah, Ashwin and Sawhney, Mehtaab, Improved bounds for Szemerédi's theorem. arXiv:2402.17995 (2024). - [OAI26] OpenAI, Quasipolynomial Bounds for Arithmetic Progressions. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/3.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/3.
The file states 6 research or textbook statements: 6 solved.
Erdos3.erdos_3
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean#L38.
If \(A \subset \mathbb{N}\) has \(\sum_{n \in A}\frac 1 n = \infty\), then must \(A\) contain arbitrarily long arithmetic progressions?
Yes. This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof.
theorem erdos_3 : ∀ A : Set ℕ,
(¬ Summable fun a : A ↦ 1 / (a : ℝ)) →
∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength k
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 55.
Erdos3.erdos_3.variants.kelley_meka
Solved: stated here without proof.
There are \(\beta > 0\) and \(c > 0\) such that \(r_3(N) \ll N \exp(-c (\log N)^{\beta})\).
Proved by Kelley and Meka [KeMe23].
theorem erdos_3.variants.kelley_meka : ∃ β > (0 : ℝ), ∃ c > (0 : ℝ),
(fun N ↦ (r 3 N : ℝ)) ≪ fun N : ℕ ↦ (N : ℝ) * Real.exp (-c * Real.log N ^ β)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 72.
Erdos3.erdos_3.variants.three
Solved: stated here; a Lean proof assuming erdos_3.variants.kelley_meka is at https://github.com/wilsonwu-ai/sundai-erdos-3/blob/8a58287a16558bf1e708eaa2d0f7cba4c86566a3/lean/Erdos3ThreeCase.lean#L96-L97.
The case of \(3\)-term progressions: if \(A \subset \mathbb{N}\) has \(\sum_{n \in A}\frac 1 n = \infty\), then \(A\) contains a non-trivial \(3\)-term arithmetic progression.
Proved by Bloom and Sisask [BlSi20].
theorem erdos_3.variants.three : ∀ A : Set ℕ,
(¬ Summable fun a : A ↦ 1 / (a : ℝ)) → ∃ S ⊆ A, S.IsAPOfLength 3
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 87.
Erdos3.erdos_3.variants.green_tao
Solved: stated here without proof.
There is \(c > 0\) such that \(r_4(N) \ll N (\log N)^{-c}\).
Proved by Green and Tao [GrTa17].
theorem erdos_3.variants.green_tao : ∃ c > (0 : ℝ),
(fun N ↦ (r 4 N : ℝ)) ≪ fun N : ℕ ↦ (N : ℝ) * Real.log N ^ (-c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 97.
Erdos3.erdos_3.variants.gowers
Solved: stated here without proof.
For every \(k \geq 3\) there is \(c_k > 0\) such that \(r_k(N) \ll_k N (\log \log N)^{-c_k}\).
Proved by Gowers [Go01].
theorem erdos_3.variants.gowers (k : ℕ) (hk : 3 ≤ k) : ∃ c > (0 : ℝ),
(fun N ↦ (r k N : ℝ)) ≪ fun N : ℕ ↦ (N : ℝ) * Real.log (Real.log N) ^ (-c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 107.
Erdos3.erdos_3.variants.leng_sah_sawhney
Solved: stated here without proof.
For every \(k \geq 5\) there is \(c_k > 0\) such that \(r_k(N) \ll_k N \exp(-(\log \log N)^{c_k})\).
Proved by Leng, Sah and Sawhney [LSS24].
theorem erdos_3.variants.leng_sah_sawhney (k : ℕ) (hk : 5 ≤ k) : ∃ c > (0 : ℝ),
(fun N ↦ (r k N : ℝ)) ≪
fun N : ℕ ↦ (N : ℝ) * Real.exp (-Real.log (Real.log N) ^ c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/3.lean, line 117.
Sources
TheoremErdős Problem 4#
Reference: erdosproblems.com/4
Quoted from FormalConjectures/ErdosProblems/4.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/4.
The file states 2 research or textbook statements: 2 solved.
Erdos4.erdos_4
Solved: stated here without proof.
Is it true that, for any \(C > 0\), there infinitely many \(n\) such that:
\[ p_{n + 1} - p_n > C \frac{\log\log n\log\log\log\log n}{(\log\log\log n) ^ 2}\log n \]
theorem erdos_4 : (∀ C > 0, Erdos4For C)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/4.lean, line 43.
Erdos4.erdos_4.variants.rankin
Solved: stated here without proof.
Rankin's theorem: there exists a positive constant \(C\) such that
Erdos4For Cholds.
theorem erdos_4.variants.rankin :
∃ C > 0, Erdos4For C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/4.lean, line 48.
Sources
TheoremErdős Problem 5#
References: - erdosproblems.com/5 - [BFM16] Banks, William D. and Freiberg, Tristan and Maynard, James, On limit points of the sequence of normalized prime gaps. Proc. Lond. Math. Soc. (3) (2016), 515-539. - [Er55] Erdős, Paul, Some remarks on number theory. Riveon Lematematika (1955), 45-48. - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984) (1985), 74-84. - [Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67. - [GPY09] Goldston, Daniel A. and Pintz, János and Yıldırım, Cem Y., Primes in tuples. I. Ann. of Math. (2) (2009), 819-862. - [HiMa88] Hildebrand, Adolf and Maier, Helmut, Gaps between prime numbers. Proc. Amer. Math. Soc. (1988), 1-9. - [Me20] Merikoski, Jori, Limit points of normalized prime gaps. J. Lond. Math. Soc. (2) (2020), 99-124. - [Pi16] Pintz, János, Polignac numbers, conjectures of Erdős on gaps between primes, arithmetic progressions in primes, and the bounded gap conjecture. From arithmetic to zeta-functions (2016), 367-384. - [Ri56] Ricci, Giovanni, Recherches sur l'allure de la suite \(\{p_{n+1}-p_n/\log p_n\}\). Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 93-106. - [We31] Westzynthius, E., Über die Verteilung der Zahlen, die zu den n ersten Primzahlen teilerfremd sind. Commentat. Phys. Math. (1931), 1-37.
Quoted from FormalConjectures/ErdosProblems/5.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/5.
The file states 14 research or textbook statements: 3 open and 11 solved. It also has 6 test statements, counted here but not shown.
Erdos5.erdos_5
Open: stated without proof.
Let \(C\geq 0\). Is there an infinite sequence of \(n_i\) such that
\[\lim_{i\to \infty}\frac{p_{n_i+1}-p_{n_i}}{\log n_i}=C?\]We formalise "an infinite sequence of \(n_i\)" as a strictly monotone sequence of indices
n : ℕ → ℕ. Note that the numerator is the gap between the two consecutive primes \(p_{n_i}\) and \(p_{n_i+1}\), which isprimeGap (n i), and not the gap between the primes indexed by two consecutive members of the sequence.
theorem erdos_5 : ∀ C : ℝ, 0 ≤ C →
∃ n : ℕ → ℕ, StrictMono n ∧ Tendsto (fun i => normalizedGap (n i)) atTop (𝓝 C)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 84.
Erdos5.erdos_5.variants.limit_point_set
Open: stated without proof.
Let \(S\) be the set of limit points of \((p_{n+1}-p_n)/\log n\). This problem asks whether \(S=[0,\infty]\).
Since \(\infty\in S\) is known (see
erdos_5.variants.westzynthius), the open content is the equality of the finite part of \(S\) with \([0,\infty)\).
theorem erdos_5.variants.limit_point_set : limitPointSet = Ici 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 96.
Erdos5.erdos_5.variants.westzynthius
Solved: stated here without proof.
\(\infty\in S\) by Westzynthius' result [We31] on large prime gaps.
theorem erdos_5.variants.westzynthius :
∃ n : ℕ → ℕ, StrictMono n ∧ Tendsto (fun i => normalizedGap (n i)) atTop atTop
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 103.
Erdos5.erdos_5.variants.goldston_pintz_yildirim
Solved: stated here without proof.
\(0\in S\) by the work of Goldston, Pintz, and Yildirim [GPY09] on small prime gaps.
theorem erdos_5.variants.goldston_pintz_yildirim : (0 : ℝ) ∈ limitPointSet
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 111.
Erdos5.erdos_5.variants.erdos_ricci
Solved: stated here without proof.
Erdős [Er55] and Ricci [Ri56] independently showed that \(S\) has positive Lebesgue measure.
theorem erdos_5.variants.erdos_ricci : 0 < volume limitPointSet
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 118.
Erdos5.erdos_5.variants.hildebrand_maier
Solved: stated here without proof.
Hildebrand and Maier [HiMa88] showed that \(S\) contains arbitrarily large (finite) numbers.
theorem erdos_5.variants.hildebrand_maier : ∀ C : ℝ, ∃ x ∈ limitPointSet, C < x
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 125.
Erdos5.erdos_5.variants.hildebrand_maier_measure
Solved: stated here without proof.
[HiMa88] in fact prove the stronger statement that there is a constant \(c>0\) with \(\lambda([0,T]\cap S)\geq cT\) for all sufficiently large \(T\).
theorem erdos_5.variants.hildebrand_maier_measure : ∃ c > (0 : ℝ), ∀ᶠ T : ℝ in atTop,
ENNReal.ofReal (c * T) ≤ volume (limitPointSet ∩ Icc 0 T)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 133.
Erdos5.erdos_5.variants.pintz
Solved: stated here without proof.
Pintz [Pi16] showed that there exists some small constant \(c>0\) such that \([0,c]\subset S\).
theorem erdos_5.variants.pintz : ∃ c > (0 : ℝ), Icc 0 c ⊆ limitPointSet
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 141.
Erdos5.erdos_5.variants.banks_freiberg_maynard
Solved: stated here without proof.
Banks, Freiberg, and Maynard [BFM16] showed that at least \(12.5\%\) of \([0,\infty)\) belongs to \(S\).
This is [BFM16, Theorem 1.1]: for any nine nonnegative reals \(\beta_1\leq\beta_2\leq\cdots\leq\beta_9\), at least one of the differences \(\beta_j-\beta_i\) with \(i\lt j\) belongs to \(S\).
theorem erdos_5.variants.banks_freiberg_maynard (β : Fin 9 → ℝ) (hβ : ∀ i, 0 ≤ β i)
(hβmono : Monotone β) : ∃ i j, i < j ∧ β j - β i ∈ limitPointSet
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 153.
Erdos5.erdos_5.variants.banks_freiberg_maynard_measure
Solved: stated here without proof.
The \(12.5\%\) claim itself, as deduced in [BFM16, Corollary 1.2]: \(\lambda([0,T]\cap S)\geq (1-o(1))T/8\) as \(T\to\infty\).
Note that the constant \(1/8\) is only attained asymptotically and ineffectively; the bound [BFM16] obtain for all \(T>0\) is the weaker \(\lambda([0,T]\cap S)>T/22\).
theorem erdos_5.variants.banks_freiberg_maynard_measure : ∀ ε > (0 : ℝ), ∀ᶠ T : ℝ in atTop,
ENNReal.ofReal ((1 - ε) * T / 8) ≤ volume (limitPointSet ∩ Icc 0 T)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 165.
Erdos5.erdos_5.variants.merikoski
Solved: stated here without proof.
Merikoski [Me20] showed that at least \(1/3\) of \([0,\infty)\) belongs to \(S\).
This is [Me20, Theorem 1]: for any reals \(\beta_1\leq\beta_2\leq\beta_3\leq\beta_4\), at least one of the differences \(\beta_j-\beta_i\) with \(i\lt j\) belongs to \(S\). Note that, in contrast with
erdos_5.variants.banks_freiberg_maynard, the \(\beta_i\) are not required to be nonnegative.
theorem erdos_5.variants.merikoski (β : Fin 4 → ℝ) (hβmono : Monotone β) :
∃ i j, i < j ∧ β j - β i ∈ limitPointSet
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 177.
Erdos5.erdos_5.variants.merikoski_measure
Solved: stated here without proof.
The \(1/3\) claim itself [Me20, Corollary 2]: \(\lambda([0,T]\cap S)\geq T/3\) for all \(T>0\).
Unlike the \(1/8\) of [BFM16], this bound holds uniformly in \(T\) with no error term.
theorem erdos_5.variants.merikoski_measure : ∀ T > (0 : ℝ),
ENNReal.ofReal (T / 3) ≤ volume (limitPointSet ∩ Icc 0 T)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 187.
Erdos5.erdos_5.variants.merikoski_bounded_gaps
Solved: stated here without proof.
Merikoski [Me20] showed that \(S\) has bounded gaps.
This is [Me20, Corollary 3]: there is a (ineffective) constant \(C\geq 0\) such that \(S\cap[T,T+C]\neq\emptyset\) for all \(T\geq 0\).
theorem erdos_5.variants.merikoski_bounded_gaps :
∃ C ≥ (0 : ℝ), ∀ T ≥ (0 : ℝ), (limitPointSet ∩ Icc T (T + C)).Nonempty
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 198.
Erdos5.erdos_5.variants.dense
Open: stated without proof.
In [Er65b], [Er85c], and [Er97c] Erdős asks whether \(S\) is everywhere dense (but Weisenberg notes that clearly \(S\) is closed so this is equivalent to asking whether \(S=[0,\infty]\)).
theorem erdos_5.variants.dense : Ici (0 : ℝ) ⊆ closure limitPointSet
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/5.lean, line 207.
Sources
TheoremErdős Problem 6#
References: - erdosproblems.com/6 - [BFT15] Banks, William D. and Freiberg, Tristan and Turnage-Butterbaugh, Caroline L., Consecutive primes in tuples. Acta Arith. (2015), 261-266. - [Ma15] Maynard, James, Small gaps between primes. Ann. of Math. (2) (2015), 383-413.
Quoted from FormalConjectures/ErdosProblems/6.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/6.
The file states 3 research or textbook statements: 3 solved.
Erdos6.erdos_6
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos6.lean#L154.
There are infinitely many \(n\) such that \(d_n < d_{n+1} < d_{n+2}\), where \(d\) denotes the prime gap function.
theorem erdos_6 :
{n | primeGap n < primeGap (n + 1) ∧ primeGap (n + 1) < primeGap (n + 2)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/6.lean, line 39.
Erdos6.erdos_6.variants.increasing
Solved: stated here without proof.
For all \(m\), there are infinitely many \(n\) such that \(d_n < d_{n+1} < \dots < d_{n+m}\), where \(d\) denotes the prime gap function.
Proved by Banks, Freiberg, and Turnage-Butterbaugh [BFT15] with an application of the Maynard-Tao machinery concerning bounded gaps between primes [Ma15]
theorem erdos_6.variants.increasing (m : ℕ) :
{n | ∀ i ∈ Finset.range m, primeGap (n + i) < primeGap (n + i + 1)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/6.lean, line 51.
Erdos6.erdos_6.variants.decreasing
Solved: stated here without proof.
For all \(m\), there are infinitely many \(n\) such that \(d_n > d_{n+1} > \dots > d_{n+m}\), where \(d\) denotes the prime gap function.
Proved by Banks, Freiberg, and Turnage-Butterbaugh [BFT15] with an application of the Maynard-Tao machinery concerning bounded gaps between primes [Ma15]
theorem erdos_6.variants.decreasing (m : ℕ) :
{n | ∀ i ∈ Finset.range m, primeGap (n + i) > primeGap (n + i + 1)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/6.lean, line 64.
Sources
TheoremErdős Problem 7#
Reference: erdosproblems.com/7
Quoted from FormalConjectures/ErdosProblems/7.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/7.
The file states 1 research or textbook statement: 1 open.
Erdos7.erdos_7
Open: stated without proof.
Is there a covering system all of whose moduli are odd (and greater than 1)?
theorem erdos_7 :
∃ (C : StrictCoveringSystem ℤ), ∀ i,
¬ C.moduli i ≤ Ideal.span {2} ∧ C.moduli i ≠ ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/7.lean, line 36.
Sources
TheoremErdős Problem 9#
Reference: erdosproblems.com/9
Quoted from FormalConjectures/ErdosProblems/9.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/9.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 3 test statements, counted here but not shown.
Erdos9.erdos_9.variants.infinite
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/de08009e59829727653bfa20b8d8f7ed1b1baf79/erdos-9/Solution.lean#L25.
The set is known to be infinite. In [Er77c] Erdős credits Schinzel with proving that there are infinitely many odd integers not of this form, but gives no reference.
[Er77c] Erdős, P., Problems and results on combinatorial number theory. III..
theorem erdos_9.variants.infinite : Erdos9A.Infinite
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/9.lean, line 70.
Erdos9.erdos_9
Open: stated without proof.
Is the upper density of the set of odd numbers that cannot be expressed as a prime plus two powers of 2 positive?
theorem erdos_9 : 0 < Erdos9A.upperDensity
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/9.lean, line 78.
Sources
TheoremErdős Problem 10#
References: - erdosproblems.com/10 - [Cr71] Crocker, R., On the sum of a prime and of two powers of two. Pacific J. Math. 36 (1971), 103-107. - [Ga75] Gallagher, P. X., Primes and powers of 2. Acta Arith. 29 (1976), 353-370. - [GrSo98] Granville, A. and Soundararajan, K., A binary additive problem of Erdős and the order of \(2\) mod \(p^2\). Ramanujan J. 2 (1998), 283-298.
Quoted from FormalConjectures/ErdosProblems/10.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/10.
The file states 6 research or textbook statements: 2 open and 4 solved. It also has 2 test statements, counted here but not shown.
Erdos10.erdos_10
Open: stated without proof.
Is there some \(k\) such that every large integer is the sum of a prime and at most \(k\) powers of \(2\)?
theorem erdos_10 : ∃ k, ∀ᶠ n : ℕ in atTop, n ∈ sumPrimeAndTwoPows k
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 63.
Erdos10.erdos_10.variants.gallagher
Solved: stated here without proof.
Gallagher [Ga75] has shown that for any \(ϵ > 0\) there exists \(k(ϵ)\) such that the set of integers which are the sum of a prime and at most \(k(ϵ)\) many powers of \(2\) has lower density at least \(1 - ϵ\).
Ref: Gallagher, P. X., Primes and powers of 2.
theorem erdos_10.variants.gallagher (ε : ℝ)
(hε : 0 < ε) : ∃ k, 1 - ε ≤ (sumPrimeAndTwoPows k).lowerDensity
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 74.
Erdos10.erdos_10.variants.granville_soundararajan_odd
Open: stated without proof.
Granville and Soundararajan [GrSo98] have conjectured that at most \(3\) powers of \(2\) suffice for all odd integers, and hence at most \(4\) powers of \(2\) suffice for all even integers.
Ref: Granville, A. and Soundararajan, K., A Binary Additive Problem of Erdős and the Order of \(2\) mod \(p^2\)
theorem erdos_10.variants.granville_soundararajan_odd :
{n : ℕ | Odd n ∧ 1 < n} ⊆ sumPrimeAndTwoPows 3 ∧
{n : ℕ | Even n ∧ n ≠ 0} ⊆ sumPrimeAndTwoPows 4
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 86.
Erdos10.erdos_10.variants.grechuk_example
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/bed1ae569eaac7109327f644fa149b902b562873/erdos-10/Solution.lean#L36.
Bogdan Grechuk has observed that
1117175146is not the sum of a prime and at most \(3\) powers of \(2\).
theorem erdos_10.variants.grechuk_example :
1117175146 ∉ sumPrimeAndTwoPows 3
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 98.
Erdos10.erdos_10.variants.two_pows
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos10_erdos_10_variants_two_pows.lean#L340.
There are infinitely many even integers not the sum of a prime and \(2\) powers of \(2\)
theorem erdos_10.variants.two_pows :
Set.Infinite <| {n : ℕ | Even n} \ sumPrimeAndTwoPows 2
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 107.
Erdos10.erdos_10.variants.grechuk
Solved: stated here; a Lean proof is at https://gist.github.com/DaryxXx/e112c74cc648b08a420b0959315cf65f/4b347897ff1811f1db1d82594c581f54b8f31b7d#file-main-lean-L2287.
Bogdan Grechuk has observed that \(1117175146\) is not the sum of a prime and at most \(3\) powers of \(2\), and pointed out that parity considerations, coupled with the fact that there are many integers not the sum of a prime and \(2\) powers of \(2\) suggest that there exist infinitely many even integers which are not the sum of a prime and at most \(3\) powers of \(2\).
This follows from Crocker's construction [Cr71] of infinitely many odd \(t \equiv 15 \pmod{16}\) which are not the sum of a prime and \(2\) powers of \(2\): each such \(t + 1\) is even and not the sum of a prime and at most \(3\) powers of \(2\).
The linked Lean formalisation is by Daryxx, see comment section.
theorem erdos_10.variants.grechuk :
Set.Infinite <| {n : ℕ | Even n} \ sumPrimeAndTwoPows 3
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/10.lean, line 126.
Sources
TheoremErdős Problem 11#
Reference: erdosproblems.com/11
Quoted from FormalConjectures/ErdosProblems/11.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/11.
The file states 7 research or textbook statements: 4 open and 3 solved. It also has 1 test statement, counted here but not shown.
Erdos11.erdos_11
Open: stated without proof.
Is every large odd integer \(n\) the sum of a squarefree number and a power of 2?
theorem erdos_11 :
∀ᶠ n : ℕ in atTop, Odd n → ∃ k l : ℕ, Squarefree k ∧ n = k + 2 ^ l
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 36.
Erdos11.erdos_11.variants.all_odd
Open: stated without proof.
Every odd \(n > 1\) is the sum of a squarefree number and a power of 2. This is the form in earlier versions of erdosproblems.com/11 and the hypothesis of [GrSo98]. It is stronger than
erdos_11, which asks only about large \(n\): a single exception would refute it.
theorem erdos_11.variants.all_odd (n : ℕ) (hn : Odd n) (hn' : 1 < n) :
∃ k l : ℕ, Squarefree k ∧ n = k + 2 ^ l
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 46.
Erdos11.erdos_11.variants.not_four_dvd
Open: stated without proof.
Erdős often asked this under the weaker assumption that \(n > 1\) is not divisible by 4.
theorem erdos_11.variants.not_four_dvd (n : ℕ) (hn : ¬ 4 ∣ n) (hn' : 1 < n) :
∃ k l : ℕ , Squarefree k ∧ n = k + 2^l
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 61.
Erdos11.erdos_11.variants.two_pow_two
Open: stated without proof.
Is every odd \(n > 1\) the sum of a squarefree number and two powers of 2?
theorem erdos_11.variants.two_pow_two (n : ℕ) (hn : Odd n) (hn' : 1 < n) :
∃ k l m : ℕ , Squarefree k ∧ n = k + 2^l + 2^m
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 69.
Erdos11.erdos_11.variants.finite_bound1
Solved: stated here without proof.
Every odd \(1 < n < 10^7\) is the sum of a squarefree number and a power of 2.
theorem erdos_11.variants.finite_bound1 (n : ℕ) (hn : Odd n) (h : n < 10^7) (hn' : 1 < n) :
∃ k l : ℕ , Squarefree k ∧ n = k + 2^l
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 77.
Erdos11.erdos_11.variants.finite_bound2
Solved: stated here without proof.
Every odd \(1 < n < 2^50\) is the sum of a squarefree number and a power of 2.
theorem erdos_11.variants.finite_bound2 (n : ℕ) (hn : Odd n) (h : n < 2^50) (hn' : 1 < n) :
∃ k l : ℕ , Squarefree k ∧ n = k + 2^l
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 85.
Erdos11.erdos_11.variants.granville_soundararajan
Solved: stated here without proof.
Suppose that every odd \(n > 1\) is the sum of a squarefree number and a power of 2. Then the set of primes \(p\) such that \(2^p \not\equiv 2 \pmod{p^2}\) (the non-Wieferich primes) is infinite. This follows from Theorem 1 in [GrSo98]. [GrSo98] Granville, A. and Soundararajan, K., A Binary Additive Problem of Erdős and the Order of \(2\) mod \(p^2\). The Ramanujan Journal (1998), 283-298.
theorem erdos_11.variants.granville_soundararajan (H : type_of% erdos_11.variants.all_odd) :
{p : ℕ | p.Prime ∧ ¬ 2 ^ p ≡ 2 [MOD p ^ 2]}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/11.lean, line 96.
Sources
TheoremErdős Problem 12#
Reference: erdosproblems.com/12
Quoted from FormalConjectures/ErdosProblems/12.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/12.
The file states 9 research or textbook statements: 1 open, 7 solved and 1 textbook result.
Erdos12.isGood_example
Textbook result, stated without proof. A Lean proof is at https://github.com/mo271/formal-conjectures/blob/2663234a28260853790aa5752d8d4550ff0ab1ca/FormalConjectures/ErdosProblems/12.lean#L39.
The set of \(p ^ 2\) where \(p \cong 3 \mod 4\) is prime is an example of a good set. Formal proof provided by AlphaProof
theorem isGood_example :
IsGood {p ^ 2 | (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : p.Prime)}
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 45.
Erdos12.erdos_12.parts.i
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/8d872b465955e46e2d28bc165d186ea41fd0da9e/FormalConjectures/ErdosProblems/12.lean#L810.
Let \(A\) be an infinite set such that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). Is there such an \(A\) with \(\liminf \frac{|A \cap \{1, \dotsc, N\}|}{N^{1/2}} > 0\) ?
The DeepMind prover agent has found a formal proof of this statement.
theorem erdos_12.parts.i : ∃ (A : Set ℕ), IsGood A ∧
(0 : ℝ) < Filter.atTop.liminf
(fun N => (A ∩ Icc 1 N).ncard / (N : ℝ).sqrt)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 62.
Erdos12.erdos_12.parts.ii
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/118a6a60df73a9f47d6c89f3cdb3786eaa2e8d0a/FormalConjectures/ErdosProblems/12.lean#L740.
Let \(A\) be an infinite set such that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). Does there exist some absolute constant \(c > 0\) such that there are always infinitely many \(N\) with \(|A \cap \{1, \dotsc, N\}| < N^{1−c}\)?
The DeepMind prover agent has found a formal disproof of this statement.
theorem erdos_12.parts.ii : ¬ ∃ c > (0 : ℝ), ∀ (A : Set ℕ), IsGood A →
{N : ℕ| (A ∩ Icc 1 N).ncard < (N : ℝ) ^ (1 - c)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 78.
Erdos12.erdos_12.parts.iii
Open: stated without proof.
Let \(A\) be an infinite set such that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). Is it true that \(∑_{n \in A} \frac{1}{n} < \infty\)?
theorem erdos_12.parts.iii :
∀ (A : Set ℕ), IsGood A → Summable (fun (n : A) ↦ (1 / n : ℝ))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 87.
Erdos12.erdos_12.variants.erdos_sarkozy_density_0
Solved: stated here without proof.
Erdős and Sárközy proved that such an \(A\) must have density 0. [ErSa70] Erd\H os, P. and Sárk\"ozi, A., On the divisibility properties of sequences of integers. Proc. London Math. Soc. (3) (1970), 97-101
theorem erdos_12.variants.erdos_sarkozy_density_0 (A : Set ℕ) (hA : IsGood A) : A.HasDensity 0
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 97.
Erdos12.erdos_12.variants.erdos_sarkozy
Solved: stated here without proof.
Given any function \(f(x)\to \infty\) as \(x\to \infty\) there exists a set \(A\) with the property that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\), such that there are infinitely many \(N\) such that $$\lvert A\cap{1,\ldots,N}\rvert > \frac{N}{f(N)}.
theorem erdos_12.variants.erdos_sarkozy (f : ℕ → ℕ) (hf : atTop.Tendsto f atTop) :
∃ A, IsGood A ∧ {N : ℕ | (N : ℝ) / f N < (A ∩ Icc 1 N).ncard}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 106.
Erdos12.erdos_12.variants.example
Solved: stated here without proof.
An example of an \(A\) with the property that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\) and such that
\[\liminf \frac{\lvert A\cap\{1,\ldots,N\}\rvert}{N^{1/2}}\log N > 0\]is given by the set of \(p^2\), where \(p\equiv 3\pmod{4}\) is prime.
theorem erdos_12.variants.example (A : Set ℕ)
(hA : A = {p ^ 2 | (p : ℕ) (_ : p.Prime) (_ : p ≡ 3 [MOD 4])}) :
IsGood A ∧ 0 < atTop.liminf (fun (N : ℕ) ↦ (A ∩ Icc 1 N).ncard * (N : ℝ).log / √N)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 117.
Erdos12.erdos_12.variants.schoen
Solved: stated here without proof.
Let \(A\) be a set of natural numbers with the property that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). If all elements in \(A\) are pairwise coprime then
\[\lvert A\cap\{1,\ldots,N\}\rvert \ll N^{2/3}\]for infinitely many \(N\).
theorem erdos_12.variants.schoen (A : Set ℕ) (hA : IsGood A) (hA' : A.Pairwise Nat.Coprime) :
∃ C > (0 : ℝ), {N : ℕ | (A ∩ Icc 1 N).ncard ≤ C * (N : ℝ) ^ (2 / 3 : ℝ)}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 130.
Erdos12.erdos_12.variants.baier
Solved: stated here without proof.
Let \(A\) be a set of natural numbers with the property that there are no distinct \(a,b,c \in A\) such that \(a \mid (b+c)\) and \(b,c > a\). If all elements in \(A\) are pairwise coprime then
\[\lvert A\cap\{1,\ldots,N\}\rvert \ll N^{2/3}/\log N\]for infinitely many \(N\).
theorem erdos_12.variants.baier (A : Set ℕ) (hA : IsGood A) (hA' : A.Pairwise Nat.Coprime) :
∃ C > (0 : ℝ),
{N : ℕ | (A ∩ Icc 1 N).ncard ≤ C * (N : ℝ) ^ (2 / 3 : ℝ) / (N : ℝ).log}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/12.lean, line 141.
Sources
TheoremErdős Problem 13#
Reference: erdosproblems.com/13
Quoted from FormalConjectures/ErdosProblems/13.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/13.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos13.erdos_13
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos13.lean#L8261.
If \(A \subseteq \{1, ..., N\}\) is a set with no \(a, b, c \in A\) such that \(a | (b+c)\) and \(a < \min(b,c)\), then \(|A| \le N/3 + O(1)\). This has been solved by Bedert [Be23].
[Be23] Bedert, B., On a problem of Erdős and Sárközy about sequences with no term dividing the sum of two larger terms. arXiv:2301.07065 (2023).
theorem erdos_13 : ∃ C : ℝ, ∀ N : ℕ, ∀ A ⊆ Icc 1 N, IsForbiddenTripleFree A →
(A.card : ℝ) ≤ (N : ℝ) / 3 + C
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/13.lean, line 49.
Erdos13.erdos_13.variants.general
Open: stated without proof.
A general version asks, for a fixed \(r \in \mathbb{N}\), if a set \(A \subseteq \{1, ..., N\}\) has no \(a \in A\) and \(b_1, ..., b_r \in A\) such that \(a | (b_1 + ... + b_r)\) and \(a < \min(b_1, ..., b_r)\), then is it true that \(|A| \le N/(r+1) + O(1)\)?
theorem erdos_13.variants.general : ∀ r : ℕ, ∃ C : ℝ, ∀ N : ℕ,
∀ A ⊆ Icc 1 N,
(∀ a ∈ A, ∀ (b : Fin r → ℕ), (∀ i, b i ∈ A) → (∀ i, a < b i) →
¬ (a ∣ ∑ i, b i)) →
(A.card : ℝ) ≤ (N : ℝ) / (r + 1) + C
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/13.lean, line 60.
Sources
TheoremErdős Problem 14#
Reference: erdosproblems.com/14
Quoted from FormalConjectures/ErdosProblems/14.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/14.
The file states 2 research or textbook statements: 2 open.
Erdos14.erdos_14.parts.i
Open: stated without proof.
Let \(A ⊆ \mathbb{N}\). Let \(B ⊆ \mathbb{N}\) be the set of integers which are representable in exactly one way as the sum of two elements from \(A\). Is it true that for all \(\epsilon > 0\) and large \(N\), \(|\{1,\ldots,N\} \setminus B| \gg_\epsilon N^{1/2 - \epsilon}\)?
theorem erdos_14.parts.i :
∀ A, ∀ ε > 0, nonUniqueSumCount A ≫ almostSquareRoot ε
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/14.lean, line 54.
Erdos14.erdos_14.parts.ii
Open: stated without proof.
Is it possible that \(|\{1,\ldots,N\} \setminus B| = o(N^\frac{1}{2})\)?
theorem erdos_14.parts.ii :
∃ (A : Set ℕ), IsLittleO atTop (nonUniqueSumCount A) squareRoot
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/14.lean, line 61.
Sources
TheoremErdős Problem 15: Convergence of Series with Primes#
Reference: erdosproblems.com/15
Quoted from FormalConjectures/ErdosProblems/15.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/15.
The file states 1 research or textbook statement: 1 open.
Erdos15.erdos_15
Open: stated without proof.
Is it true that \(\sum_{n=1}^\infty(-1)^n\frac{n}{p_n}\) converges, where \(p_n\) is the sequence of primes?
Note: In the problem statement, \(p_n\) is the \(n\)-th prime, indexed such that \(p_1=2, p_2=3, \ldots\). We 0-index here to reflect how Nat.nth works.
Note: convergence here is convergence of the sequence of partial sums, which is what the problem asks about.
Summablewould be the wrong notion: it is unconditional summability, equivalent over \(\mathbb{R}\) to absolute convergence, and \(\sum_n n/p_n\) diverges.
theorem erdos_15 :
∃ l : ℝ, Tendsto (fun N => ∑ k ∈ Finset.range N,
(-1 : ℝ) ^ (k + 1) * (k + 1) / (k.nth Nat.Prime)) atTop (𝓝 l)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/15.lean, line 44.
Sources
TheoremErdős Problem 16#
References: - erdosproblems.com/16 - [Ch23] Chen, Yong-Gao, A conjecture of Erdős on \(p+2^k\). arXiv:2312.04120 (2023). - [Er50] Erdős, P., On integers of the form \(2^k+p\) and some related problems. Summa Brasil. Math. (1950), 113-123. - [Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. (1934), 668-678.
Quoted from FormalConjectures/ErdosProblems/16.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/16.
The file states 3 research or textbook statements: 3 solved.
Erdos16.erdos_16
Solved: stated here; a Lean proof is at https://github.com/danielchin/proofs/blob/main/Proofs/ErdosProblems/Erdos16.lean.
Is the set of odd integers not of the form \(2^k+p\) the union of an infinite arithmetic progression and a set of density \(0\)?
Erdős called this conjecture "rather silly".
Chen [Ch23] has proved the answer is no.
This was formalized in Lean by Chin using Aristotle.
theorem erdos_16 :
¬ ∃ A B : Set ℕ, Erdos16Set = A ∪ B ∧
(∃ a d : ℕ, d > 0 ∧ A = { x | ∃ m : ℕ, x = a + m * d }) ∧
density_zero B
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/16.lean, line 63.
Erdos16.erdos_16.variant.romanoff
Solved: stated here without proof.
Romanoff [Ro34] showed that the set of odd integers of this form has positive density.
theorem erdos_16.variant.romanoff :
let S := { n : ℕ | Odd n ∧ ∃ k p : ℕ, p.Prime ∧ n = 2 ^ k + p }
positive_lower_density S
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/16.lean, line 80.
Erdos16.erdos_16.variant.erdos
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos16_erdos_16_variant_erdos.lean#L103.
Using covering congruences Erdős [Er50] proved that the set of odd integers which are not of this form contains an infinite arithmetic progression.
theorem erdos_16.variant.erdos :
∃ a d : ℕ, d > 0 ∧ { x | ∃ m : ℕ, x = a + m * d } ⊆ Erdos16Set
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/16.lean, line 91.
Sources
TheoremErdős Problem 17#
Reference: erdosproblems.com/17
Quoted from FormalConjectures/ErdosProblems/17.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/17.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
Erdos17.erdos_17
Open: stated without proof.
Erdős Problem 17. Are there infinitely many cluster primes?
theorem erdos_17 : {p : ℕ | IsClusterPrime p}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/17.lean, line 42.
Erdos17.erdos_17.variants.upper_BES
Solved: stated here without proof.
In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound
\[\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}\]for every real \(A > 0\).
[BES99] Blecksmith, Richard and Erd\H os, Paul and Selfridge, J. L., Cluster primes. Amer. Math. Monthly (1999), 43--48.
theorem erdos_17.variants.upper_BES {A : ℝ} (hA : 0 < A) :
(fun x ↦ (clusterPrimeCount x : ℝ)) =O[atTop] fun x ↦ x / (log x) ^ A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/17.lean, line 56.
Erdos17.erdos_17.variants.upper_Elsholtz
Solved: stated here without proof.
In 2003, Elsholtz [El03] refined the upper bound to
\[\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)\]for every real \(0 < c < 1/8\).
[El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.
theorem erdos_17.variants.upper_Elsholtz :
∃ C : ℝ, 0 < C ∧
∀ c ∈ Set.Ioo 0 (1 / 8),
IsBigOWith C atTop (fun x ↦ (clusterPrimeCount x : ℝ))
(fun x ↦ x * exp (-c * (log (log x)) ^ 2))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/17.lean, line 68.
Sources
TheoremErdős Problem 18#
Reference: * erdosproblems.com/18 * [ErGr80] Erdős, P. and Graham, R. L. (1980). Old and New Problems and Results in Combinatorial Number Theory. Monographies de L'Enseignement Mathématique, 28. Université de Genève. (See the sections on Egyptian fractions or practical numbers). * [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.
Quoted from FormalConjectures/ErdosProblems/18.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/18.
The file states 6 research or textbook statements: 3 open, 2 solved and 1 textbook result. It also has 7 test statements, counted here but not shown.
Erdos18.factorial_isPractical
Textbook result, proved here.
\(h(n!)\) is well-defined since \(n!\) is practical for \(n ≥ 1\).
theorem factorial_isPractical (n : ℕ) : Nat.IsPractical n.factorial
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 182.
Erdos18.erdos_18a
Open: stated without proof.
Conjecture 1. Are there infinitely many practical numbers \(m\) such that \(h(m) < (\log \log m)^{O(1)}\)?
More precisely: does there exist a constant \(C > 0\) such that for infinitely many practical numbers \(m\), we have \(h(m) < (\log \log m)^C\)?
theorem erdos_18a :
∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧
(practicalH m : ℝ) < (log (log m)) ^ C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 234.
Erdos18.erdos_18b
Open: stated without proof.
Conjecture 2. Is it true that \(h(n!) < n^{o(1)}\)? That is, for all \(\varepsilon > 0\), is \(h(n!) < n^\varepsilon\) for sufficiently large \(n\)?
theorem erdos_18b :
∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (n : ℝ) ^ ε
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 245.
Erdos18.erdos_18c
Open: stated without proof.
Conjecture 3. Or perhaps even \(h(n!) < (\log n)^{O(1)}\)?
Erdős offered $250 for a proof or disproof.
theorem erdos_18c :
∃ C : ℝ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, (practicalH n.factorial : ℝ) < (log n) ^ C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 256.
Erdos18.erdos_18_upper_bound
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/b246a4165f55ada0614aa2b85c8bc6381522e808/erdos-18/Solution.lean#L31.
Erdős's Theorem. Erdős proved that \(h(n!) < n\) for all \(n \ge 1\).
theorem erdos_18_upper_bound :
∀ᶠ n : ℕ in atTop, practicalH (Nat.factorial n) < n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 267.
Erdos18.erdos_18_vose
Solved: stated here without proof.
Vose's Theorem. Vose proved the existence of infinitely many practical numbers \(m\) such that \(h(m) \ll (\log m)^{1/2}\). This gives a positive answer to a weaker form of Conjecture 1.
theorem erdos_18_vose :
∃ C : ℝ, 0 < C ∧ ∃ᶠ m in atTop, Nat.IsPractical m ∧
(practicalH m : ℝ) < C * (log m) ^ (1 / 2 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/18.lean, line 277.
Sources
TheoremErdős Problem 19#
The Erdős–Faber–Lovász conjecture: if \(G\) is an edge-disjoint union of \(n\) copies of \(K_n\), is \(\chi(G) = n\)?
We model \(G\) by a family of \(n\) vertex sets of size \(n\) (the copies of \(K_n\)) which pairwise share at most one vertex and which cover the vertex type. Two copies of \(K_n\) are edge-disjoint exactly when their vertex sets share at most one vertex.
References: * erdosproblems.com/19 * [Hi81] Hindman, N., On a conjecture of Erdős, Faber, and Lovász about \(n\)-colorings. Canad. J. Math. (1981). * [Ka92] Kahn, J., Coloring nearly-disjoint hypergraphs with \(n + o(n)\) colors. J. Combin. Theory Ser. A (1992). * [KKKMO21] Kang, D. Y., Kelly, T., Kühn, D., Methuku, A. and Osthus, D., A proof of the Erdős–Faber–Lovász conjecture. Ann. of Math. (2023). arXiv:2101.04698
Quoted from FormalConjectures/ErdosProblems/19.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/19.
The file states 7 research or textbook statements: 1 open, 3 solved and 3 textbook results. It also has 1 test statement and 1 API statement, counted here but not shown.
Erdos19.EFLConfig.le_chromaticNumber
Textbook result, proved here.
The graph \(G\) contains a copy of \(K_n\), so \(n \le \chi(G)\).
theorem le_chromaticNumber : (n : ℕ∞) ≤ C.graph.chromaticNumber
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 79.
Erdos19.EFLConfig.colorable_of_sharedColoring
Textbook result, proved here.
If the shared vertices can be coloured with \(n\) colours so that shared vertices in a common clique get distinct colours, then \(G\) is \(n\)-colourable.
theorem colorable_of_sharedColoring (c : V → Fin n)
(hc : ∀ i u v, u ∈ C.A i → v ∈ C.A i → C.IsShared u → C.IsShared v → c u = c v → u = v) :
C.graph.Colorable n
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 99.
Erdos19.EFLConfig.card_sharedSet_le
Textbook result, proved here.
There are at most \(\binom{n}{2}\) shared vertices, since two cliques share at most one vertex.
theorem card_sharedSet_le : C.sharedSet.card ≤ n.choose 2
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 155.
Erdos19.erdos_19
Open: stated without proof.
If \(G\) is an edge-disjoint union of \(n\) copies of \(K_n\), then is \(\chi(G) = n\)?
theorem erdos_19 :
∀ (V : Type) (n : ℕ) (C : EFLConfig V n), C.graph.chromaticNumber = n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 195.
Erdos19.erdos_19.variants.lt_ten
Solved: stated here without proof.
Hindman [Hi81] proved the Erdős–Faber–Lovász conjecture for \(n < 10\).
theorem erdos_19.variants.lt_ten :
∀ (V : Type) (n : ℕ) (C : EFLConfig V n), n < 10 → C.graph.chromaticNumber = n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 230.
Erdos19.erdos_19.variants.kahn
Solved: stated here without proof.
Kahn [Ka92] proved that \(\chi(G) \le (1 + o(1))n\).
theorem erdos_19.variants.kahn :
∀ ε > (0 : ℝ), ∀ᶠ n in atTop, ∀ (V : Type) (C : EFLConfig V n),
C.graph.Colorable ⌊(1 + ε) * n⌋₊
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 238.
Erdos19.erdos_19.variants.large_n
Solved: stated here without proof.
Kang, Kelly, Kühn, Methuku and Osthus [KKKMO21] proved the Erdős–Faber–Lovász conjecture for all sufficiently large \(n\).
theorem erdos_19.variants.large_n :
∀ᶠ n in atTop, ∀ (V : Type) (C : EFLConfig V n), C.graph.chromaticNumber = n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/19.lean, line 248.
Sources
TheoremErdős Problem 20#
References: * erdosproblems.com/20 * Wikipedia * [ErRa60] Erdős, Paul and Rado, Richard. Intersection theorems for systems of sets. J. London Math. Soc. 35 (1960), 85--90.
Quoted from FormalConjectures/ErdosProblems/20.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/20.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 test statement, counted here but not shown.
Erdos20.erdos_20
Open: stated without proof.
Is it true that \(f(n,k) < c_k^n\) for some constant \(c_k>0\) and for all \(n > 0\)?
theorem erdos_20 : ∃ (c : ℕ → ℕ), ∀ n k, n > 0 → f n k < (c k) ^ n
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/20.lean, line 54.
Erdos20.erdos_20.variants.erdos_rado_bound
Solved: stated here; a Lean proof is at https://github.com/HowieHwong/lean-erdos-proofs/blob/b8b641ba2d00dc4d1fe205a078a4159372672459/Erdos/P20.lean#L202.
Erdős and Rado [ErRa60] proved the factorial upper bound for the \(k\)-sunflower threshold: any family of \(n\)-uniform sets with more than \((k-1)^n \, n!\) members contains a \(k\)-sunflower, hence \(f(n,k) \le (k-1)^n \, n! + 1\).
theorem erdos_20.variants.erdos_rado_bound :
∀ n k, n > 0 → 2 ≤ k → f n k ≤ (k - 1) ^ n * n.factorial + 1
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/20.lean, line 67.
Sources
TheoremErdős Problem 21#
References: - erdosproblems.com/21 - [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42. - [Er90] Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467-478. - [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240. - [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10. - [ErLo75] Erdős, P. and Lovász, L., Problems and results on \(3\)-chromatic hypergraphs and some related questions. (1975), 609--627. - [Ka92b] Kahn, Jeff, On a problem of Erdős and Lovász: random lines in a projective plane. Combinatorica (1992), 417-423. - [Ka94] Kahn, Jeff, On a problem of Erdős and Lovász. II. \(n(r)=O(r)\). J. Amer. Math. Soc. (1994), 125-143. - [Tr14] A. Tripathi, A result on intersecting families with maximum transversal size. arXiv:1409.4610 (2014). - [BaWa21] J. Barát and I. M. Wanless, Intersecting and 2-intersecting hypergraphs with maximal covering number: the Erdős-Lovász theme revisited. J. Combin. Des. (2021), 260-286.
Quoted from FormalConjectures/ErdosProblems/21.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/21.
The file states 4 research or textbook statements: 1 open and 3 solved.
Erdos21.erdos_21
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos21.lean#L13036.
Let \(f(n)\) be minimal such that there is an intersecting family \(\mathcal{F}\) of sets of size \(n\) (so \(A\cap B\neq\emptyset\) for all \(A,B\in \mathcal{F}\)) with \(\lvert \mathcal{F}\rvert=f(n)\) such that any set \(S\) with \(\lvert S\rvert \leq n-1\) is disjoint from at least one \(A\in \mathcal{F}\).
Is it true that
\[f(n) \ll n?\]Conjectured by Erdős and Lovász [ErLo75], who proved that
\[\frac{8}{3}n-3\leq f(n) \ll n^{3/2}\log n\]for all \(n\). The upper bound was improved by Kahn [Ka92b] to \(f(n) \ll n\log n\). (The upper bound constructions in both cases are formed by taking a random set of lines from a projective plane of order \(n-1\), assuming \(n-1\) is a prime power.)
This problem was solved by Kahn [Ka94] who proved the upper bound \(f(n) \ll n\). The Erdős-Lovász lower bound of \(\frac{8}{3}n-O(1)\) has not been improved, and it has been speculated (see e.g. [Ka94]) that the correct answer is \(3n+O(1)\).
It is trivial that \(f(1)=1\) and \(f(2)=3\). The values \(f(3)=6\) and \(f(4)=9\) were established by Tripathi [Tr14]. Barát and Wanless [BaWa21] proved that \(f(5)=13\), and that \(13\leq f(6)\leq 18\).
theorem erdos_21 : ∃ C : ℕ, ∀ᶠ n : ℕ in atTop, f n ≤ C * n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/21.lean, line 86.
Erdos21.erdos_21.variants.lower
Solved: stated here without proof.
Erdős and Lovász [ErLo75] proved that \(\frac{8}{3}n-3\leq f(n)\) for all \(n\).
theorem erdos_21.variants.lower (n : ℕ) : (8 / 3 : ℝ) * n - 3 ≤ f n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/21.lean, line 91.
Erdos21.erdos_21.variants.three_n
Open: stated without proof.
It has been speculated (see e.g. [Ka94]) that the correct answer is \(3n+O(1)\).
theorem erdos_21.variants.three_n : ∃ C : ℕ, ∀ᶠ n : ℕ in atTop,
f n ≤ 3 * n + C ∧ 3 * n ≤ f n + C
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/21.lean, line 96.
Erdos21.erdos_21.variants.small_values
Solved: stated here without proof.
\(f(1)=1\), \(f(2)=3\), \(f(3)=6\) [Tr14], \(f(4)=9\) [Tr14] and \(f(5)=13\) [BaWa21].
theorem erdos_21.variants.small_values : f 1 = 1 ∧ f 2 = 3 ∧ f 3 = 6 ∧ f 4 = 9 ∧ f 5 = 13
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/21.lean, line 102.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.