Erdős Problem 472 to Erdős Problem 494
TheoremErdős Problem 472#
Reference: erdosproblems.com/472
Quoted from FormalConjectures/ErdosProblems/472.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/472.
The file states 1 research or textbook statement: 1 open.
Erdos472.erdos_472
Open: stated without proof.
Given a finite sequence of primes \(q_1\lt \cdots\lt q_m\), extend it by taking \(q_{n+1}\) to be the smallest prime of the form \(q_n+q_i-1\) for \(n\geq m\). Is there an initial sequence for which this process continues forever?
theorem erdos_472 : ∃ m : ℕ, ∃ q : ℕ → ℕ, UlamPrimeExtension m q
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/472.lean, line 56.
Sources
TheoremErdős Problem 473#
References: - erdosproblems.com/473 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique (1980).
Quoted from FormalConjectures/ErdosProblems/473.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/473.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos473.erdos_473
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos473.lean#L236.
Is there a permutation \(a_1, a_2, \ldots\) of the positive integers such that \(a_k + a_{k+1}\) is always prime?
A question of Segal [ErGr80, p.94]. The answer is yes, as shown by Odlyzko. The linked formal proof (Codex and GPT-5.6 Sol) builds the permutation as a spanning one-way ray of the graph on the positive integers in which two numbers are adjacent when their sum is prime.
theorem erdos_473 :
∃ a : ℕ ≃ ℕ+, ∀ n : ℕ, ((a n : ℕ) + (a (n + 1) : ℕ)).Prime
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/473.lean, line 45.
Erdos473.erdos_473.variants.finite
Open: stated without proof.
Segal also asked whether for every \(n \ge 2\) there is a permutation \(a_1, \ldots, a_n\) of \(\{1, \ldots, n\}\) such that \(a_k + a_{k+1}\) is prime for all \(1 \le k < n\). This is conjectured to be true, and has been verified for infinitely many \(n\).
theorem erdos_473.variants.finite :
∀ n : ℕ, 2 ≤ n → ∃ a : Fin n ≃ Fin n, ∀ k : Fin n, ∀ h : k.val + 1 < n,
((a k).val + 1 + ((a ⟨k.val + 1, h⟩).val + 1)).Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/473.lean, line 55.
Sources
TheoremErdős Problem 476#
References: - erdosproblems.com/476 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [dSHa94] Dias da Silva, J. A. and Hamidoune, Y. O., Cyclic spaces for Grassmann derivatives and additive theory. Bull. London Math. Soc. (1994), 140-146.
Quoted from FormalConjectures/ErdosProblems/476.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/476.
The file states 1 research or textbook statement: 1 solved.
Erdos476.erdos_476
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos476.lean.
Let \(A\subseteq \mathbb{F}_p\). Let
\[ A\hat{+}A = \{ a+b : a\neq b \in A\}. \]Is it true that
\[ \lvert A\hat{+}A\rvert \geq \min(2\lvert A\rvert-3,p)? \]This is the Erdős-Heilbronn inequality, proved by Dias da Silva and Hamidoune.
theorem erdos_476 :
∀ p : ℕ, Fact p.Prime → ∀ A : Finset (ZMod p),
A.restrictedSumset.card ≥ min (2 * A.card - 3) p
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/476.lean, line 52.
Sources
TheoremErdős Problem 477#
References: - erdosproblems.com/477 - Sek59 Milan Sekanina, Замечания к фактoризации беcкoнечнoй цикличеcкoй группы, Czechoslovak Mathematical Journal, Vol. 9 (1959), No. 4, 485–495 - The resolution is recorded at erdosproblems.com/477, with a proof exposition by T. F. Bloom of a construction found independently by several provers.
Quoted from FormalConjectures/ErdosProblems/477.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/477.
The file states 5 research or textbook statements: 1 open and 4 solved.
Erdos477.erdos_477
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos477.lean#L54.
Is there a polynomial \(f:\mathbb{Z}\to \mathbb{Z}\) of degree at least \(2\) and a set \(A\subset \mathbb{Z}\) such that for any \(n\in \mathbb{Z}\) there is exactly one \(a\in A\) and \(b\in \{ f(k) : k\in\mathbb{Z}\}\) such that \(n=a+b\)?
The answer is yes, contrary to the expectation of Erdős and Graham: such an
Aexists whenever \(f(n) = n^d\) for even \(d \ge 6\).The linked formal proof (Codex, following Price's exposition) exhibits a complement of \(\{k^6 : k \in \mathbb{Z}\}\); it states uniqueness as
∃! p : ℤ × ℤ, p.1 ∈ A ∧ p.2 ∈ B ∧ p.1 + p.2 = nand the degree condition as2 ≤ f.natDegree.
theorem erdos_477 :
∃ f : ℤ[X], 2 ≤ f.degree ∧ ∃ A : Set ℤ,
∀ z, ∃! ab ∈ A ×ˢ (Set.range f.eval), z = ab.1 + ab.2
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/477.lean, line 51.
Erdos477.erdos_477.variants.S_sq
Solved: stated here without proof.
There is no such \(A\) for the polynomial \(f(x) = X^2\).
This is shown in [Sek59].
theorem erdos_477.variants.S_sq :
letI f := X ^ 2
∀ A : Set ℤ, ∃ z, ¬ ∃! a ∈ A ×ˢ (Set.range f.eval), z = a.1 + a.2
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/477.lean, line 62.
Erdos477.erdos_477.variants.degree_two_dvd_condition_b_ne_zero
Solved: stated here without proof.
There is no such \(A\) for any polynomial \(f(x) = aX^2 + bX + c\), if \(a | b\) with \(a \ne 0\) and \(b \ne 0\). This was found be AlphaProof for the specific instance \(X^2 - X + 1\) and then generalised.
theorem erdos_477.variants.degree_two_dvd_condition_b_ne_zero {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0)
(hab : a ∣ b) :
let f := a • X ^ 2 + b • X + C c
∀ A : Set ℤ, ∃ z, ¬ ∃! a ∈ A ×ˢ (Set.range f.eval), z = a.1 + a.2
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/477.lean, line 73.
Erdos477.erdos_477.variants.X_pow_three
Open: stated without proof.
Probably there is no such \(A\) for the polynomial \(X^3\).
theorem erdos_477.variants.X_pow_three :
letI f := X ^ 3
∀ A : Set ℤ, ∃ z, ¬ ∃! a ∈ A ×ˢ (Set.range f.eval), z = a.1 + a.2
Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/477.lean, line 83.
Erdos477.erdos_477.variants.monomial
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos477.lean#L42.
Sekanina [Sek59] asked whether there is no such \(A\) for \(X^k\), for every \(k \ge 2\). This is false: a complement exists for every even \(k \ge 6\). The linked formal proof gives the case \(k = 6\).
theorem erdos_477.variants.monomial :
¬ ∀ (k : ℕ), 2 ≤ k →
letI f := X ^ k
∀ A : Set ℤ, ∃ z, ¬ ∃! a ∈ A ×ˢ (Set.range f.eval), z = a.1 + a.2
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/477.lean, line 96.
Sources
TheoremErdős Problem 478#
References: - erdosproblems.com/478 - [AnTa16] V. Andrejić and M. Tatarevic, On distinct residues of factorials. arXiv:1603.04086 (2016). - [GSSV24] Grebennikov, Alexandr and Sagdeev, Arsenii and Semchankau, Aliaksei and Vasilevskii, Aliaksei, On the sequence {\(n! \bmod p\)}. Rev. Mat. Iberoam. (2024), 637--648. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [KlMu17] Klurman, Oleksiy and Munsch, Marc, Distribution of factorials modulo {\(p\)}. J. Théor. Nombres Bordeaux (2017), 169--177. - [RoSc60] Rokowska, B. and Schinzel, A., Sur un problème de {M}. {E}rdős. Elem. Math. (1960), 84--85. - [Tr13] T. Trudgian, There are no socialist primes less than \(10^9\). arXiv:1310.6403 (2013).
Quoted from FormalConjectures/ErdosProblems/478.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/478.
The file states 1 research or textbook statement: 1 open.
Erdos478.erdos_478
Open: stated without proof.
Let \(p\) be a prime and
\[A_p = \{ k! \pmod{p} : 1\leq k\lt p\}.\]Is it true that
\[\lvert A_p\rvert \sim (1-\tfrac{1}{e})p?\]
theorem erdos_478 :
Filter.Tendsto
(fun p : ℕ =>
(((Finset.Ico 1 p).image (fun k => Nat.factorial k % p)).card : ℝ) / p)
(Filter.atTop ⊓ Filter.principal {p : ℕ | p.Prime})
(nhds (1 - 1 / Real.exp 1))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/478.lean, line 45.
Sources
TheoremErdős Problem 479#
Reference: erdosproblems.com/479
Quoted from FormalConjectures/ErdosProblems/479.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/479.
The file states 1 research or textbook statement: 1 open.
Erdos479.erdos_479
Open: stated without proof.
Is it true that, for every integer \(k\neq 1\), there are infinitely many \(n\) such that \(2^n\equiv k\pmod{n}\)?
theorem erdos_479 : ∀ᵉ (k : ℤ) (k ≠ 1),
{ n : ℕ | (2 : ℤ) ^ n ≡ k [ZMOD (n : ℤ)] }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/479.lean, line 35.
Sources
TheoremErdős Problem 480#
Reference: erdosproblems.com/480
Quoted from FormalConjectures/ErdosProblems/480.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/480.
The file states 3 research or textbook statements: 3 solved.
Erdos480.erdos_480
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos480.lean#L973.
Let \(x_1,x_2,\ldots\in [0,1]\) be an infinite sequence. Is it true that
\[\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq 5^{-1/2}\approx 0.447?\]A conjecture of Newman.
theorem erdos_480 : ∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
⨅ (n : ℕ+), atTop.liminf (fun m => (n : ℕ) * |x (m + (n : ℕ)) - x m|) ≤ 1 / √5
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/480.lean, line 40.
Erdos480.erdos_480.variants.chung_graham
Solved: stated here without proof.
This was proved by Chung and Graham \cite{ChGr84}, who in fact prove that
\[\inf_n \liminf_{m\to \infty} n \lvert x_{m+n}-x_m\rvert\leq \frac{1}{c}\approx 0.3944\]where
\[c=1+\sum_{k\geq 1}\frac{1}{F_{2k}}=2.5353705\cdots\]and \(F_m\) is the \(m\)th Fibonacci number.
theorem erdos_480.variants.chung_graham :
let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
⨅ (n : ℕ+), atTop.liminf (fun m => (n : ℕ) * |x (m + (n : ℕ)) - x m|) ≤ 1 / c
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/480.lean, line 52.
Erdos480.erdos_480.variants.chung_graham_best_possible
Solved: stated here without proof.
They also prove that this constant is best possible.
theorem erdos_480.variants.chung_graham_best_possible :
let c : ℝ := 1 + ∑' (k : ℕ+), (1 : ℝ) / (2*k : ℕ).fib
∀ ε > (0 : ℝ), ¬ (∀ (x : ℕ → ℝ), (∀ n, x n ∈ Set.Icc 0 1) →
⨅ (n : ℕ+), atTop.liminf (fun m => (n : ℕ) * |x (m + (n : ℕ)) - x m|) ≤ 1 / c - ε)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/480.lean, line 62.
Sources
TheoremErdős Problem 481#
References: - erdosproblems.com/481 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980), p.96. - [Kl82] Klarner, David A., A sufficient condition for certain semigroups to be free. J. Algebra (1982), 140-148. - [KoTa22] Kolpakov, Alexander and Talambutsa, Alexey, On free semigroups of affine maps on the real line. Proc. Amer. Math. Soc. (2022), 2301-2307.
Quoted from FormalConjectures/ErdosProblems/481.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/481.
The file states 1 research or textbook statement: 1 solved.
Erdos481.erdos_481
Solved: stated here without proof.
Let \(a_1,\ldots,a_r,b_1,\ldots,b_r\in \mathbb{N}\) such that \(\sum_{i}\frac{1}{a_i}>1\). For any finite sequence of \(n\) (not necessarily distinct) integers \(A=(x_1,\ldots,x_n)\) let \(T(A)\) denote the sequence of length \(rn\) given by
\[(a_ix_j+b_i)_{1\leq j\leq n, 1\leq i\leq r}.\]Prove that, if \(A_1=(1)\) and \(A_{i+1}=T(A_i)\), then there must be some \(A_k\) with repeated elements.
This is true. This appears to have first been shown by Klarner [Kl82], with a generalisation given by Kolpakov and Talambutsa [KoTa22]. Essentially the same proof was found independently by Barreto in the comment section.
theorem erdos_481 {r : ℕ} (a b : Fin r → ℕ) (ha : ∀ i, 0 < a i)
(hab : 1 < ∑ i, (1 : ℝ) / a i) :
∃ k, ¬ ((T a b)^[k] [1]).Nodup
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/481.lean, line 57.
Sources
TheoremErdős Problem 482#
References: - erdosproblems.com/482 - [GrPo70] Graham, R. L. and Pollak, H. O., Note on a nonlinear recurrence related to {\(\surd 2\)}. Math. Mag. (1970), 143-145. - [St05] Stoll, Th., On families of nonlinear recurrences related to digits. J. Integer Seq. (2005), Article 05.3.2, 8. - [St06] Stoll, Thomas, On a problem of Erd\H{o}s and Graham concerning digits. Acta Arith. (2006), 89-100. - [RaGi91] Rabinowitz, S. and Gilbert, P., A nonlinear recurrence yielding binary digits. Math. Mag. 64 (1991), 168-171.
A formal Lean proof is given in an external repository,
gotrevor/lean-gallery, formalized by Trevor Morris with Claude Code.
Quoted from FormalConjectures/ErdosProblems/482.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/482.
The file states 4 research or textbook statements: 4 solved.
Erdos482.erdos_482
Solved: stated here; a Lean proof is at https://github.com/gotrevor/lean-gallery/blob/a28a487968d989b24c9dde9b1958aa5b92c6fccb/LeanGallery/NumberTheory/Erdos482/Statement.lean#L46-L49.
Define a sequence by \(a_1=1\) and
\[a_{n+1}=\lfloor\sqrt{2}(a_n+1/2)\rfloor\]for \(n\geq 1\). The difference \(a_{2n+1}-2a_{2n-1}\) is the \(n\)th digit in the binary expansion of \(\sqrt{2}\).
Find similar results for \(\theta=\sqrt{m}\), and other algebraic numbers.
The result for \(\sqrt{2}\) was obtained by Graham and Pollak [GrPo70]. The problem statement is open-ended, but presumably Erdős and Graham would have been satisfied with the wide-ranging generalisations of Stoll ([St05] and [St06]).
The binary expansion is \(\sqrt{2} = 1.0110101\ldots\), and the \(n\)th digit counts the leading \(1\) as digit \(1\). It is stated with Mathlib's
Real.digits: the \(n\)th digit of \(\sqrt{2}\) is digit \(n - 1\) of \(\sqrt{2}/2 = 0.10110101\ldots\), that is \(\lfloor \sqrt{2} \cdot 2^{n-1} \rfloor \bmod 2\). The second conjunct records that these digits are the binary expansion: they reconstruct \(\sqrt{2}/2\).
theorem erdos_482 :
(∀ n : ℕ, 1 ≤ n →
(a (2 * n + 1) : ℤ) - 2 * a (2 * n - 1) = (Real.digits (√2 / 2) 2 (n - 1) : ℕ)) ∧
Real.ofDigits (Real.digits (√2 / 2) 2) = √2 / 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/482.lean, line 73.
Erdos482.erdos_482.variants.stoll_general
Solved: stated here; a Lean proof is at https://github.com/gotrevor/lean-gallery/blob/a834bbad2f36eedcc16066b2bc4da49f98ab5b85/LeanGallery/NumberTheory/Erdos482/Statement.lean#L64-L67.
Stoll's general answer to the open-ended part [St05]: for every real \(w > 0\) and every base \(g \ge 2\), there are parameters \(a\), \(b\), and \(\varepsilon\), with \(ab = g\), such that the corresponding Graham–Pollak-type recurrence reads the base-\(g\) digits of \(w\).
The mantissa normalization is \(w / g^{\lfloor \log_g w \rfloor}\), so the right-hand side is the standard Mathlib base-\(g\) digit of the normalized expansion.
theorem erdos_482.variants.stoll_general (g : ℕ) [NeZero g] (hg : 2 ≤ g) (w : ℝ) (hw : 0 < w) :
∃ a b ε : ℝ, a * b = g ∧
∀ n : ℕ, 1 ≤ n →
generalRecurrence g a b ε (2 * n) - g * generalRecurrence g a b ε (2 * n - 2) =
(Real.digits (w / (g : ℝ) ^ ⌊Real.logb g w⌋ * (g : ℝ) ^ (n - 1) / g) g 0 : ℕ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/482.lean, line 89.
Erdos482.erdos_482.variants.binary_explicit
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/33a6b9a285cb64ac276ce4d0b3a4111b82c972b6/src/latest/ErdosProblems/Erdos482.lean#L323-L332.
The explicit binary answer to the open-ended part [RaGi91], [St05]: for every normalized real \(t \in [1, 2)\), the recurrence with coefficients \(\alpha(t) = 2(t+1)/(t+2)\) and \(\beta(t) = (t+2)/(t+1)\) reads off the binary digits of \(t\), and those digits reconstruct \(t\). Unlike
erdos_482.variants.stoll_general, the coefficients are given, not merely shown to exist.
theorem erdos_482.variants.binary_explicit (t : ℝ) (ht1 : 1 ≤ t) (ht2 : t < 2) :
(∀ n, 1 ≤ n →
stollBinary t (2 * n) - 2 * stollBinary t (2 * n - 2) = (binaryDigit t n).val) ∧
Real.ofDigits (fun k ↦ binaryDigit t (k + 2)) = t - 1
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/482.lean, line 125.
Erdos482.erdos_482.variants.stoll_explicit
Solved: stated here without proof.
The explicit base-\(g\) construction in Stoll [St05, Theorem 1.3]. For a normalized \(t \in [1,g)\), take \(a = g/((g-1)(t+g))\) and \(b = (g-1)(t+g)\). Every parameter \(-1/g \le \varepsilon < (g+1)(g-2)/g\) gives the same significant digits of \(t\).
The sequence is indexed from zero, so the difference at \(2n+2\) and \(2n\) gives digit \(n\), including the leading digit at \(n=0\). The floor difference uses the terminating expansion when \(t\) has two base-\(g\) expansions.
theorem erdos_482.variants.stoll_explicit (g : ℕ) (hg : 2 ≤ g) (t : ℝ)
(ht : 1 ≤ t) (htg : t < g) (ε : ℝ)
(hεlo : -1 / (g : ℝ) ≤ ε)
(hεhi : ε < ((g : ℝ) + 1) * ((g : ℝ) - 2) / g) :
let a := (g : ℝ) / (((g : ℝ) - 1) * (t + g))
let b := ((g : ℝ) - 1) * (t + g)
∀ n : ℕ,
generalRecurrence g a b ε (2 * n + 2) -
(g : ℤ) * generalRecurrence g a b ε (2 * n) =
⌊t * (g : ℝ) ^ n⌋ - (g : ℤ) * ⌊t * (g : ℝ) ^ n / g⌋
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/482.lean, line 139.
Sources
TheoremErdős Problem 483#
References: - erdosproblems.com/483 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254, p.233, Problem 20.
Quoted from FormalConjectures/ErdosProblems/483.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/483.
The file states 1 research or textbook statement: 1 open. It also has 2 test statements, counted here but not shown.
Erdos483.erdos_483
Open: stated without proof.
Let \(f(k)\) be the minimal \(N\) such that if \(\{1,\ldots,N\}\) is \(k\)-coloured then there is a monochromatic solution to \(a+b=c\). Estimate \(f(k)\). In particular, is it true that \(f(k) < c^k\) for some constant \(c>0\)?
The exponential bound is stated directly: for every positive number of colours, there is a forcing interval of length strictly below \(c^k\). This is equivalent to the bound on the least forcing threshold and avoids choosing a default value for that threshold.
theorem erdos_483 :
∃ C : ℝ, 0 < C ∧ ∀ k : ℕ, 0 < k →
∃ N : ℕ, (N : ℝ) < C ^ k ∧ Forces k N
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/483.lean, line 64.
Sources
TheoremErdős Problem 484#
References: - erdosproblems.com/484 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115. - [ESS89] Erdős, P., Sárközy, A., and Sós, V. T., On a conjecture of Roth and some related problems. I. (1989), 47-59.
Quoted from FormalConjectures/ErdosProblems/484.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/484.
The file states 1 research or textbook statement: 1 solved.
Erdos484.erdos_484
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos484.lean.
Prove that there exists an absolute constant \(c>0\) such that, whenever \(\{1,\ldots,N\}\) is \(k\)-coloured (and \(N\) is large enough depending on \(k\)) then there are at least \(cN\) many integers in \(\{1,\ldots,N\}\) which are representable as a monochromatic sum (that is, \(a+b\) where \(a,b\in \{1,\ldots,N\}\) are in the same colour class and \(a\neq b\)).
A conjecture of Roth. Solved by Erdős, Sárközy, and Sós [ESS89], who in fact prove that there are at least \(\frac{N}{2}-O(N^{1-1/2^{k+1}})\) many even numbers which are of this form.
theorem erdos_484 :
∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 0 < k → ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ f : ℕ → Fin k,
c * N ≤ (((Finset.Icc 1 N).filter fun n =>
∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N,
a ≠ b ∧ f a = f b ∧ a + b = n).card : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/484.lean, line 49.
Sources
TheoremErdős Problem 485#
References: - erdosproblems.com/485 - [Re47] Rényi, A., On the minimal number of terms of the square of a polynomial. Hungarica Acta Math. (1947), 30-34. - [Er49b] Erdős, P., On the number of terms of the square of a polynomial. Nieuw Arch. Wiskunde (2) (1949), 63-65. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [Sc87] Schinzel, A., On the number of terms of a power of a polynomial. Acta Arith. (1987), 55-70. - [ScZa09] Schinzel, Andrzej and Zannier, Umberto, On the number of terms of a power of a polynomial. Atti Accad. Naz. Lincei Rend. Lincei Mat. Appl. (2009), 95-98.
Quoted from FormalConjectures/ErdosProblems/485.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/485.
The file states 1 research or textbook statement: 1 solved.
Erdos485.erdos_485
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos485.lean#L39.
Let \(f(k)\) be the minimum number of terms in \(P(x)^2\), where \(P \in \mathbb{Q}[x]\) ranges over all polynomials with exactly \(k\) non-zero terms. Is it true that \(f(k) \to \infty\) as \(k \to \infty\)?
A conjecture of Erdős and Rényi (this is Problem 4.4 in [Ha74], attributed to Erdős); the function was first investigated by Rényi and Rédei [Re47], and Erdős [Er49b] proved that \(f(k) < k^{1-c}\) for some \(c > 0\). The answer is yes: Schinzel [Sc87] proved \(f(k) > \log \log k / \log 2\), and Schinzel and Zannier [ScZa09] improved this to \(f(k) \gg \log k\).
theorem erdos_485 : Tendsto f atTop atTop
Category research solved; AMS 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/ErdosProblems/485.lean, line 63.
Sources
TheoremErdős Problem 486: Logarithmic density for sets avoiding modular subsets#
References: * erdosproblems.com/486 * [Wa26] Wang, S., A proposed solution to Erdős Problem 486 (2026), https://github.com/ShouqiaoW/erdos/blob/main/486/paper.pdf
Quoted from FormalConjectures/ErdosProblems/486.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/486.
The file states 1 research or textbook statement: 1 solved.
Erdos486.erdos_486
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos486.lean#L20; a Lean proof is at https://github.com/Konamiu/formal-conjectures/blob/c69df0584ca9767090f5a68c8f09f1ff3c93ab80/FormalConjectures/ErdosProblems/486.lean#L39.
Let \(A \subseteq \mathbb{N}\), and for each \(n \in A\) choose some \(X_n \subseteq \mathbb{Z}/n\mathbb{Z}\). Let \(B = \{m \in \mathbb{N} : m \not\in X_n \pmod{n} \text{ for all } n \in A \text{ with } m > n\}\). Must \(B\) have a logarithmic density?
The set \(A\) is encoded by taking \(X_n = \emptyset\) for \(n \notin A\). Only positive moduli \(n\) are considered, since \(\mathbb{Z}/0\mathbb{Z} = \mathbb{Z}\) would allow \(B\) to be an arbitrary set.
The answer is no: Wang [Wa26] (with GPT-5.6) constructed a congruence system whose survivor set \(B\) has lower logarithmic density at most \(177/200\) and upper logarithmic density at least \(49/50\). The first linked formal proof establishes this for the real-cutoff normalisation \(\frac{1}{\log x}\sum_{m < x, m \in B} \frac{1}{m}\) with the moduli restricted to \(A\); the second derives the statement below (
Set.HasLogDensity, all moduli) from it.
theorem erdos_486 :
¬ ∀ X : (n : ℕ) → Set (ZMod n),
∃ d, {m : ℕ | ∀ n, 0 < n → n < m → (m : ZMod n) ∉ X n}.HasLogDensity d
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/486.lean, line 55.
Sources
TheoremErdős Problem 487#
References: - erdosproblems.com/487 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [DaEr36] Davenport, H. and Erdős, P., On sequences of positive integers. Acta Arithmetica (1936), 147-151. - [Kl71] Kleitman, Daniel, Collections of subsets containing no two sets and their union. Proceedings of the LA Meeting AMS (1971), 153-155.
Quoted from FormalConjectures/ErdosProblems/487.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/487.
The file states 1 research or textbook statement: 1 solved.
Erdos487.erdos_487
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos487.lean.
Let \(A\subseteq \mathbb{N}\) have positive density. Must there exist distinct \(a,b,c\in A\) such that \([a,b]=c\) (where \([a,b]\) is the least common multiple of \(a\) and \(b\))?
This is true, a consequence of the positive solution to [447] by Kleitman [Kl71].
Davenport and Erdős [DaEr36] showed that there must exist an infinite sequence \(a_1\lt a_2\cdots\) in \(A\) such that \(a_i\mid a_j\) for all \(i\leq j\), under the assumption that the upper logarithmic density of \(A\) is positive.
theorem erdos_487 :
∀ A : Set ℕ, A.HasPosDensity →
∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ Nat.lcm a b = c
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/487.lean, line 51.
Sources
TheoremErdős Problem 488#
Reference: erdosproblems.com/488
Quoted from FormalConjectures/ErdosProblems/488.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/488.
The file states 1 research or textbook statement: 1 open.
Erdos488.erdos_488
Open: stated without proof.
Let \(A\) be a finite set and
\[B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.\]Is it true that, for every \(m>n\geq \max(A)\),
\[\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?\]
theorem erdos_488 : ∀ (A : Finset ℕ), A.Nonempty →
-- These are needed for the reasons outlined here: https://github.com/google-deepmind/formal-conjectures/pull/256
0 ∉ A → 1 ∉ A →
letI B := {n ≥ 1 | ∃ a ∈ A, a ∣ n}
∀ᵉ (n : ℕ) (m > n), A.max ≤ n →
((Finset.Icc 1 m).filter (· ∈ B)).card / (m : ℚ) <
2 * ((Finset.Icc 1 n).filter (· ∈ B)).card / n
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/488.lean, line 38.
Sources
TheoremErdős Problem 489#
Reference: erdosproblems.com/489
Quoted from FormalConjectures/ErdosProblems/489.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/489.
The file states 2 research or textbook statements: 2 solved.
Erdos489.erdos_489
Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-489/F061/Erdos489.lean.
Let \(A\subseteq \mathbb{N}\) be a set such that \(\lvert A\cap [1,x]\rvert=o(x^{1/2})\). Let \(B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}\). If \(B=\{b_1 < b_2 < \cdots\}\) then is it true that
\[\lim_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2\]exists (and is finite)?
For example, when \(A=\{p^2: p\textrm{ prime}\}\) then \(B\) is the set of squarefree numbers, and the existence of this limit was proved by Erdős.
See also [208].
theorem erdos_489 :
∀ (A : Set ℕ),
(fun x : ℕ => (((Finset.Icc 1 x).filter (· ∈ A)).card : ℝ)) =o[atTop]
(fun x : ℕ => (x : ℝ).sqrt) →
(sievedSet A).Infinite →
∃ L : ℝ, Tendsto (fun x : ℕ => GapSumSq A x / (x : ℝ)) atTop (𝓝 L)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/489.lean, line 59.
Erdos489.erdos_489.variants.squarefree
Solved: stated here without proof.
When \(A = \{p^2 : p \textrm{ prime}\}\), \(B\) is the set of squarefree numbers, and the existence of this limit was proved by Erdős. This is the \(\alpha = 2\) case of Erdős Problem 145.
theorem erdos_489.variants.squarefree :
∃ L : ℝ, Tendsto
(fun x : ℕ => GapSumSq {n | ∃ p, Nat.Prime p ∧ n = p ^ 2} x / (x : ℝ))
atTop (𝓝 L)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/489.lean, line 70.
Sources
TheoremErdős Problem 490#
References: - erdosproblems.com/490 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er69] Erdős, Paul, Some applications of graph theory to number theory. The Many Facets of Graph Theory (Proc. Conf., Western Mich. Univ., Kalamazoo, Mich., 1968) (1969), 77-82. - [Er72] Erdős, Paul, Extremal problems in number theory. Proceedings of the 1972 Number Theory Conference (Univ. Colorado, Boulder, Colo.) (1972), 80-86. - [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. - [Sz76] Szemerédi, E., On a problem of P. Erdős. J. Number Theory (1976), 264-270.
Quoted from FormalConjectures/ErdosProblems/490.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/490.
The file states 2 research or textbook statements: 1 open and 1 solved.
Erdos490.erdos_490
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos490.lean#L38.
Let \(A,B\subseteq \{1,\ldots,N\}\) be such that all the products \(ab\) with \(a\in A\) and \(b\in B\) are distinct. Is it true that
\[\lvert A\rvert \lvert B\rvert \ll \frac{N^2}{\log N}?\]This would be best possible, for example letting \(A=[1,N/2]\cap \mathbb{N}\) and \(B=\{ N/2\lt p\leq N: p\textrm{ prime}\}\). This is true, and was proved by Szemerédi [Sz76].
In [Er72] Erdős goes on to ask whether
\[\lim_{N\to \infty}\max_{A,B\subseteq [N]}\frac{\lvert A\rvert\lvert B\rvert\log N}{N^2}\]exists, where the maximum is over \(A\) and \(B\) with all the products \(ab\) distinct, and to determine its value. As noted in the comments to 896 by van Doorn, if the limit exists it must be \(\geq 1\).
theorem erdos_490 : ∃ C : ℝ, ∀ᶠ N : ℕ in atTop,
∀ A B : Finset ℕ, A ⊆ Finset.Icc 1 N → B ⊆ Finset.Icc 1 N →
(∀ a₁ ∈ A, ∀ b₁ ∈ B, ∀ a₂ ∈ A, ∀ b₂ ∈ B, a₁ * b₁ = a₂ * b₂ → a₁ = a₂ ∧ b₁ = b₂) →
(A.card * B.card : ℝ) ≤ C * N ^ 2 / Real.log N
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/490.lean, line 62.
Erdos490.erdos_490.variants.limit
Open: stated without proof.
Erdős [Er72] asks whether
\[\lim_{N\to \infty}\max_{A,B\subseteq [N]}\frac{\lvert A\rvert\lvert B\rvert\log N}{N^2}\]exists, where the maximum is over \(A\) and \(B\) with all the products \(ab\) distinct, and to determine its value.
theorem erdos_490.variants.limit : ∃ L : ℝ, Tendsto (fun N : ℕ =>
(sSup {x : ℝ | ∃ A B : Finset ℕ, A ⊆ Finset.Icc 1 N ∧ B ⊆ Finset.Icc 1 N ∧
(∀ a₁ ∈ A, ∀ b₁ ∈ B, ∀ a₂ ∈ A, ∀ b₂ ∈ B, a₁ * b₁ = a₂ * b₂ → a₁ = a₂ ∧ b₁ = b₂) ∧
x = A.card * B.card}) * Real.log N / N ^ 2) atTop (nhds L)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/490.lean, line 75.
Sources
TheoremErdős Problem 491#
References: - erdosproblems.com/491 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er82e] Erdős, Paul, Some of my favourite problems which recently have been solved. (1982), 59--79. - [Wi70] E. Wirsing, A characterization of \(\log n\) as an additive arithmetic function. Symposia Math. (1970), 45-57.
Quoted from FormalConjectures/ErdosProblems/491.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/491.
The file states 1 research or textbook statement: 1 solved.
Erdos491.erdos_491
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos491.lean#L34.
Let \(f : \mathbb{N} \to \mathbb{R}\) be an additive function (so that \(f(ab) = f(a) + f(b)\) whenever \((a, b) = 1\)). If \(|f(n+1) - f(n)| < c\) for some constant \(c\) and all \(n\), then must there exist some \(c'\) such that \(f(n) = c' \log n + O(1)\)?
A question of Erdős [Er61, p.237; Er82e, p.65], who had proved that \(f(n) = c' \log n\) under the stronger hypotheses \(f(n+1) - f(n) = o(1)\) or \(f(n+1) \ge f(n)\). The answer is yes, proved by Wirsing [Wi70]. See also
erdos_897.variants.log_growth.
theorem erdos_491 :
∀ (f : ℕ → ℝ), (∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
(∃ C : ℝ, ∀ n : ℕ, |f (n + 1) - f n| < C) →
∃ c : ℝ, (fun n : ℕ ↦ f n - c * Real.log n) =O[atTop] (fun _ : ℕ ↦ (1 : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/491.lean, line 52.
Sources
TheoremErdős Problem 493#
References: - erdosproblems.com/493 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
Quoted from FormalConjectures/ErdosProblems/493.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/493.
The file states 1 research or textbook statement: 1 solved.
Erdos493.erdos_493
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos493.lean.
Does there exist a \(k\) such that every sufficiently large integer can be written in the form
\[\prod_{i=1}^k a_i - \sum_{i=1}^k a_i\]for some integers \(a_i\geq 2\)?
Erdős attributes this question to Schinzel. Eli Seamans has observed that the answer is yes (with \(k=2\)) for a very simple reason: \(n = 2(n+2)-(2+(n+2))\). There may well have been some additional constraint in the problem as Schinzel posed it, but [Er61] does not record what this is.
theorem erdos_493 :
∃ k : ℕ, ∃ N : ℤ, ∀ n : ℤ, N ≤ n →
∃ a : Fin k → ℤ,
(∀ i : Fin k, (2 : ℤ) ≤ a i) ∧
(∏ i : Fin k, a i) - (∑ i : Fin k, a i) = n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/493.lean, line 41.
Sources
TheoremErdős Problem 494#
References: - erdosproblems.com/494 - [SeSt58] Selfridge, J. L. and Straus, E., On the determination of numbers by their sums of a fixed order. Pacific Journal of Math. (1958), 847-856. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [GFS62] Gordon, B. and Fraenkel, A. S. and Straus, E. G., On the determination of sets by the sets of sums of a certain order. Pacific J. Math. (1962), 187--196. - [FoIz94] Fomin, D. V. and Izhboldin, O. T., Sets of multiple sums. Proc. St. Petersburg Math. Soc. 3 (1994), 244-259.
Quoted from FormalConjectures/ErdosProblems/494.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/494.
The file states 9 research or textbook statements: 9 solved.
Erdos494.erdos_494.variants.k_eq_2_card_not_pow_two
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/a2d6dcb99d4f11469cbb40c18959357031786c4c/erdos-494/Solution.lean#L26.
Selfridge and Straus [SeSt58] showed that the conjecture is true when \(k = 2\) and \(|A| \ne 2^l\) for \(l \ge 0\). They also gave counterexamples when \(k = 2\) and \(|A| = 2^l\).
theorem erdos_494.variants.k_eq_2_card_not_pow_two :
∀ card : ℕ, (∀ l : ℕ, card ≠ 2 ^ l) → Erdos494Unique 2 card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 59.
Erdos494.erdos_494.variants.k_eq_2_card_pow_two
Solved: stated here; a Lean proof is at https://github.com/hjyuh/formal-conjectures/blob/e0da6ec78953b17618895a093d4bee90fd3f6f67/FormalConjectures/ErdosProblems/494.lean#L533.
Selfridge and Straus [SeSt58] gave counterexamples to the conjecture when \(k = 2\) and \(|A| = 2^l\).
theorem erdos_494.variants.k_eq_2_card_pow_two :
∀ card : ℕ, (∃ l : ℕ, card = 2 ^ l) → ¬Erdos494Unique 2 card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 71.
Erdos494.erdos_494.variants.k_eq_3_card_gt_6
Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/a2d6dcb99d4f11469cbb40c18959357031786c4c/erdos-494/Solution.lean#L30.
Selfridge and Straus [SeSt58] also showed that the conjecture is true when 1) \(k = 3\) and \(|A| > 6\), except possibly for \(|A| = 27\) and \(|A| = 486\), or 2) \(k = 4\) and \(|A| > 12\). More generally, they proved that \(A\) is determined by \(A_k\) (and \(|A|\)) if \(|A|\) is divisible by a prime greater than \(k\).
The cases \(|A| = 27\) and \(|A| = 486\) were left open in [SeSt58]. Fomin and Izhboldin [FoIz94] later found two distinct sets of each of these sizes with the same multiset of \(3\)-sums, so these exceptions are genuine.
theorem erdos_494.variants.k_eq_3_card_gt_6 :
∀ card > 6, card ≠ 27 → card ≠ 486 → Erdos494Unique 3 card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 89.
Erdos494.erdos_494.variants.k_eq_4_card_gt_12
Solved: stated here without proof.
Selfridge and Straus [SeSt58] showed that the conjecture is true when \(k = 4\) and \(|A| > 12\).
theorem erdos_494.variants.k_eq_4_card_gt_12 :
∀ card > 12, Erdos494Unique 4 card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 98.
Erdos494.erdos_494.variants.card_divisible_by_prime_gt_k
Solved: stated here without proof.
Selfridge and Straus [SeSt58] proved that \(A\) is determined by \(A_k\) if \(|A|\) is divisible by a prime greater than \(k\).
theorem erdos_494.variants.card_divisible_by_prime_gt_k :
∀ (k card p : ℕ), p.Prime → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494Unique k card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 107.
Erdos494.erdos_494.variants.k_eq_card
Solved: stated here; a Lean proof is at https://github.com/hjyuh/formal-conjectures/blob/e0da6ec78953b17618895a093d4bee90fd3f6f67/FormalConjectures/ErdosProblems/494.lean#L592.
Kruyt noted that the conjecture fails when \(|A| = k\), by rotating \(A\) around an appropriate point.
theorem erdos_494.variants.k_eq_card :
∀ k > 2, ¬Erdos494Unique k k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 118.
Erdos494.erdos_494.variants.card_eq_2k
Solved: stated here; a Lean proof is at https://github.com/hjyuh/formal-conjectures/blob/e0da6ec78953b17618895a093d4bee90fd3f6f67/FormalConjectures/ErdosProblems/494.lean#L916.
Similarly, Tao noted that the conjecture fails when \(|A| = 2k\), by taking \(A\) to be a set of the total sum 0 and considering \(-A\).
theorem erdos_494.variants.card_eq_2k :
∀ k > 2, ¬Erdos494Unique k (2 * k)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 130.
Erdos494.erdos_494.variants.gordon_fraenkel_straus
Solved: stated here without proof.
Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all \(k > 2\) when \(|A|\) is sufficiently large.
theorem erdos_494.variants.gordon_fraenkel_straus :
∀ k > 2, ∀ᶠ card in atTop, Erdos494Unique k card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 139.
Erdos494.erdos_494.variants.product
Solved: stated here; a Lean proof is at https://github.com/hjyuh/formal-conjectures/blob/e0da6ec78953b17618895a093d4bee90fd3f6f67/FormalConjectures/ErdosProblems/494.lean#L951.
A counterexample to the product version of the conjecture (by Steinerberger).
theorem erdos_494.variants.product :
∃ (A B : Finset ℂ), A.card = B.card ∧ prodMultiset A 3 = prodMultiset B 3 ∧
A ≠ B
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/494.lean, line 156.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.