Erdős Problem 400 to Erdős Problem 422

TheoremErdős Problem 400#

Reference: erdosproblems.com/400

Quoted from FormalConjectures/ErdosProblems/400.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/400.

The file states 3 research or textbook statements: 2 open and 1 solved. It also has 1 test statement, counted here but not shown.

Erdos400.erdos_400.parts.i

Open: stated without proof.

Can one show that \(\sum_{n\leq x}g_k(n) \sim c_k x\log x\) for some constant \(c_k\)?

theorem erdos_400.parts.i :
    ∀ᵉ (k ≥ 2), ∃ c : ℝ,
      (fun x : ℕ ↦ (∑ n ∈ Icc 1 x, (g k n : ℝ))) ~[atTop]
      (fun x : ℕ ↦ c * x * Real.log x)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/400.lean, line 44.

Erdos400.erdos_400.parts.ii

Open: stated without proof.

Is it true that there is a constant \(c_k\) such that for almost all \(n < x\) we have \(g_k(n)=c_k\log x+o(\log x)\)?

theorem erdos_400.parts.ii :
    ∀ᵉ (k ≥ 2), ∃ c : ℝ, ∀ ε > 0,
      Tendsto (fun x : ℕ ↦
        (((Icc 1 x).filter (fun n ↦
          |(g k n : ℝ) - c * Real.log x| ≤ ε * Real.log x)).card : ℝ) / x)
        atTop (𝓝 1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/400.lean, line 55.

Erdos400.erdos_400.variants.upper_bound

Solved: stated here without proof.

Erdős and Graham write that it is easy to show that \(g_k(n) \ll_k \log n\) always, but the best possible constant is unknown.

theorem erdos_400.variants.upper_bound (k : ℕ) (hk : k ≥ 2) :
    (fun n : ℕ ↦ (g k n : ℝ)) ≪ (fun n : ℕ ↦ Real.log (n : ℝ))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/400.lean, line 68.

Sources

• FormalConjectures/ErdosProblems/400.lean at 2055e5ad
• erdosproblems.com/400

LeanErdos400.erdos_400.parts.i · Erdos400.erdos_400.parts.ii · Erdos400.erdos_400.variants.upper_bound

TheoremErdős Problem 401#

References: - erdosproblems.com/401 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

Quoted from FormalConjectures/ErdosProblems/401.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/401.

The file states 1 research or textbook statement: 1 solved.

Erdos401.erdos_401

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos401.lean.

Is there some function \(f(r)\) such that \(f(r)\to \infty\) as \(r\to\infty\), such that, for infinitely many \(n\), there exist \(a_1,a_2\) with

\[a_1+a_2> n+f(r)\log n\]

such that \(a_1!a_2! \mid n!2^n3^n\cdots p_r^n\)?

It is ambiguous in [ErGr80] what the intended quantifiers are on the variables (they write 'is it true that we can find \(a_1+a_2>n+f(r)\log n\)...'). Comparing to previous problems such as [728] and [729] it seems most likely that they intended to ask the formulation in the problem statement.

The answer is yes: Barreto and Leeham have used ChatGPT to provide a proof of the stated problem (in fact essentially the same construction as their solution to [729]).

theorem erdos_401 :
    ∃ f : ℕ → ℝ, Tendsto f atTop atTop ∧
      ∀ (r : ℕ) (hr : 1 ≤ r),
        {n : ℕ | ∃ a₁ a₂ : ℕ, 0 < a₁ ∧ 0 < a₂ ∧
          (a₁ : ℝ) + a₂ > n + f r * Real.log n ∧
          a₁.factorial * a₂.factorial ∣
            n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/401.lean, line 51.

Sources

• FormalConjectures/ErdosProblems/401.lean at 2055e5ad
• erdosproblems.com/401

LeanErdos401.erdos_401

TheoremErdős Problem 402#

Reference: erdosproblems.com/402

Quoted from FormalConjectures/ErdosProblems/402.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/402.

The file states 3 research or textbook statements: 3 solved.

Erdos402.erdos_402

Solved: stated here without proof.

Prove that, for any finite set \(A\subset\mathbb{N}\), there exist \(a, b\in A\) such that

\[ \gcd(a, b)\leq a/|A|. \]

theorem erdos_402 (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty) : ∃ᵉ (a ∈ A) (b ∈ A),
    a.gcd b ≤ (a / A.card : ℚ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/402.lean, line 38.

Erdos402.erdos_402.variants.equality

Solved: stated here without proof.

A conjecture of Graham [Gr70], who also conjectured that (assuming \(A\) itself has no common divisor) the only cases where equality is achieved are when \(A = \{1, \dots, n\}\) or \(A = \{L/1, \dots, L/n\}\) (where \(L = \operatorname{lcm}(1, \dots, n)\)) or \(A = \{2, 3, 4, 6\}\). Note: The source [BaSo96] mentioned on the Erdős page makes it clear what quantifiers to use for "where equality is achieved". See Theorem 1.1 there.

TODO(firsching): Consider if we should have the other direction here as well or an iff statement.

theorem erdos_402.variants.equality (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty)
    (h₃ : A.gcd id = 1)
    (h : ∀ᵉ (a ∈ A) (b ∈ A), (a / A.card : ℚ) ≤ a.gcd b) :
    A = Finset.Icc 1 A.card ∨
    A = (Finset.Icc 1 A.card).image ((Finset.Icc 1 A.card).lcm id / ·) ∨
    A = {2, 3, 4, 6}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/402.lean, line 53.

Erdos402.erdos_402.variants.szegedy_zaharescu_weak

Solved: stated here without proof.

Proved for all sufficiently large sets (including the sharper version which characterises the case of equality) independently by Szegedy [Sz86] and Zaharescu [Za87]. The following is taken from [Sz86].

There exists an effectively computable \(n_0\) with the following properties: (i) if \(n \ge n_0\) and \(a_1, a_2, \dots, a_n\) are distinct natural numbers then \(\max_{i, j} \frac{a_i}{(a_i, a_j)} \ge n\). (ii) If equality holds then the system \(\{a_1, a_2, \dots, a_n\}\) is either of the type \(\{k, 2k, \dots, nk\}\) or of the type \(\left\{\frac{k}{1}, \frac{k}{2}, \dots, \frac{k}{n}\right\}\).

theorem erdos_402.variants.szegedy_zaharescu_weak : ∀ᶠ n in atTop,
    ∀ (A : Finset ℕ), A.card = n → 0 ∉ A →
      (n ≤ (A ×ˢ A).sup (fun x => x.1 / x.1.gcd x.2)) ∧
      (n = (A ×ˢ A).sup (fun x => x.1 / x.1.gcd x.2) ↔
        ∃ k > 0, A = (Finset.Icc 1 n).image (k * ·) ∨
          A = (Finset.Icc 1 n).image (k * (Finset.Icc 1 n).lcm id / ·))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/402.lean, line 72.

Sources

• FormalConjectures/ErdosProblems/402.lean at 2055e5ad
• erdosproblems.com/402

LeanErdos402.erdos_402 · Erdos402.erdos_402.variants.equality · Erdos402.erdos_402.variants.szegedy_zaharescu_weak

TheoremErdős Problem 403#

References: - erdosproblems.com/403 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Li76] Lin, S., On two problems of Erdős concerning sums of distinct factorials. Bell Laboratories internal memorandum (1960).

Quoted from FormalConjectures/ErdosProblems/403.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/403.

The file states 1 research or textbook statement: 1 solved.

Erdos403.erdos_403

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/f8a51976fd2e66a52b4928c109fb9ae877a1a507/problems/403/Erdos403.lean.

Does the equation

\[2^m=a_1!+\cdots+a_k!\]

with \(a_1\lt a_2\lt \cdots \lt a_k\) have only finitely many solutions?

Asked by Burr and Erdős. Frankl and Lin [Li76] independently showed that the answer is yes, and the largest solution is

\[2^7=2!+3!+5!.\]

In fact Lin showed that the largest power of \(2\) which can divide a sum of distinct factorials containing \(2\) is \(2^{254}\), and that there are only 5 solutions to \(3^m=a_1!+\cdots+a_k!\) (when \(m=0,1,2,3,6\)).

See also [404].

A solution is encoded below as a pair \((m, s)\) where \(s\) is the finite set \(\{a_1 < a_2 < \cdots < a_k\}\) of positive integers, so the distinctness of the \(a_i\) is given by set membership. The empty set contributes no solutions since \(2^m \geq 1 > 0\).

The linked proof gives more than finiteness: it classifies the solutions outright, as \((0,\{1\})\), \((1,\{2\})\), \((3,\{2,3\})\), \((5,\{2,3,4\})\) and \((7,\{2,3,5\})\), so the set below has exactly five elements.

theorem erdos_403 :
    {p : ℕ × Finset ℕ | (∀ a ∈ p.2, 0 < a) ∧
      2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/403.lean, line 59.

Sources

• FormalConjectures/ErdosProblems/403.lean at 2055e5ad
• erdosproblems.com/403

LeanErdos403.erdos_403

TheoremErdős Problem 405#

References: - erdosproblems.com/405 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980) - [BrEr91] Brindza, B. and Erdős, P., On some {D}iophantine problems involving powers and factorials. J. Austral. Math. Soc. Ser. A (1991), 1--7. - [YuLi96] Yu, Kunrui and Liu, Dehua, A complete resolution of a problem of {E}rdős and {G}raham. Rocky Mountain J. Math. (1996), 1235--1244.

Quoted from FormalConjectures/ErdosProblems/405.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/405.

The file states 3 research or textbook statements: 2 solved and 1 textbook result.

Erdos405.erdos_405

Solved: stated here without proof.

Let \(p\) be an odd prime. Is it true that the equation \((p-1)!+a^{p-1}=p^k\) has only finitely many solutions?

Originally proposed by Erdős and Graham [ErGr80]. Brindza and Erdős [BrEr91] proved that there are finitely many such solutions.

theorem erdos_405 :
    Set.Finite { x : ℕ × ℕ × ℕ | let (a, k, p) := x; p.Prime ∧ Odd p ∧
      Nat.factorial (p - 1) + a ^ (p - 1) = p ^ k}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/405.lean, line 48.

Erdos405.erdos_405.variants.nonodd_p

Textbook result, proved here.

Erdős and Graham [ErGr80] ask this allowing \(p=2\), but this is presumably an oversight, since clearly there are infinitely many solutions when \(p=2\).

Observe that this creates \(1! + a = 2^k\). For all \(k\), fix \(a = 2^k - 1\).

theorem erdos_405.variants.nonodd_p :
    Set.Infinite { x : ℕ × ℕ × ℕ | let (a, k, p) := x; p.Prime ∧
      Nat.factorial (p - 1) + a ^ (p - 1) = p ^ k}

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/405.lean, line 60.

Erdos405.erdos_405.variants.yu_liu

Solved: stated here without proof.

Yu and Liu [YuLi96] showed that the only solutions to \((p-1)! + a^(p-1) = p^k\) for an odd prime p are:

\[ 2! + 1^2 = 3\\ 2! + 5^2 = 3^3\\ 4! + 1^4 = 5^2 \]

theorem erdos_405.variants.yu_liu :
    { x : ℕ × ℕ × ℕ | let (a, k, p) := x; p.Prime ∧ Odd p ∧
      Nat.factorial (p - 1) + a ^ (p - 1) = p ^ k } =
    {(1, 1, 3), (5, 3, 3), (1, 2, 5)}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/405.lean, line 94.

Sources

• FormalConjectures/ErdosProblems/405.lean at 2055e5ad
• erdosproblems.com/405

LeanErdos405.erdos_405 · Erdos405.erdos_405.variants.nonodd_p · Erdos405.erdos_405.variants.yu_liu

TheoremErdős Problem 406#

Reference: erdosproblems.com/406

Quoted from FormalConjectures/ErdosProblems/406.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/406.

The file states 2 research or textbook statements: 2 open.

Erdos406.erdos_406

Open: stated without proof.

Is it true that there are only finitely many powers of \(2\) which have only the digits \(0\) and \(1\) when written in base \(3\)?

theorem erdos_406 : { n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1] }.Finite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/406.lean, line 35.

Erdos406.erdos_406.variants.one_two

Open: stated without proof.

If we only allow the digits \(1\) and \(2\) then \(2^{15}\) seems to be the largest such power of \(2\).

theorem erdos_406.variants.one_two :
    IsGreatest { n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [1, 2] } (2 ^ 15)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/406.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/406.lean at 2055e5ad
• erdosproblems.com/406

LeanErdos406.erdos_406 · Erdos406.erdos_406.variants.one_two

TheoremErdős Problem 407#

References: - erdosproblems.com/407 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [EGST88] Evertse, J.-H. and Győry, K. and Stewart, C. L. and Tijdeman, R., \(S\)-unit equations and their applications. New advances in transcendence theory (Durham, 1986) (1988), 110-174. - [TiWa88] Tijdeman, R. and Wang, Lian Xiang, Sums of products of powers of given prime numbers. Pacific J. Math. (1988), 177-193. - [BaBe24] Bajpai, Prajeet and Bennett, Michael A., Effective \(S\)-unit equations beyond three terms: Newman's conjecture. Acta Arith. (2024), 421-458.

Quoted from FormalConjectures/ErdosProblems/407.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/407.

The file states 1 research or textbook statement: 1 solved.

Erdos407.erdos_407

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos407.lean#L257.

Let \(w(n)\) count the number of solutions to

\[n=2^a+3^b+2^c3^d\]

with \(a,b,c,d\geq 0\) integers. Is it true that \(w(n)\) is bounded by some absolute constant?

A conjecture originally due to Newman.

This is true, and was proved by Evertse, Győry, Stewart, and Tijdeman [EGST88].

Quantitative bounds were provided by Tijdeman and Wang [TiWa88], who proved that (if \(w(n)\) only counts distinct solutions, where we call two solutions distinct if the sets \(\{2^a,3^b,2^{c}3^d\}\) are distinct) then \(w(n) \leq 4\) for all large \(n\).

This was made effective by Bajpai and Bennett [BaBe24], who proved that \(w(n)\leq 4\) if \(n\geq 131082\) and \(w(n)\leq 9\) for all \(n\). (The largest \(n\) for which \(w(n)=9\) is \(299\).)

theorem erdos_407 : ∃ C : ℕ, ∀ n : ℕ, w n ≤ C

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/407.lean, line 63.

Sources

• FormalConjectures/ErdosProblems/407.lean at 2055e5ad
• erdosproblems.com/407

LeanErdos407.erdos_407

TheoremErdős Problem 408#

References: - erdosproblems.com/408 - OEIS A003434: the values \(f(n)\) for \(n \geq 2\). - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique (1980). - [Pi29] Pillai, S. Sivasankaranarayana, On a function connected with \(\phi(n)\). Bull. Amer. Math. Soc. 35 (1929), 837-841. doi:10.1090/S0002-9904-1929-04800-6 - [Sh50] Shapiro, Harold N., On the iterates of a certain class of arithmetic functions. Comm. Pure Appl. Math. 3 (1950), 259-272. - [EGPS90] Erdős, P., Granville, A., Pomerance, C. and Spiro, C., On the normal behavior of the iterates of some arithmetic functions. Analytic number theory (Allerton Park, IL, 1989), Progr. Math. 85 (1990), 165-204. - [Gu04] Guy, Richard K., Unsolved problems in number theory. Third edition, Springer (2004), Problem B41. - [FKL10] Ford, K., Konyagin, S. V. and Luca, F., Prime chains and Pratt trees. Geom. Funct. Anal. 20 (2010), 1231-1258. arXiv:0904.0473 doi:10.1007/s00039-010-0089-0

Quoted from FormalConjectures/ErdosProblems/408.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/408.

The file states 4 research or textbook statements: 2 open and 2 solved. It also has 4 test statements, counted here but not shown.

Erdos408.erdos_408.parts.i

Open: stated without proof.

Let \(\phi(n)\) be the Euler totient function and \(\phi_k(n)\) be the iterated \(\phi\) function, so that \(\phi_1(n)=\phi(n)\) and \(\phi_k(n)=\phi(\phi_{k-1}(n))\). Let

\[f(n) = \min\{k : \phi_k(n)=1\}.\]

Does \(f(n)/\log n\) have a distribution function?

We ask for a distribution function \(F\) (non-decreasing, with \(F(-\infty) = 0\) and \(F(+\infty) = 1\)) such that, for every continuity point \(c\) of \(F\), the set \(\{n : f(n)/\log n \leq c\}\) has natural density \(F(c)\). For \(n \leq 1\) the quotient is \(0\) in Lean, which does not affect densities. Erdős, Granville, Pomerance and Spiro [EGPS90] proved that the answer is yes, conditional on a form of the Elliott–Halberstam conjecture.

theorem erdos_408.parts.i :
    ∃ F : ℝ → ℝ, Monotone F ∧ Tendsto F atBot (𝓝 0) ∧ Tendsto F atTop (𝓝 1) ∧
      ∀ c : ℝ, ContinuousAt F c →
        {n : ℕ | (f n : ℝ) / Real.log n ≤ c}.HasDensity (F c)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/408.lean, line 118.

Erdos408.erdos_408.parts.ii

Open: stated without proof.

Is \(f(n)/\log n\) almost always constant?

We read this as: is there a constant \(\alpha\) such that, for every \(\epsilon > 0\), the set of \(n\) with \(|f(n)/\log n - \alpha| < \epsilon\) has natural density \(1\)? Erdős, Granville, Pomerance and Spiro [EGPS90] proved that, conditional on a form of the Elliott–Halberstam conjecture, \(f(n)\) has normal order \(\alpha \log n\) for some constant \(\alpha > 0\), so that the answer is yes under this hypothesis.

theorem erdos_408.parts.ii :
    ∃ α : ℝ, ∀ ε > (0 : ℝ),
      {n : ℕ | |(f n : ℝ) / Real.log n - α| < ε}.HasDensity 1

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/408.lean, line 134.

Erdos408.erdos_408.variants.pillai

Solved: stated here without proof.

Pillai [Pi29] proved that, for all \(n \geq 2\),

\[\left\lfloor \frac{\log n - \log 2}{\log 3} \right\rfloor + 1 \leq f(n) \leq \left\lfloor \frac{\log n}{\log 2} \right\rfloor + 1.\]

These are Theorems I and III of [Pi29]; Pillai's function \(R(n)\) is the least \(r\) with \(\phi_r(n) = 1\), which is \(f(n)\). The lower bound is attained at \(n = 2 \cdot 3^k\), and \(f(2^k) = k\) (Erdos408.f_two_pow), so the upper bound cannot be replaced by \(f(n) < \log_2 n\).

theorem erdos_408.variants.pillai (n : ℕ) (hn : 2 ≤ n) :
    ⌊(Real.log n - Real.log 2) / Real.log 3⌋₊ + 1 ≤ f n ∧
      f n ≤ ⌊Real.log n / Real.log 2⌋₊ + 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/408.lean, line 148.

Erdos408.erdos_408.variants.ford_konyagin_luca

Solved: stated here without proof.

The third question asks what can be said about the largest prime factor \(P^+(\phi_k(n))\) when, say, \(k = \log\log n\); it is open-ended and is not formalised. The site remarks that it is likely true that, if \(k \to \infty\) however slowly with \(n\), then \(P^+(\phi_k(n)) \leq n^{o(1)}\) for almost all \(n\).

Ford, Konyagin and Luca [FKL10, Theorem 5] proved that for every \(\epsilon > 0\) and \(\delta > 0\) there is an integer \(k\) such that, for all large \(x\), at least \((1 - \epsilon)x\) integers \(n \leq x\) satisfy \(P^+(\phi_k(n)) \leq x^{\delta}\). Since \(P^+(\phi(m)) \leq P^+(m)\), this gives the remark above for every \(k = k(n) \to \infty\).

theorem erdos_408.variants.ford_konyagin_luca (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ k : ℕ, ∀ᶠ x : ℝ in atTop, (1 - ε) * x ≤
      ((Finset.Icc 1 ⌊x⌋₊).filter fun n ↦
        ((Nat.totient^[k] n).maxPrimeFac : ℝ) ≤ x ^ δ).card

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/408.lean, line 165.

Sources

• FormalConjectures/ErdosProblems/408.lean at 2055e5ad
• erdosproblems.com/408

LeanErdos408.erdos_408.parts.i · Erdos408.erdos_408.parts.ii · Erdos408.erdos_408.variants.pillai · Erdos408.erdos_408.variants.ford_konyagin_luca

TheoremErdős Problem 409#

Reference: erdosproblems.com/409

Quoted from FormalConjectures/ErdosProblems/409.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/409.

The file states 12 research or textbook statements: 12 open. It also has 1 test statement, counted here but not shown.

Erdos409.erdos_409.parts.i

Open: stated without proof.

How many iterations of \(n\mapsto\phi(n) + 1\) are needed before a prime is reached?

theorem erdos_409.parts.i (n : ℕ) (hn : 0 < n) :
    IsLeast { i | (φ · + 1)^[i] n |>.Prime } erdos_409.parts.i.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 42.

Erdos409.erdos_409.parts.i.isTheta

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\phi(n) + 1\) before a prime is reached. What is \(\Theta(c(n))\)?

theorem erdos_409.parts.i.isTheta (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =Θ[atTop] erdos_409.parts.i.isTheta.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 84.

Erdos409.erdos_409.parts.i.isBigO

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\phi(n) + 1\) before a prime is reached. Find the simplest function \(g(n)\) such that \(c(n) = O(g(n))\)?

theorem erdos_409.parts.i.isBigO (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =O[atTop] erdos_409.parts.i.isBigO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 96.

Erdos409.erdos_409.parts.i.isLittleO

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\phi(n) + 1\) before a prime is reached. Find the simplest function \(g(n)\) such that \(c(n) = o(g(n))\)?

theorem erdos_409.parts.i.isLittleO (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =o[atTop] erdos_409.parts.i.isLittleO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 108.

Erdos409.erdos_409.parts.ii

Open: stated without proof.

Can infinitely many \(n\) reach the same prime under the iteration \(n\mapsto\phi(n) + 1\)?

theorem erdos_409.parts.ii :
    ∃ (p : ℕ) (hp : p.Prime), { n | ∃ i, (φ · + 1)^[i] n = p }.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 117.

Erdos409.erdos_409.parts.iii

Open: stated without proof.

What is the density of \(n\) which reach any fixed prime under the iteration \(n\mapsto\phi(n) + 1\)?

theorem erdos_409.parts.iii (p : ℕ) (h : p.Prime) :
    { n | ∃ i, (φ · + 1)^[i] n = p }.HasDensity erdos_409.parts.iii.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 127.

Erdos409.erdos_409.variants.sigma

Open: stated without proof.

If the iteration \(n\mapsto\sigma(n) - 1\) starting at \(n > 1\) reaches a prime, how many iterations are needed before a prime is reached?

theorem erdos_409.variants.sigma (n : ℕ) (hn : n > 1)
    (hterm : ∃ i, (σ 1 · - 1)^[i] n |>.Prime) :
    IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } erdos_409.variants.sigma.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 140.

Erdos409.erdos_409.variants.sigma_termination

Open: stated without proof.

If \(n > 1\) then the iteration \(n\mapsto\sigma(n) - 1\) necessarily reaches a prime. Note: this is open — it is not clear that the σ iteration always terminates, since it is non-decreasing (unlike the φ iteration which is strictly decreasing).

theorem erdos_409.variants.sigma_termination (n : ℕ) (hn : n > 1) :
    ∃ i, (σ 1 · - 1)^[i] n |>.Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 149.

Erdos409.erdos_409.variants.sigma_isTheta

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\sigma(n) - 1\) before a prime is reached. What is \(\Theta(c(n))\)?

