diff --git a/FormalConjectures/ErdosProblems/164.lean b/FormalConjectures/ErdosProblems/164.lean new file mode 100644 index 0000000000..021eaea941 --- /dev/null +++ b/FormalConjectures/ErdosProblems/164.lean @@ -0,0 +1,64 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 164 + +*References:* +- [erdosproblems.com/164](https://www.erdosproblems.com/164) +- [Er76g] Erdős, P., *Problems and results on combinatorial number theory. II*. J. Indian Math. Soc. + (N.S.) (1976), 285-298. +- [Er86] Erdős, P., *Problémes et résultats en théorie des nombres*. (1986). +- [Va99] Various, *Some of Paul's favorite problems*. Booklet produced for the conference "Paul + Erdős and his mathematics", Budapest, July 1999 (1999). +- [ABLLPSTT26] B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, and + T. Tao, *Primitive sets and Von Mangoldt Chains: Erdős problem #1196 and beyond*. + arXiv:2605.00301 (2026). +- [Er35] Erdős, Paul, *Note on Sequences of Integers No One of Which is Divisible By Any Other*. + J. London Math. Soc. (1935), 126-128. +- [Li23] Lichtman, J. D., *A proof of the Erdős primitive set conjecture*. arXiv:2202.02384 (2023). +-/ + +namespace Erdos164 + +/-- A set `A ⊆ ℕ` is *primitive* if no member of `A` divides another. -/ +def IsPrimitive (A : Set ℕ) : Prop := + ∀ a ∈ A, ∀ b ∈ A, a ∣ b → a = b + +/-- +A set $A\subset \mathbb{N}$ is primitive if no member of $A$ divides another. Is the sum +\[\sum_{n\in A}\frac{1}{n\log n}\] +maximised over all primitive sets when $A$ is the set of primes? + +Erdős [Er35] proved that this sum always converges for a primitive set. Lichtman [Li23] proved +that the answer is yes. An alternative, simpler, proof is given by Alexeev, Barreto, Li, Lichtman, +Price, Shah, Tang, and Tao [ABLLPSTT26]. + +Following the convention of [Li23] we require the members of a primitive set to be greater than +one; this excludes $A = \{1\}$, for which the summand $\frac{1}{1\cdot\log 1}$ is not defined. +-/ +@[category research solved, AMS 11, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos164.lean"] +theorem erdos_164 : answer(True) ↔ + IsPrimitive {p : ℕ | p.Prime} ∧ + ∀ A : Set ℕ, (∀ a ∈ A, 2 ≤ a) → IsPrimitive A → + (∑' a : A, 1 / ((a : ℕ) * Real.log (a : ℕ))) ≤ + ∑' p : {p : ℕ | p.Prime}, 1 / ((p : ℕ) * Real.log (p : ℕ)) := by + sorry + +end Erdos164 diff --git a/FormalConjectures/ErdosProblems/24.lean b/FormalConjectures/ErdosProblems/24.lean new file mode 100644 index 0000000000..10141f1457 --- /dev/null +++ b/FormalConjectures/ErdosProblems/24.lean @@ -0,0 +1,59 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 24 + +*References:* +- [erdosproblems.com/24](https://www.erdosproblems.com/24) +- [Er90] Erdős, Paul, *Some of my favourite unsolved problems*. A tribute to Paul Erdős (1990), + 467-478. +- [Er97b] Erdős, Paul, *Some old and new problems in various branches of combinatorics*. Discrete + Math. (1997), 227-231. +- [Er92b] Erdős, Paul, *Some of my favourite problems in various branches of combinatorics*. + Matematiche (Catania) (1992), 231-240. +- [Er97f] Erdős, Paul, *Some unsolved problems*. Combinatorics, geometry and probability + (Cambridge, 1993) (1997), 1-10. +- [Gr12] Grzesik, Andrzej, *On the maximum number of five-cycles in a triangle-free graph*. + J. Combin. Theory Ser. B (2012), 1061-1066. +- [HHKNR13] Hatami, Hamed and Hladký, Jan and Kráľ, Daniel and Norine, Serguei and Razborov, + Alexander, *On the number of pentagons in triangle-free graphs*. J. Combin. Theory Ser. A + (2013), 722-732. +-/ + +open SimpleGraph + +namespace Erdos24 + +/-- +Does every triangle-free graph on $5n$ vertices contain at most $n^5$ copies of $C_5$? + +Győri proved this with $1.03n^5$, which has been improved by Füredi. The answer is yes, as proved +independently by Grzesik [Gr12] and Hatami, Hladky, Král, Norine, and Razborov [HHKNR13]. + +Copies of $C_5$ are counted as subgraphs isomorphic to the cycle graph on five vertices, +i.e. by `SimpleGraph.copyCount`. +-/ +@[category research solved, AMS 5, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos24.lean"] +theorem erdos_24 : answer(True) ↔ + ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 → + G.copyCount (cycleGraph 5) ≤ n ^ 5 := by + sorry + +end Erdos24 diff --git a/FormalConjectures/ErdosProblems/314.lean b/FormalConjectures/ErdosProblems/314.lean new file mode 100644 index 0000000000..dd937c3e81 --- /dev/null +++ b/FormalConjectures/ErdosProblems/314.lean @@ -0,0 +1,63 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 314 + +*References:* +- [erdosproblems.com/314](https://www.erdosproblems.com/314) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [LiSt24] J. Lim and Steinerberger, S., *On differences of two harmonic numbers*. + arXiv:2405.11354 (2024). +-/ + +open Filter + +namespace Erdos314 + +/-- The block harmonic sum $\sum_{n\leq k\leq m}\frac{1}{k}$. -/ +noncomputable def harmonicSum (n m : ℕ) : ℝ := ∑ k ∈ Finset.Icc n m, (1 : ℝ) / k + +/-- `mMin n` is the minimal `m` such that $\sum_{n\leq k\leq m}\frac{1}{k}\geq 1$; such an `m` +exists for `n ≥ 1` since the harmonic series diverges. -/ +noncomputable def mMin (n : ℕ) : ℕ := sInf {m | 1 ≤ harmonicSum n m} + +/-- $\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1$, the overshoot of the minimal block sum +reaching $1$. -/ +noncomputable def epsilon (n : ℕ) : ℝ := harmonicSum n (mMin n) - 1 + +/-- +Let $n\geq 1$ and let $m$ be minimal such that $\sum_{n\leq k\leq m}\frac{1}{k}\geq 1$. We define +\[\epsilon(n) = \sum_{n\leq k\leq m}\frac{1}{k}-1.\] +How small can $\epsilon(n)$ be? Is it true that +\[\liminf n^2\epsilon(n)=0?\] + +This is true, and shown by Lim and Steinerberger [LiSt24], who further proved that, for any +$\delta>0$, there exist infinitely many $n$ and $m$ such that +\[n^2\left\lvert \sum_{n\leq k\leq m}\frac{1}{k}-1\right\rvert\ll \frac{1}{(\log n)^{5/4-\delta}}.\] +Erdős and Graham (and also Lim and Steinerberger) believe that the exponent of $2$ is best +possible here, in that $\liminf \epsilon(n) n^{2+\delta}=\infty$ for all $\delta>0$. +-/ +@[category research solved, AMS 11 40, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos314.lean"] +theorem erdos_314 : answer(True) ↔ + atTop.liminf (fun n : ℕ => (n : ℝ) ^ 2 * epsilon n) = 0 := by + sorry + +end Erdos314 diff --git a/FormalConjectures/ErdosProblems/315.lean b/FormalConjectures/ErdosProblems/315.lean new file mode 100644 index 0000000000..89c7b16524 --- /dev/null +++ b/FormalConjectures/ErdosProblems/315.lean @@ -0,0 +1,73 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 315 + +*References:* +- [erdosproblems.com/315](https://www.erdosproblems.com/315) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [Ka25] Y. Kamio, *Asymptotic analysis of infinite decompositions of a unit fraction into unit + fractions*. arXiv:2503.02317 (2025). +- [LiTa25] Z. Li and Q. Tang, *On a conjecture of Erdős and Graham about the Sylvester's + sequence*. arXiv:2503.12277 (2025). +-/ + +open Filter + +namespace Erdos315 + +/-- The sequence $u_1=1$, $u_{n+1}=u_n(u_n+1)$, indexed here so that `u i` is $u_{i+1}$: +`u 0 = 1`, `u 1 = 2`, `u 2 = 6`, `u 3 = 42`, … (so `u i + 1` is Sylvester's sequence +$2, 3, 7, 43, \ldots$). -/ +def u : ℕ → ℕ + | 0 => 1 + | n + 1 => u n * (u n + 1) + +/-- The Vardi constant $c_0=\lim u_n^{1/2^n}=1.264085\cdots$. With the `0`-indexing of `u`, the +$n$-th term $u_n^{1/2^n}$ of the defining sequence is `(u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))` at +`i = n - 1`. -/ +noncomputable def c₀ : ℝ := limUnder atTop fun i => (u i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1)) + +/-- +Let $u_1=1$ and $u_{n+1}=u_n(u_n+1)$, so that $\sum_{k\geq 1}\frac{1}{u_k+1}$ and +$u_k=\lfloor c_0^{2^k}+1\rfloor$ for $k\geq 1$, where +\[c_0=\lim u_n^{1/2^n}=1.264085\cdots.\] +Let $a_1 (a i : ℝ) ^ ((1 / 2 : ℝ) ^ (i + 1))) < c₀ := by + sorry + +end Erdos315 diff --git a/FormalConjectures/ErdosProblems/333.lean b/FormalConjectures/ErdosProblems/333.lean new file mode 100644 index 0000000000..f909154d75 --- /dev/null +++ b/FormalConjectures/ErdosProblems/333.lean @@ -0,0 +1,57 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 333 + +*References:* +- [erdosproblems.com/333](https://www.erdosproblems.com/333) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [ErNe77] Erdős, P. and Newman, D. J., *Bases for sets of integers*. J. Number Theory (1977), + 420-425. +-/ + +open Classical Filter Asymptotics + +open scoped Pointwise + +namespace Erdos333 + +/-- +Let $A\subseteq \mathbb{N}$ be a set of density zero. Does there exist a $B$ such that +$A\subseteq B+B$ and +\[\lvert B\cap \{1,\ldots,N\}\rvert =o(N^{1/2})\] +for all large $N$? + +The answer is no. Erdős and Newman [ErNe77] have proved this is true when $A$ is the set of +squares. In fact, Theorem 2 of [ErNe77] already implies a negative answer to this problem, but +this seems to have been overlooked by Erdős and Graham. + +See also [806]. +-/ +@[category research solved, AMS 11, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos333.lean"] +theorem erdos_333 : answer(False) ↔ + ∀ A : Set ℕ, A.HasDensity 0 → + ∃ B : Set ℕ, A ⊆ B + B ∧ + (fun N => (((Finset.Icc 1 N).filter (· ∈ B)).card : ℝ)) =o[atTop] + fun N => Real.sqrt N := by + sorry + +end Erdos333 diff --git a/FormalConjectures/ErdosProblems/369.lean b/FormalConjectures/ErdosProblems/369.lean new file mode 100644 index 0000000000..fd7411ef1e --- /dev/null +++ b/FormalConjectures/ErdosProblems/369.lean @@ -0,0 +1,62 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 369 + +*References:* +- [erdosproblems.com/369](https://www.erdosproblems.com/369) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [EgSe76] Eggleton, R. B. and Selfridge, J. L., *Consecutive integers with no large prime factors*. + J. Austral. Math. Soc. Ser. A (1976), 1--11. +- [BFMW20] Bober, J. W. and Fretwell, D. and Martin, G. and Wooley, T. D., *Smooth values of + polynomials*. J. Aust. Math. Soc. (2020), 245--261. +- [BaWo98] Balog, Antal and Wooley, Trevor D., *On strings of consecutive integers with no large + prime factors*. J. Austral. Math. Soc. Ser. A (1998), 266-276. +-/ + +open Filter + +namespace Erdos369 + +/-- +Let $\epsilon>0$ and $k\geq 2$. Is it true that, for all sufficiently large $n$, there is a +sequence of $k$ consecutive integers in $\{1,\ldots,n\}$ all of which are $n^\epsilon$-smooth? + +The problem is trivially true as written (simply taking $\{1,\ldots,k\}$ and $n>k^{1/\epsilon}$). +There are (at least) two possible variants which are non-trivial, and it is not clear which +Erdős and Graham meant. We formalize the second: each $m\in P$ (where $P$ is the sequence of $k$ +consecutive integers sought for) must be in $[n/2,n]$. In this case a positive answer also +follows directly from the result of Balog and Wooley [BaWo98] for infinitely many $n$. Proving +this is true for all large $n$ does not follow immediately from [BaWo98], but can be deduced +using a similar construction, as shown by SkyYang. + +The statement below takes the $k$ consecutive integers as $a+1,\ldots,a+k$ with +$\lfloor n/2\rfloor\leq a+1$ and $a+k\leq n$, and renders "$n^\epsilon$-smooth" as: every prime +factor is at most $n^\epsilon$. +-/ +@[category research solved, AMS 11, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos369.lean"] +theorem erdos_369 : answer(True) ↔ + ∀ (ε : ℝ) (hε : 0 < ε) (k : ℕ) (hk : 2 ≤ k), + ∀ᶠ (n : ℕ) in atTop, ∃ a : ℕ, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ + ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, (p : ℝ) ≤ (n : ℝ) ^ ε := by + sorry + +end Erdos369 diff --git a/FormalConjectures/ErdosProblems/401.lean b/FormalConjectures/ErdosProblems/401.lean new file mode 100644 index 0000000000..15cf3a0d3f --- /dev/null +++ b/FormalConjectures/ErdosProblems/401.lean @@ -0,0 +1,60 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 401 + +*References:* +- [erdosproblems.com/401](https://www.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). +-/ + +open Filter + +namespace Erdos401 + +/-- +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]). + +The statement below writes $p_i$ for the $i$-th prime, so that +$2^n3^n\cdots p_r^n=(p_1p_2\cdots p_r)^n$, and takes $a_1,a_2$ to be positive integers. +-/ +@[category research solved, AMS 11, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos401.lean"] +theorem erdos_401 : answer(True) ↔ + ∃ 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 := by + sorry + +end Erdos401 diff --git a/FormalConjectures/ErdosProblems/429.lean b/FormalConjectures/ErdosProblems/429.lean new file mode 100644 index 0000000000..08e954e694 --- /dev/null +++ b/FormalConjectures/ErdosProblems/429.lean @@ -0,0 +1,59 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 429 + +*References:* +- [erdosproblems.com/429](https://www.erdosproblems.com/429) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [Er80] Erdős, Paul, *A survey of problems in combinatorial number theory*. + Ann. Discrete Math. (1980), 89-115. +- [We24] D. Weisenberg, *Sparse Admissible Sets and a Problem of Erdős and Graham*. + Integers (2024). +-/ + +open Filter + +namespace Erdos429 + +/-- +Is it true that, if $A\subseteq \mathbb{N}$ is sparse enough and does not cover all residue +classes modulo $p$ for any prime $p$, then there exists some $n$ such that $n+a$ is prime for +all $a\in A$? + +Weisenberg [We24] has shown the answer is no: $A$ can be arbitrarily sparse and missing at +least one residue class modulo every prime $p$, and yet $A+n$ is not contained in the primes +for any $n\in \mathbb{Z}$. (Weisenberg gives several constructions of such an $A$.) + +The statement below formalizes "sparse enough" via a threshold: is there some +$f:\mathbb{N}\to\mathbb{N}$ with $f(N)\to\infty$ such that every infinite $A$ with +$\lvert A\cap[1,N]\rvert\leq f(N)$ for all $N$, missing a residue class modulo every prime, +admits such an $n$? Weisenberg's constructions refute this for every choice of $f$. +-/ +@[category research solved, AMS 11, + formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos429.lean"] +theorem erdos_429 : answer(False) ↔ + ∃ f : ℕ → ℕ, Tendsto f atTop atTop ∧ + ∀ A : Set ℕ, A.Infinite → (∀ N, (A ∩ Set.Icc 1 N).ncard ≤ f N) → + (∀ p : ℕ, p.Prime → ∃ b : ZMod p, ∀ a ∈ A, (a : ZMod p) ≠ b) → + ∃ n : ℕ, ∀ a ∈ A, (n + a).Prime := by + sorry + +end Erdos429 diff --git a/FormalConjectures/ErdosProblems/435.lean b/FormalConjectures/ErdosProblems/435.lean new file mode 100644 index 0000000000..f58cae9bab --- /dev/null +++ b/FormalConjectures/ErdosProblems/435.lean @@ -0,0 +1,57 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 435 + +*References:* +- [erdosproblems.com/435](https://www.erdosproblems.com/435) +- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number + theory*. Monographies de L'Enseignement Mathematique (1980). +- [HwSo24] W. Hwang and K. Song, *The Frobenius problem for Numerical Semigroups generated by + binomial coefficients*. arXiv:2412.17882 (2024). +-/ + +namespace Erdos435 + +/-- +Let $n\in\mathbb{N}$ with $n\neq p^k$ for any prime $p$ and $k\geq 0$. What is the largest +integer not of the form +\[\sum_{1\leq i