Merge branch 'main' into erdos-graffiti-conjecture

Author: henrykmichalewski

FormalConjectures/Arxiv/1506.05785/MaximumAngle.lean

@@ -0,0 +1,44 @@
+/-
+Copyright 2025 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
+
+/-!
+# Approximation of Quantum Gates using Lattices
+
+*Reference:* [arxiv/1506.05785](https://arxiv.org/pdf/1506.05785)
+_On the Approximation of Quantum Gates using Lattices_
+by *Alec Greene and Steven Damelin*
+-/
+
+open scoped EuclideanSpace
+
+/-- The integer lattice ℤ⁴ as the ℤ-span of the standard basis in 4-dimensional Euclidean space. -/
+scoped[EuclideanSpace] notation "ℤ⁴" => Submodule.span ℤ (Set.range (PiLp.basisFun 2 ℝ (Fin 4)))
+
+instance : IsZLattice ℝ ℤ⁴ := ZSpan.isZLattice _
+
+/--
+*Conjecture 3.4*
+There exists $0 < \delta < 1$ such that for any $a \in \mathbb{S}^3$,
+there exists $b \in \mathbb{Z}^4$ and $k \in \mathbb{Z}$ such that $\|b\| = 5^k$ and
+$\langle a, \frac{b}{\|b\|} \rangle \geq 1 - 5^{-\frac{k}{2 - \delta}}.$
+-/
+@[category research open, AMS 81 11]
+theorem conjecture_3_4 : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧
+    ∀ (a : EuclideanSpace ℝ (Fin 4)) (ha : ‖a‖ = 1), ∃ (b : ℤ⁴) (k : ℤ), ‖b‖ = 5 ^ k ∧
+      inner a (‖b‖⁻¹ • b) ≥ 1 - (5 : ℝ) ^ (-k / (2 - δ)) := by
+  sorry

FormalConjectures/ErdosProblems/128.lean

@@ -0,0 +1,38 @@
+/-
+Copyright 2025 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 128
+
+*Reference:* [erdosproblems.com/128](https://www.erdosproblems.com/128)
+-/
+
+variable {V : Type*} {G : SimpleGraph V} [Fintype V]
+
+/--
+Let G be a graph with n vertices such that every subgraph on ≥ $n/2$
+vertices has more than $n^2/50$ edges. Must G contain a triangle?
+-/
+@[category research open, AMS 5]
+theorem erdos_128 :
+    ((∀ (G' : G.Subgraph) [Fintype G'.verts] [Fintype G'.edgeSet],
+        letI n := Fintype.card V;
+        2 * G'.verts.toFinset.card ≥ n →
+        50 * G'.edgeSet.toFinset.card > n^2) → ¬ (G.CliqueFree 3))
+    ↔ answer(sorry) := by
+  sorry

FormalConjectures/ErdosProblems/141.lean

@@ -0,0 +1,114 @@
+/-
+Copyright 2025 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 141
+
+*References:*
+- [erdosproblems.com/141](https://www.erdosproblems.com/141)
+- [Wikipedia](https://en.wikipedia.org/wiki/Primes_in_arithmetic_progression#Consecutive_primes_in_arithmetic_progression)
+-/
+
+/--
+The predicate that a set `s` consists of `l` consecutive primes (possibly infinite).
+This predicate does not assert a specific value for the first term.
+-/
+def Set.IsPrimeProgressionOfLength (s : Set ℕ) (l : ℕ∞) : Prop :=
+    ∃ a, ENat.card s = l ∧ s = {(a + n).nth Nat.Prime | (n : ℕ) (_ : n < l)}
+
+open Nat
+
+/--
+The first three odd primes are an example of three consecutive primes.
+-/
+@[category test, AMS 5 11]
+theorem first_three_odd_primes : ({3, 5, 7} : Set ℕ).IsPrimeProgressionOfLength 3 := by
+  use 1
+  constructor
+  · aesop
+  · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def,
+    show (2).nth Nat.Prime = 5 from nth_count prime_five,
+    show (3).nth Nat.Prime = 7 from Nat.nth_count (by decide : (7).Prime)]
+
+/--
+The predicate that a set `s` is both an arithmetic progression of length `l` and a progression
+of `l` consecutive primes.
+-/
+def Set.IsAPAndPrimeProgressionOfLength (s : Set ℕ) (l : ℕ) :=
+   s.IsAPOfLength l ∧ s.IsPrimeProgressionOfLength l
+
+/--
+There are 3 consecutive primes in arithmetic progression.
+-/
+@[category test, AMS 5 11]
+example : ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength 3 := by
+  use {3, 5, 7}
+  constructor
+  · use 3, 2
+    unfold Set.IsAPOfLengthWith
+    constructor
+    · aesop
+    · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def]
+  · exact first_three_odd_primes
+
+/--
+Let $k≥3$. Are there $k$ consecutive primes in arithmetic progression?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_141 : (∀ k ≥ 3, ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength k)
+    ↔ answer(sorry) := by
+  sorry
+
+/--
+The existence of such progressions has been verified for $k≤10$.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_141.variant.first_cases :
+    (∀ k ≥ 3, k ≤ 10 → ∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength k) := by
+  sorry
+
+/--
+Are there $11$ consecutive primes in arithmetic progression?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_141.variant.eleven : (∃ (s : Set ℕ), s.IsAPAndPrimeProgressionOfLength 11)
+    ↔ answer(sorry) := by
+  sorry
+
+/--
+The set of arithmetic progressions of consecutive primes of length $k$.
+-/
+def consecutivePrimeArithmeticProgressions (k : ℕ) : Set (Set ℕ) :=
+  {s | s.IsAPAndPrimeProgressionOfLength k}
+
+/--
+It is open, even for $k=3$, whether there are infinitely many such progressions.
+-/
+@[category research open, AMS 5 11]
+theorem erdos_141.variant.infinite_three :
+    (consecutivePrimeArithmeticProgressions 3).Infinite ↔ answer(sorry) :=
+  sorry
+
+/--
+Fix a $k \geq 3$. Is it true that there are infinitely many arithmetic prime progressions of length $k$?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_141.variant.infinite_general_case  (k : ℕ) (hk : k ≥ 3) :
+    (consecutivePrimeArithmeticProgressions k).Infinite ↔ answer(sorry) :=
+  sorry
+  

FormalConjectures/ErdosProblems/168.lean

@@ -66,8 +66,8 @@ Sanity check: if `S` is a maximal non ternary subset of `{1,..., N}` then `F N`
 cardinality of `S`
 -/
 @[category API, AMS 5 11]
-lemma F_eq_card (N : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 N)
-    (hS' : NonTernary S) (hS'' : ∀ T, T ⊆ Finset.Icc 1 N → NonTernary T → S ⊆ T → T = S) :
+lemma F_eq_card (N : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 N) (hS' : NonTernary S)
+    (hS'' : ∀ T, T ⊆ Finset.Icc 1 N → NonTernary T → S.card ≤ T.card → T.card = S.card) :
     F N = S.card := by
   sorry
 

FormalConjectures/ErdosProblems/200.lean

@@ -0,0 +1,47 @@
+/-
+Copyright 2025 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 200
+
+*Reference:* [erdosproblems.com/200](https://www.erdosproblems.com/200)
+-/
+
+open Filter Real
+
+/--
+The length of the longest arithmetic progression of primes in $\{1,\ldots,n\}$.
+-/
+noncomputable def longestPrimeArithmeticProgressions (n : ℕ) : ℕ :=
+  sSup {(k : ℕ) | ∃ s ⊆ Set.Icc 1 n, s.IsAPOfLength k ∧ ∀ m ∈ s, m.Prime}
+
+/--
+Does the longest arithmetic progression of primes in $\{1,\ldots,N\}$ have length $o(\log N)$?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_200 : (fun n => (longestPrimeArithmeticProgressions n : ℝ))
+    =o[atTop] (fun n => log n) ↔ answer(sorry) := by
+  sorry
+
+/--
+It follows from the prime number theorem that such a progression has length $\leq(1+o(1))\log N$.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_200.variants.upper : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
+    ∀ n, longestPrimeArithmeticProgressions n ≤ (1 + o n) * log n := by
+  sorry

FormalConjectures/ErdosProblems/208.lean

@@ -0,0 +1,57 @@
+/-
+Copyright 2025 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 208
+*Reference:* [erdosproblems.com/208](https://www.erdosproblems.com/208)
+-/
+
+open Filter Real
+
+/-- The sequence of squarefree numbers, denoted by `s` as in Erdős problem 208. -/
+noncomputable def erdos208.s : ℕ → ℕ := Nat.nth Squarefree
+
+open erdos208
+
+/--
+Let $s_1 < s_2 < ⋯$ be the sequence of squarefree numbers. Is it true that
+for any $ϵ > 0$ and large $n$, $s_{n+1} − s_n ≪_ϵ s_n^ε$?
+-/
+@[category research open, AMS 11]
+theorem erdos_208.i :
+    (∀ ε > (0 : ℝ), (fun n => (s (n + 1) - s n : ℝ)) =O[atTop] (fun n => (s n : ℝ)^ε)) ↔
+    answer(sorry) := by sorry
+
+/--
+Let $s_1 < s_2 < ⋯$ be the sequence of squarefree numbers. Is it true that
+$s_{n + 1} - s_n ≤ (1 + o(1)) * (\pi^2 / 6) * log (s_n) / log (log (s_n))$?
+-/
+@[category research open, AMS 11]
+theorem erdos_208.ii :
+    (∃ (c : ℕ → ℝ), (c =o[atTop] (1 : ℕ → ℝ)) ∧ ∀ᶠ n in atTop,
+      s (n + 1) - s n ≤ (1 + (c n)) * (π^2 / 6) * log (s n) / log (log (s n))) ↔ answer(sorry) := by
+  sorry
+
+/--
+In [Er79] Erdős says perhaps $s_{n+1} − s_n ≪ log s_n$, but he is 'very doubtful'.
+
+[Er79] Erdős, Paul, __Some unconventional problems in number theory__. Math. Mag. (1979), 67-70.
+-/
+@[category research open, AMS 11]
+theorem erdos_208.variants.log_bound :
+    (fun n ↦ (s (n + 1) - s n : ℝ)) =O[atTop] fun n ↦ log (s n) := by sorry

FormalConjectures/ErdosProblems/245.lean

@@ -44,7 +44,7 @@ The answer is yes, proved by Freiman [Fr73].
 @[category research solved, AMS 5 11]
 theorem erdos_245 :
     (∀ (A : Set ℕ), A.Infinite → Tendsto (fun N => (A.bdd N |>.ncard : ℝ) / N) atTop (𝓝 0) →
-    3 ≤ limsup (fun N => ((A + A).bdd N |>.ncard : ℝ) / (A.bdd N).ncard) atTop) ↔ answer(True) := by
+    3 ≤ limsup (fun N => ((A + A).bdd N |>.ncard : EReal) / (A.bdd N).ncard) atTop) ↔ answer(True) := by
   sorry
 
 /--
@@ -73,5 +73,5 @@ $$
 @[category research solved, AMS 5 11]
 theorem erdos_245.variants.two (A : Set ℕ) (h_inf : A.Infinite)
     (hf : Tendsto (fun N => (A.bdd N |>.ncard : ℝ) / N) atTop (𝓝 0)) :
-    2 ≤ limsup (fun N => ((A + A).bdd N |>.ncard : ℝ) / (A.bdd N).ncard) atTop := by
+    2 ≤ limsup (fun N => ((A + A).bdd N |>.ncard : EReal) / (A.bdd N).ncard) atTop := by
   sorry

FormalConjectures/ErdosProblems/249.lean

@@ -0,0 +1,34 @@
+/-
+Copyright 2025 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 249
+
+*Reference:* [erdosproblems.com/249](https://www.erdosproblems.com/249)
+-/
+
+open scoped Nat
+
+/--
+Is
+$$\sum_{n} \frac{φ(n)}{2^n}$$
+irrational? Here $\phi$ is the Euler totient function.
+-/
+@[category research open, AMS 11]
+theorem erdos_249 : Irrational (∑' n : ℕ, (φ n) / (2 ^ n)) ↔ answer(sorry) := by
+  sorry