theorem erdos_409.variants.sigma_isTheta (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =Θ[atTop] erdos_409.variants.sigma_isTheta.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 162.

Erdos409.erdos_409.variants.sigma_isBigO

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\sigma(n) - 1\) before a prime is reached. Find the simplest function \(g(n)\) such that \(c(n) = O(g(n))\)?

theorem erdos_409.variants.sigma_isBigO (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =O[atTop] erdos_409.variants.sigma_isBigO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 174.

Erdos409.erdos_409.variants.sigma_isLittleO

Open: stated without proof.

Let \(c(n)\) be the minimum number of iterations of \(n\mapsto\sigma(n) - 1\) before a prime is reached. Find the simplest function \(g(n)\) such that \(c(n) = o(g(n))\)?

theorem erdos_409.variants.sigma_isLittleO (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =o[atTop] erdos_409.variants.sigma_isLittleO.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 186.

Erdos409.erdos_409.variants.sigma_prime_termination

Open: stated without proof.

Is it true that iterates of \(n\mapsto\sigma(n) - 1\) always reach a prime?

theorem erdos_409.variants.sigma_prime_termination :
    ∀ n > 1, ∃ i, (σ 1 · - 1)^[i] n |>.Prime

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/409.lean, line 195.

Sources

• FormalConjectures/ErdosProblems/409.lean at 2055e5ad
• erdosproblems.com/409

LeanErdos409.erdos_409.parts.i · Erdos409.erdos_409.parts.i.isTheta · Erdos409.erdos_409.parts.i.isBigO · Erdos409.erdos_409.parts.i.isLittleO · Erdos409.erdos_409.parts.ii · Erdos409.erdos_409.parts.iii · Erdos409.erdos_409.variants.sigma · Erdos409.erdos_409.variants.sigma_termination · Erdos409.erdos_409.variants.sigma_isTheta · Erdos409.erdos_409.variants.sigma_isBigO · Erdos409.erdos_409.variants.sigma_isLittleO · Erdos409.erdos_409.variants.sigma_prime_termination

TheoremErdős Problem 410#

Reference: erdosproblems.com/410

Quoted from FormalConjectures/ErdosProblems/410.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/410.

The file states 1 research or textbook statement: 1 open.

Erdos410.erdos_410

Open: stated without proof.

Let \(σ_1(n) = σ(n)\), the sum of divisors function, and \(σ_k(n) = σ(σ_{k-1}(n))\).

Is it true that \(\lim_{k → ∞} σ_k(n)^{\frac 1 k} = ∞\)?

This is problem (iii) from Erdos, Granville, Pomerance, Spiro "On the normal behavior of the iterates of some arithmetical functions" (page 169 of the book "Analytic Number Theory", 1990).

theorem erdos_410 : ∀ n > 1,
    Tendsto (fun k : ℕ ↦ ((sigma 1)^[k] n : ℝ) ^ (1 / (k : ℝ))) atTop atTop

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/410.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/410.lean at 2055e5ad
• erdosproblems.com/410

LeanErdos410.erdos_410

TheoremErdős Problem 412#

Reference: erdosproblems.com/412

Reviewed by @b-mehta on 2025-05-27

Quoted from FormalConjectures/ErdosProblems/412.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/412.

The file states 1 research or textbook statement: 1 open.

Erdos412.erdos_412

Open: stated without proof.

Let \(σ_1(n)=σ(n)\), the sum of divisors function, and \(σ_k(n) = σ(σ_{k-1}(n))\). Is it true that, for every \(m, n ≥ 2\), there exist some \(i, j\) such that \(σ_i(m) = σ_j(n)\)?

theorem erdos_412 : ∀ᵉ (m ≥ 2) (n ≥ 2), ∃ i j, (σ 1)^[i] m = (σ 1)^[j] n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/412.lean, line 39.

Sources

• FormalConjectures/ErdosProblems/412.lean at 2055e5ad
• erdosproblems.com/412

LeanErdos412.erdos_412

TheoremErdős Problem 413#

References: - erdosproblems.com/413 - A5236 - [La26] Lau, C. F., On the Number of Prime Factors of Consecutive Integers. arXiv:2604.15042 (2026).

Erdős called a natural number n a barrier for ω, the number of distinct prime divisors, if m + ω(m) ≤ n for all m < n. He believed there should be infinitely many such barriers, and even posed a relaxed variant asking whether there is some ε > 0 for which infinitely many n satisfy m + ε · ω(m) ≤ n for every m < n.

Quoted from FormalConjectures/ErdosProblems/413.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/413.

The file states 5 research or textbook statements: 2 open and 3 solved.

Erdos413.erdos_413.parts.i

Open: stated without proof.

Are there infinitely many barriers for ω?

theorem erdos_413.parts.i :
    { n | IsBarrier (fun m => ω m) n }.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/413.lean, line 49.

Erdos413.erdos_413.variants.hasPosDensity_barrier_expProd

Solved: stated here without proof.

Erdős proved that the barrier set for expProd is infinite and even has positive density.

HasPosDensity is the right reading rather than positive lower density. In [Er79d] this is Theorem 1, "the density of integers satisfying (2) is positive", where d₀(n) = ∏ αᵢ is expProd. The averaging argument there bounds the density below, but Erdős states the existence separately on the last page: "With a little more trouble, I can prove that the density of integers n for which n is a barrier for d₀(n) exists." He goes further, that if αᵢ is the density of n with max_{m<n} (m + d₀(m)) = n + i, then every αᵢ exists and they sum to 1.

[Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.

theorem erdos_413.variants.hasPosDensity_barrier_expProd :
    { n | IsBarrier (fun m => expProd m) n }.HasPosDensity

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/413.lean, line 69.

Erdos413.erdos_413.variants.bigOmega

Open: stated without proof.

Erdős believed there should be infinitely many barriers for Ω, the total prime multiplicity.

theorem erdos_413.variants.bigOmega :
    { n | IsBarrier (fun m => Ω m) n }.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/413.lean, line 75.

Erdos413.erdos_413.variants.bigOmega_largest_barrier_lt_100k

Solved: stated here without proof.

Selfridge computed that the largest Ω-barrier below 10^5 is 99840.

theorem erdos_413.variants.bigOmega_largest_barrier_lt_100k :
    IsGreatest {n : ℕ | n < 10 ^ 5 ∧ IsBarrier (fun m => Ω m) n} 99840

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/413.lean, line 81.

Erdos413.erdos_413.parts.ii

Solved: stated here without proof.

Does there exist some \(\epsilon > 0\) such that there are infinitely many \(\epsilon\)-barriers for \(\omega\)? Lau [La26, Theorem 1.3] gives a positive answer.

theorem erdos_413.parts.ii :
    (∃ ε > (0 : ℝ), { n | IsBarrier (fun n => ε * ω n) n }.Infinite)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/413.lean, line 88.

Sources

• FormalConjectures/ErdosProblems/413.lean at 2055e5ad
• erdosproblems.com/413

LeanErdos413.erdos_413.parts.i · Erdos413.erdos_413.variants.hasPosDensity_barrier_expProd · Erdos413.erdos_413.variants.bigOmega · Erdos413.erdos_413.variants.bigOmega_largest_barrier_lt_100k · Erdos413.erdos_413.parts.ii

TheoremErdős Problem 414#

Reference: erdosproblems.com/414

Quoted from FormalConjectures/ErdosProblems/414.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/414.

The file states 1 research or textbook statement: 1 open.

Erdos414.erdos_414

Open: stated without proof.

Let \(h_1(n) = h(n)\) and \(h_k(n) = h(h_{k-1}(n))\). Is it true, for any \(m,n\), there exist \(i\) and \(j\) such that \(h_i(m) = h_j(n)\)?

theorem erdos_414 : ∀ᵉ  (m > 0) (n > 0), ∃ i j, h^[i] m = h^[j] n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/414.lean, line 39.

Sources

• FormalConjectures/ErdosProblems/414.lean at 2055e5ad
• erdosproblems.com/414

LeanErdos414.erdos_414

TheoremErdős Problem 416#

References: - erdosproblems.com/416 - [OAI26a] OpenAI, An asymptotic formula for the number of totients. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf

Quoted from FormalConjectures/ErdosProblems/416.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/416.

The file states 7 research or textbook statements: 1 open and 6 solved.

Erdos416.erdos_416.parts.i

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L12.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2 ?

Yes. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which gives V(cx)/V(x)→c for every fixed c>0.

theorem erdos_416.parts.i :
    Filter.Tendsto (fun x => (V (2 * x) / V (x))) Filter.atTop (𝓝 2)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 51.

Erdos416.erdos_416.variants.regularly_varying

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L12.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Then V(cx)/V(x)→c for every fixed c>0, which answers a question of Erdős and Hall. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem erdos_416.variants.regularly_varying (c : ℝ) (hc : 0 < c) :
    Filter.Tendsto (fun x => V (c * x) / V x) Filter.atTop (𝓝 c)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 63.

Erdos416.erdos_416.parts.ii

Open: stated without proof.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Is there an asymptotic formula for V(x)?

theorem erdos_416.parts.ii :
    Filter.Tendsto (fun x => V x / erdos_416.parts.ii.answer x) atTop (𝓝 1)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 74.

Erdos416.erdos_416.variants.Pillai

Solved: stated here without proof.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Pillai proved V(x)=o(x). Ref: S. Sivasankaranarayana Pillai, On some functions connected with \(\phi(n)\)

theorem erdos_416.variants.Pillai : V =o[atTop] id

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 84.

Erdos416.erdos_416.variants.Erdos

Solved: stated here without proof.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Erdős proved V(x)=x(logx)^(−1+o(1)). Ref: Erdős, P., On the normal number of prime factors of \(p-1\) and some related problems concerning Euler's \(\varphi\)-function.

theorem erdos_416.variants.Erdos : ∃ f : ℝ → ℝ, f =o[atTop] (1 : ℝ → ℝ) ∧
    ∀ᶠ x in Filter.atTop, V x = x * x.log ^ (-1 + f x)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 93.

Erdos416.erdos_416.variants.Maier_Pomerance

Solved: stated here without proof.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x)=x/logx * e^((C+o(1))(log log log x)^2), for some explicit constant C>0. Ref:Maier, Helmut and Pomerance, Carl, On the number of distinct values of Euler's \(\phi\)-function.

theorem erdos_416.variants.Maier_Pomerance :
    0 < erdos_416.variants.Maier_Pomerance.answer ∧ ∃ f : ℝ → ℝ, f =o[atTop] (1 : ℝ → ℝ) ∧
      ∀ᶠ x in Filter.atTop, (V x : ℝ) = x / x.log *
        (rexp <| (erdos_416.variants.Maier_Pomerance.answer + f x) * x.log.log.log ^ 2)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 106.

Erdos416.erdos_416.variants.Ford

Solved: stated here without proof.

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x) ≍ x/log x*e^(C_1*(log log log x − log log log log x)^2+C_2 log log log x − C_3 log log log log x) Ref: Ford, Kevin, The distribution of totients.

theorem erdos_416.variants.Ford :
    let (C₁, C₂, C₃) : ℝ × ℝ × ℝ := erdos_416.variants.Ford.answer
    0 < C₁ ∧ 0 < C₂ ∧ 0 < C₃ ∧
    let G (x : ℝ) : ℝ := x / x.log * (rexp <| C₁ * (x.log.log.log - x.log.log.log.log) ^ 2
        + C₂* x.log.log.log - C₃ * x.log.log.log.log)
    V =Θ[atTop] G

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/416.lean, line 121.

Sources

• FormalConjectures/ErdosProblems/416.lean at 2055e5ad
• erdosproblems.com/416

LeanErdos416.erdos_416.parts.i · Erdos416.erdos_416.variants.regularly_varying · Erdos416.erdos_416.parts.ii · Erdos416.erdos_416.variants.Pillai · Erdos416.erdos_416.variants.Erdos · Erdos416.erdos_416.variants.Maier_Pomerance · Erdos416.erdos_416.variants.Ford

TheoremErdős Problem 417#

References: - erdosproblems.com/417 - [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180.

Quoted from FormalConjectures/ErdosProblems/417.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/417.

The file states 2 research or textbook statements: 2 open.

Erdos417.erdos_417.parts.i

Open: stated without proof.

Let

\[V'(x)=\#\{\phi(m) : 1\leq m\leq x\}\]

and

\[V(x)=\#\{\phi(m) \leq x : 1\leq m\}.\]

Does \(\lim V(x)/V'(x)\) exist?

theorem erdos_417.parts.i :
    ∃ L : ENNReal, Tendsto (fun x ↦
      ({ k | k ∈ range totient ∧ (k : ℝ) ≤ x }.ncard : ENNReal) /
      ((totient '' { m | 1 ≤ m ∧ (m : ℝ) ≤ x }).ncard : ENNReal))
      atTop (𝓝 L)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/417.lean, line 41.

Erdos417.erdos_417.parts.ii

Open: stated without proof.

Is it \(>1\)?

theorem erdos_417.parts.ii :
    ∃ L > (1 : ENNReal), Tendsto (fun x ↦
      ({ k | k ∈ range totient ∧ (k : ℝ) ≤ x }.ncard : ENNReal) /
      ((totient '' { m | 1 ≤ m ∧ (m : ℝ) ≤ x }).ncard : ENNReal))
      atTop (𝓝 L)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/417.lean, line 52.

Sources

• FormalConjectures/ErdosProblems/417.lean at 2055e5ad
• erdosproblems.com/417

LeanErdos417.erdos_417.parts.i · Erdos417.erdos_417.parts.ii

TheoremErdős Problem 418#

References: - erdosproblems.com/418 - Wikipedia: Noncototient - [BaLu05] Banks, William D. and Luca, Florian, Nonaliquots and {R}obbins numbers. Colloq. Math. (2005), 27--32. - [BrSc95] Browkin, J. and Schinzel, A., On integers not of the form {\(n-\phi(n)\)}. Colloq. Math. (1995), 55-58. - [ChZh11] Chen, Yong-Gao and Zhao, Qing-Qing, Nonaliquot numbers. Publ. Math. Debrecen (2011), 439--442. - [Er73b] Erdős, P., \"Über die Zahlen der Form \(\sigma (n)-n\) und \(n-\phi(n)\). Elem. Math. (1973), 83-86. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [PoPo16] Pollack, Paul and Pomerance, Carl, Some problems of Erdős on the sum-of-divisors function. Trans. Amer. Math. Soc. Ser. B (2016), 1-26.

Quoted from FormalConjectures/ErdosProblems/418.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/418.

The file states 6 research or textbook statements: 2 open and 4 solved. It also has 1 test statement, counted here but not shown.

Erdos418.erdos_418

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos418.lean.

Are there infinitely many integers not of the form \(n - \phi(n)\)?

Asked by Erdős and Sierpiński. Numbers not of the form we call non-cototients.

Browkin and Schinzel [BrSc95] provided an affirmative answer to this question, proving that any integer of the shape \(2^{k}\cdot 509203\) for \(k\geq 1\) is a non-cototient.

This is discussed in problem B36 of Guy's collection [Gu04].

This was formalized in Lean by Alexeev using Aristotle.

theorem erdos_418 : { (n - n.totient : ℕ) | n }ᶜ.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 59.

Erdos418.erdos_418.variants.conditional

Proved here.

It follows from a slight strengthening of the Goldbach conjecture that every odd number can be written as \(n - \phi(n)\). In particular, we assume that every even number greater than 6 can be written as the sum of two distinct primes, in contrast to the usual Goldbach conjecture that every even number greater than 2 can be written as the sum of two primes.

theorem erdos_418.variants.conditional
    (goldbach : ∀ (n : ℕ), 6 < n → Even n → ∃ p q, p ≠ q ∧ p.Prime ∧ q.Prime ∧ n = p + q)
    (m : ℕ) (h : Odd m) :
    ∃ n, m + n.totient = n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 70.

Erdos418.erdos_418.variants.odd_noncototient

Open: stated without proof.

The Odd Noncototient Conjecture: every non-cototient is even. Equivalently, every odd natural number is of the form \(n - \phi(n)\) for some \(n\).

This is the unconditional form of erdos_418.variants.conditional, which derives the odd case from a strengthening of the Goldbach conjecture. See [Wikipedia: Noncototient].

theorem erdos_418.variants.odd_noncototient :
    { (n - n.totient : ℕ) | n }ᶜ ⊆ { k | Even k }

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 99.

Erdos418.erdos_418.variants.sigma

Solved: stated here without proof.

Erdős [Er73b] has shown that a positive density set of natural numbers cannot be written as \(\sigma(n)-n\) (numbers not of this form are called nonaliquot, or sometimes untouchable).

Here "positive density" means positive lower density: Banks and Luca [BaLu05] proved that the set of nonaliquots has lower density at least \(1/48\), Chen and Zhao [ChZh11] improved this to \(0.06\), and it is not known whether the natural density of the nonaliquots exists (Pollack and Pomerance [PoPo16] give a heuristic predicting its value).

theorem erdos_418.variants.sigma :
    0 < { (σ 1 n - n : ℕ) | n }ᶜ.lowerDensity

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 122.

Erdos418.erdos_418.variants.soln

Solved: stated here without proof.

A solution to erdos_418 was shown by Browkin and Schinzel [BrSc95] by showing that any integer of the form \(2^(k + 1)\cdot 509203\) is not of the form \(n - \phi(n)\).

theorem erdos_418.variants.soln :
    { 2 ^ (k + 1) * 509203 | k } ⊆ { (n - n.totient : ℕ) | n }ᶜ

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 131.

Erdos418.erdos_418.variants.density

Open: stated without proof.

It is open whether the set of non-cototients has positive (lower) density.

theorem erdos_418.variants.density :
    0 < { (n - n.totient : ℕ) | n }ᶜ.lowerDensity

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/418.lean, line 139.

Sources

• FormalConjectures/ErdosProblems/418.lean at 2055e5ad
• erdosproblems.com/418

LeanErdos418.erdos_418 · Erdos418.erdos_418.variants.conditional · Erdos418.erdos_418.variants.odd_noncototient · Erdos418.erdos_418.variants.sigma · Erdos418.erdos_418.variants.soln · Erdos418.erdos_418.variants.density

TheoremErdős Problem 419#

References: - erdosproblems.com/419 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [EGIP96] Erdős, Paul and Graham, S. W. and Ivić, Aleksandar and Pomerance, Carl, On the number of divisors of \(n!\). (1996), 337--355.

Quoted from FormalConjectures/ErdosProblems/419.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/419.

The file states 1 research or textbook statement: 1 solved.

Erdos419.erdos_419

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos419.lean.

If \(\tau(n)\) counts the number of divisors of \(n\), then what is the set of limit points of

\[ \frac{\tau((n+1)!)}{\tau(n!)}? \]

The limit points are exactly \(\{1\} \cup \{1+1/k : k \geq 1\}\).

theorem erdos_419 :
    {x : ℝ | MapClusterPt x atTop factorialDivisorRatio} = limitPointSet

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/419.lean, line 56.

Sources

• FormalConjectures/ErdosProblems/419.lean at 2055e5ad
• erdosproblems.com/419

LeanErdos419.erdos_419

TheoremErdős Problem 420#

References: - erdosproblems.com/420 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [EGIP96] Erdős, P. and Graham, S. W. and Ivić, A. and Pomerance, C., On the number of divisors of \(n!\). Analytic number theory, Vol. 1 (Allerton Park, IL, 1995), Progr. Math. 138, Birkhäuser Boston (1996), 337-355.

In the solved variants, \(K(n)\) is the least \(K \geq 1\) with \(\tau((n+K)!) \geq 2\tau(n!)\), so that \(K(n) > h\) if and only if \(F(h, n) < 2\). These variants state Corollaries 2 and 3 of [EGIP96] as printed; the stronger claims on erdosproblems.com are not stated.

Quoted from FormalConjectures/ErdosProblems/420.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/420.

The file states 6 research or textbook statements: 3 open and 3 solved. It also has 3 test statements, counted here but not shown.

Erdos420.erdos_420.parts.i

Open: stated without proof.

If \(\tau(n)\) counts the number of divisors of \(n\) then let

\[F(f,n)=\frac{\tau((n+\lfloor f(n)\rfloor)!)}{\tau(n!)}.\]

Is it true that

\[\lim_{n\to \infty}F((\log n)^C,n)=\infty\]

for large \(C\)?

"For large \(C\)" means for all sufficiently large real \(C\). Since \((\log n)^C\) increases with \(C\) for \(n \geq 3\) and \(F(f,n)\) is nondecreasing in \(f(n)\), this is equivalent to asking for one such \(C\).

theorem erdos_420.parts.i :
    ∀ᶠ C : ℝ in atTop, Tendsto (F fun m ↦ Real.log m ^ C) atTop atTop

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 98.

Erdos420.erdos_420.parts.ii

Open: stated without proof.

Is it true that \(F(\log n,n)\) is everywhere dense in \((1,\infty)\)?

This asks that every point of \((1,\infty)\) lies in the closure of the set of values \(F(\log n, n)\). Note that \(F(f,n) \geq 1\) always (Erdos420.one_le_F).

theorem erdos_420.parts.ii :
    Set.Ioi (1 : ℝ) ⊆ closure (Set.range (F fun m ↦ Real.log m))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 109.

Erdos420.erdos_420.parts.iii

Open: stated without proof.

More generally, if \(f(n)\leq \log n\) is a monotonic function such that \(f(n)\to \infty\) as \(n\to \infty\), then is \(F(f,n)\) everywhere dense?

"Everywhere dense" means dense in \((1,\infty)\), as in Erdos420.erdos_420.parts.ii. Asking for \(f(n) \leq \log n\) for all \(n\), rather than for all large \(n\), gives an equivalent question.

theorem erdos_420.parts.iii :
    ∀ f : ℕ → ℝ, Monotone f → (∀ n, f n ≤ Real.log n) → Tendsto f atTop atTop →
      Set.Ioi (1 : ℝ) ⊆ closure (Set.range (F f))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 121.

Erdos420.erdos_420.variants.log_frequently_lt_two

Solved: stated here without proof.

Erdős, Graham, Ivić and Pomerance proved [EGIP96, Corollary 2] that \(K(n)/\log n\) is unbounded, with \(K(n)\) as in the module docstring. Equivalently, for every \(c > 0\) we have \(F(c\log n, n) < 2\) for infinitely many \(n\). In particular \(\liminf F(c\log n, n) \leq 2\).

theorem erdos_420.variants.log_frequently_lt_two :
    ∀ c > (0 : ℝ), ∃ᶠ n : ℕ in atTop, F (fun m ↦ c * Real.log m) n < 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 133.

Erdos420.erdos_420.variants.rankin_frequently_lt_two

Solved: stated here without proof.

Erdős, Graham, Ivić and Pomerance proved [EGIP96, Corollary 2] that for infinitely many \(n\),

\[K(n) > \frac{\log n \cdot \log\log n \cdot \log\log\log\log n}{9(\log\log\log n)^3},\]

with \(K(n)\) as in the module docstring. Equivalently, \(F(f,n) < 2\) for infinitely many \(n\), where \(f(n)\) is the right-hand side.

theorem erdos_420.variants.rankin_frequently_lt_two :
    ∃ᶠ n : ℕ in atTop, F (fun m ↦ Real.log m * Real.log (Real.log m) *
      Real.log (Real.log (Real.log (Real.log m))) /
        (9 * Real.log (Real.log (Real.log m)) ^ 3)) n < 2

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 144.

Erdos420.erdos_420.variants.pow_four_ninths

Solved: stated here without proof.

Erdős, Graham, Ivić and Pomerance proved [EGIP96, Corollary 3] that for all sufficiently large \(n\) we have \(K(n) < n^{4/9}\), with \(K(n)\) as in the module docstring. Hence \(F(n^{4/9}, n) \geq 2\) for all large \(n\).

theorem erdos_420.variants.pow_four_ninths :
    ∀ᶠ n : ℕ in atTop, 2 ≤ F (fun m ↦ (m : ℝ) ^ (4 / 9 : ℝ)) n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/420.lean, line 156.

Sources

• FormalConjectures/ErdosProblems/420.lean at 2055e5ad
• erdosproblems.com/420

LeanErdos420.erdos_420.parts.i · Erdos420.erdos_420.parts.ii · Erdos420.erdos_420.parts.iii · Erdos420.erdos_420.variants.log_frequently_lt_two · Erdos420.erdos_420.variants.rankin_frequently_lt_two · Erdos420.erdos_420.variants.pow_four_ninths

TheoremErdős Problem 421#

References: - erdosproblems.com/421 - [Pratt26] K. Pratt, A proof of Erdős Problem 421.

Quoted from FormalConjectures/ErdosProblems/421.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/421.

The file states 1 research or textbook statement: 1 solved.

Erdos421.erdos_421

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos421.lean#L121.

There exists a sequence \(1 \le d_1 < d_2 < \dots\) with density 1 such that all products \(\prod_{u \le i \le v} d_i\) are distinct. This was solved affirmatively; see [Pratt26].

theorem erdos_421 :
    ∃ (d : ℕ → ℕ), StrictMono d ∧ 1 ≤ d 0 ∧ HasDensity (Set.range d) 1 ∧
    {(u, v) : ℕ × ℕ | u ≤ v}.InjOn fun (u, v) => ∏ i ∈ Finset.Icc u v, d i

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/421.lean, line 40.

Sources

• FormalConjectures/ErdosProblems/421.lean at 2055e5ad
• erdosproblems.com/421

LeanErdos421.erdos_421

TheoremErdős Problem 422#

References: - erdosproblems.com/422 - OEIS A005185

Quoted from FormalConjectures/ErdosProblems/422.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/422.

The file states 5 research or textbook statements: 4 open and 1 textbook result. It also has 2 test statements and 1 API statement, counted here but not shown.

Erdos422.erdos_422

Open: stated without proof.

Let \(f(1) = f(2) = 1\) and for \(n > 2\)

\[ f(n) = f(n - f(n - 1)) + f(n - f(n - 2)). \]

Does \(f(n)\) miss infinitely many integers?

theorem erdos_422 :
    ∀ f : ℕ+ → ℕ+, IsHofstadterQ f → Set.Infinite {n | ∀ x, f x ≠ n}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/422.lean, line 78.

Erdos422.erdos_422.variants.surjective

Open: stated without proof.

Is \(f\) surjective?

theorem erdos_422.variants.surjective :
    ∀ f : ℕ+ → ℕ+, IsHofstadterQ f → f.Surjective

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/422.lean, line 86.

Erdos422.erdos_422.variants.growth_rate

Open: stated without proof.

How does \(f\) grow?

theorem erdos_422.variants.growth_rate :
    ∀ f : ℕ+ → ℕ+, IsHofstadterQ f →
    (fun n ↦ (f n : ℝ)) =O[atTop] erdos_422.variants.growth_rate.answer

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/422.lean, line 96.

Erdos422.erdos_422.variants.eventually_const

Textbook result, proved here.

Does \(f\) become stationary at some point?

No: see IsHofstadterQ.not_eventuallyConst. The statement is existential, so the answer does not depend on whether \(f(n)\) is well-defined for all \(n\).

theorem erdos_422.variants.eventually_const :
    ¬ ∃ f : ℕ+ → ℕ+, IsHofstadterQ f ∧ EventuallyConst f atTop

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/422.lean, line 133.

Erdos422.erdos_422.variants.well_defined

Open: stated without proof.

Is \(f(n)\) well-defined for all \(n\)?

theorem erdos_422.variants.well_defined : ∃ f : ℕ+ → ℕ+, IsHofstadterQ f

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/422.lean, line 141.

Sources

• FormalConjectures/ErdosProblems/422.lean at 2055e5ad
• erdosproblems.com/422

LeanErdos422.erdos_422 · Erdos422.erdos_422.variants.surjective · Erdos422.erdos_422.variants.growth_rate · Erdos422.erdos_422.variants.eventually_const · Erdos422.erdos_422.variants.well_defined

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.