Skip to content

Commit 9d7ebd6

Browse files
ryantuckryantuck
authored
Merge branch 'main' into erdos-13
2 parents 7ed8a46 + aecad71 commit 9d7ebd6

File tree

13 files changed

+666
-0
lines changed

13 files changed

+666
-0
lines changed

‎FormalConjectures/ErdosProblems/197.lean‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 197
21+
22+
*Reference:* [erdosproblems.com/197](https://www.erdosproblems.com/197)
23+
-/
24+
25+
open Set
26+
27+
namespace Erdos197
28+
29+
/--
30+
Can $\mathbb{N}$ be partitioned into two sets, each of which can be permuted to avoid monotone
31+
3-term arithmetic progressions?
32+
-/
33+
@[category research open, AMS 5]
34+
theorem erdos_197 :
35+
answer(sorry) ↔ ∃ A B : Set ℕ, IsCompl A B ∧
36+
(∃ f : ℕ ≃ A, ¬ HasMonotoneAP f 3) ∧
37+
(∃ g : ℕ ≃ B, ¬ HasMonotoneAP g 3) := by
38+
sorry
39+
40+
end Erdos197

‎FormalConjectures/ErdosProblems/277.lean‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 277
21+
22+
*References:*
23+
- [erdosproblems.com/277](https://www.erdosproblems.com/277)
24+
- [Ha79] Haight, J. A., Covering systems of congruences, a negative result. Mathematika (1979),
25+
53--61.
26+
-/
27+
28+
open ArithmeticFunction
29+
30+
namespace Erdos277
31+
32+
/--
33+
Is it true that, for every $c$, there exists an $n$ such that $\sigma(n)>cn$ but there is no
34+
covering system whose moduli all divide $n$?
35+
36+
This was answered affirmatively by Haight [Ha79].
37+
-/
38+
@[category research solved, AMS 11]
39+
theorem erdos_277 :
40+
answer(True) ↔ ∀ c : ℝ, ∃ n : ℕ, (sigma 1 n : ℝ) > c * n ∧
41+
¬ ∃ (S : Finset (ℤ × ℕ)),
42+
(∀ z : ℤ, ∃ s ∈ S, z ≡ s.1 [ZMOD s.2]) ∧
43+
(∀ s ∈ S, s.2 ∣ n ∧ 1 < s.2) := by
44+
sorry
45+
46+
end Erdos277

‎FormalConjectures/ErdosProblems/331.lean‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 331
21+
22+
*Reference:* [erdosproblems.com/331](https://www.erdosproblems.com/331)
23+
-/
24+
25+
open Nat Filter
26+
open scoped Asymptotics Classical
27+
28+
namespace Erdos331
29+
30+
/--
31+
Let $A,B\subseteq \mathbb{N}$ such that for all large $N$\[\lvert A\cap \{1,\ldots,N\}\rvert \gg
32+
N^{1/2}\]and\[\lvert B\cap \{1,\ldots,N\}\rvert \gg N^{1/2}.\]
33+
Is it true that there are infinitely many solutions to $a_1-a_2=b_1-b_2\neq 0$ with $a_1,a_2\in A$
34+
and $b_1,b_2\in B$?
35+
36+
Ruzsa has observed that there is a simple counterexample: take $A$ to be the set of numbers whose
37+
binary representation has only non-zero digits in even places, and $B$ similarly but with non-zero
38+
digits only in odd places. It is easy to see $A$ and $B$ both grow like $\gg N^{1/2}$ and yet for
39+
any $n\geq 1$ there is exactly one solution to $n=a+b$ with $a\in A$ and $b\in B$.
40+
-/
41+
@[category research solved, AMS 11]
42+
theorem erdos_331 :
43+
answer(False) ↔
44+
∀ A B : Set ℕ,
45+
(fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count A n : ℝ)) ∧
46+
(fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count B n : ℝ)) ∧
47+
{ s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
48+
a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧
49+
a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁ }.Infinite := by
50+
sorry
51+
52+
/--
53+
Ruzsa suggests that a non-trivial variant of this problem arises if one imposes the stronger
54+
condition that $|A \cap \{1,\dots,N\}| \sim c_A N^{1/2}$ for some constant $c_A>0$, and similarly
55+
for $B$.
56+
-/
57+
@[category research open, AMS 11]
58+
theorem erdos_331.variant.ruzsa :
59+
answer(sorry) ↔
60+
∀ A B : Set ℕ,
61+
(∃ c_A > 0, (fun (n : ℕ) ↦ (count A n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_A * (n : ℝ) ^ (1 / 2 : ℝ))) →
62+
(∃ c_B > 0, (fun (n : ℕ) ↦ (count B n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_B * (n : ℝ) ^ (1 / 2 : ℝ))) →
63+
{ s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
64+
a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧
65+
a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁ }.Infinite := by
66+
sorry
67+
end Erdos331

‎FormalConjectures/ErdosProblems/770.lean‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 770
21+
22+
*References:*
23+
- [erdosproblems.com/770](https://www.erdosproblems.com/770)
24+
- [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical
25+
Society 67.1 (1949): 51-56.
26+
- [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal,
27+
Second Series 18.3 (1966): 259-269.
28+
-/
29+
30+
open Set ENat Filter
31+
32+
namespace Erdos770
33+
34+
/-- Let `h n` be the minimal number such that `2 ^ n - 1, ..., (h n) ^ n - 1` are mutually
35+
coprime. -/
36+
noncomputable def h (n : ℕ) : ℕ∞ := sInf {m | 2 < m ∧
37+
(Set.Icc 2 m).Pairwise fun i j => (i.toNat ^ n - 1).Coprime (j.toNat ^ n - 1)}
38+
39+
/-- `n + 1` is prime iff `h n = n + 1`. #TODO: prove this theorem. -/
40+
@[category test, AMS 11]
41+
theorem Nat.Prime.h_eq_add_one {n : ℕ} : h n = n + 1 ↔ (n + 1).Prime := by sorry
42+
43+
/-- If `n` is odd, then `h n = ∞`. #TODO: prove this theorem. -/
44+
@[category test, AMS 11]
45+
theorem Odd.h_unbounded {n : ℕ} (pn : Odd n) : h n = ⊤ := by sorry
46+
47+
/-- For every prime `p`, does the density of integers with `h n = p` exist? -/
48+
@[category research open, AMS 11]
49+
theorem erdos_770.density : answer(sorry) ↔ ∀ p : ℕ, p.Prime → ∃ a, HasDensity {n | h n = p} a := by
50+
sorry
51+
52+
/-- Does `liminf h n = ∞`? -/
53+
@[category research open, AMS 11]
54+
theorem erdos_770.liminf : answer(sorry) ↔ liminf h atTop = ⊤ := by
55+
sorry
56+
57+
/-- Is it true that if `p` is the greatest prime such that `p - 1 ∣ n` and `p > n ^ ε`, then
58+
`h n = p`? -/
59+
@[category research open, AMS 11]
60+
theorem erdos_770.prime : answer(sorry) ↔ ∀ ε > 0, ∀ᶠ n in atTop,
61+
let p := sSup {m : ℕ | m.Prime ∧ m - 1 ∣ n}
62+
p > (n : ℝ) ^ (ε : ℝ) → h n = p := by
63+
sorry
64+
65+
/-- It is probably true that `h n = 3` for infinitely many `n`. -/
66+
@[category research open, AMS 11]
67+
theorem erdos_770.three : {n | h n = 3}.Infinite := by
68+
sorry
69+
70+
end Erdos770

‎FormalConjectures/ErdosProblems/978.lean‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Erdős Problem 978
21+
22+
*Reference:*
23+
- [erdosproblems.com/978](https://www.erdosproblems.com/978)
24+
- [Ho67] Hooley, C., On the power free values of polynomials. Mathematika (1967), 21--26.
25+
- [Br11] Browning, T. D., Power-free values of polynomials. Arch. Math. (Basel) (2011), 139--150.
26+
- [Er53] Erdős, P., Arithmetical properties of polynomials. J. London Math. Soc. (1953), 416--425.
27+
-/
28+
29+
open Polynomial Set
30+
31+
namespace Erdos978
32+
33+
/-- Let `f ∈ ℤ[X]` be an irreducible polynomial. Suppose that the degree `k` of `f` is larger than
34+
`2` and is not equal to a power of `2`. Then the set of `n` such that `f n` is `(k - 1)`-th power
35+
free is infinite, and this is proved in [Er53]. -/
36+
@[category research solved, AMS 11]
37+
theorem erdos_978.sub_one {f : ℤ[X]} (hi : Irreducible f) (hd : f.natDegree > 2)
38+
(hp : ¬ ∃ l : ℕ, f.natDegree = 2 ^ l) :
39+
{n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))}.Infinite := by
40+
sorry
41+
42+
/-- Let `f ∈ ℤ[X]` be an irreducible polynomial. Suppose that the degree `k` of `f` is larger than
43+
`2`, and `f n` have no fixed `(k - 1)`-th power divisors other than `1`. Then the set of `n` such
44+
that `f n` is `(k - 1)`-th power free has positive density, and this is proved in [Ho67]. -/
45+
@[category research solved, AMS 11]
46+
theorem erdos_978.sub_one_density {f : ℤ[X]} (hi : Irreducible f) (hd : f.natDegree > 2)
47+
(hp : ¬ ∃ p : ℕ, p.Prime ∧ ∀ n : ℕ, (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) :
48+
HasPosDensity {n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))} := by
49+
sorry
50+
51+
/-- If the degree `k` of `f` is larger than or equal to `9`, then the set of `n` such that `f n` is
52+
`(k - 2)`-th power free has infinitely many elements. This result is proved in [Br11]. -/
53+
@[category research solved, AMS 11]
54+
theorem erdos_978.sub_two {f : ℤ[X]} (hi : Irreducible f) (hd : f.natDegree ≥ 9)
55+
(hp : ¬ ∃ p : ℕ, p.Prime ∧ ∀ n : ℕ, (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) :
56+
{n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite := by
57+
sorry
58+
59+
/-- Is it true that the set of `n` such that `f n` is `(k - 2)`-th power free has infinitely many
60+
elements? -/
61+
@[category research open, AMS 11]
62+
theorem erdos_978.sub_two' : answer(sorry) ↔ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 2 →
63+
(¬ ∃ p : ℕ, p.Prime ∧ ∀ n : ℕ, (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) →
64+
{n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite := by
65+
sorry
66+
67+
/-- Does `n ^ 4 + 2` represent infinitely many squarefree numbers? -/
68+
@[category research open, AMS 11]
69+
theorem erdos_978.squarefree : answer(sorry) ↔ {n : ℕ | Squarefree (n ^ 4 + 2)}.Infinite := by
70+
sorry
71+
72+
end Erdos978

‎FormalConjectures/GreensOpenProblems/37.lean‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
17+
import FormalConjectures.Util.ProblemImports
18+
19+
/-!
20+
# Ben Green's Open Problem 37
21+
22+
What is the smallest subset of `ℕ` containing, for each `d = 1, …, N`,
23+
an arithmetic progression of length `k` with common difference `d`?
24+
25+
*References:*
26+
- [Ben Green's Open Problem 37](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.37)
27+
- [Green & Tao, *The primes contain arbitrarily long arithmetic progressions* (arXiv:math/0404188)](https://arxiv.org/abs/math/0404188)
28+
-/
29+
30+
namespace Green37
31+
32+
open Set Filter
33+
open scoped Asymptotics
34+
35+
/-- `A` contains an arithmetic progression of length `k` and common difference `d` for every `d ∈ {1, …, N}`. -/
36+
def IsAPCover (A : Set ℕ) (N k : ℕ) : Prop := ∀ d, 1 ≤ d ∧ d ≤ N → Set.ContainsAP A k d
37+
38+
/-- The minimum size of a subset of `ℕ` that contains, for each `d = 1, …, N`,
39+
an arithmetic progression of length `k` with common difference `d`. -/
40+
noncomputable def m (N k : ℕ) : ℕ :=
41+
sInf { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k }
42+
43+
/--
44+
Given a natural number `N`, what is the smallest size of a subset of `ℕ` that contains, for each `d = 1, …, N`,
45+
an arithmetic progression of length `k` with common difference `d`.
46+
-/
47+
@[category research open, AMS 05 11]
48+
theorem green_37 (N k : ℕ) :
49+
IsLeast { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k } (answer(sorry)) := by
50+
sorry
51+
52+
/--
53+
Asymptotic version: determine the asymptotic behavior of `m(N, k)` as `N` grows.
54+
The solver should determine what function `f : ℕ → ℝ` eventually equals `(fun N ↦ (m N k : ℝ))`.
55+
-/
56+
@[category research open, AMS 05 11]
57+
theorem green_37_asymptotic (k : ℕ) :
58+
∀ᶠ N in atTop, (m N k : ℝ) = (answer(sorry) : ℕ → ℝ) N := by
59+
sorry
60+
61+
/-- Determine the asymptotic equivalence class (theta) of `m(N, k)`. -/
62+
@[category research open, AMS 05 11]
63+
theorem green_37_theta (k : ℕ) :
64+
(fun N ↦ (m N k : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := by
65+
sorry
66+
67+
/-- Determine an upper bound (big O) for `m(N, k)`. -/
68+
@[category research open, AMS 05 11]
69+
theorem green_37_bigO (k : ℕ) :
70+
(fun N ↦ (m N k : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := by
71+
sorry
72+
73+
/-- Determine a strict upper bound (little o) for `m(N, k)`. -/
74+
@[category research open, AMS 05 11]
75+
theorem green_37_littleO (k : ℕ) :
76+
(fun N ↦ (m N k : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := by
77+
sorry
78+
79+
end Green37

0 commit comments

Comments
 (0)