From 93c4cf2ab1e0d88a0466073321f9c1d493e47457 Mon Sep 17 00:00:00 2001 From: smmercuri Date: Wed, 15 Oct 2025 16:52:27 +0000 Subject: [PATCH 1/3] Add erdos 1074 --- FormalConjectures/ErdosProblems/1074.lean | 94 +++++++++++++++++++++++ 1 file changed, 94 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/1074.lean diff --git a/FormalConjectures/ErdosProblems/1074.lean b/FormalConjectures/ErdosProblems/1074.lean new file mode 100644 index 000000000..fa0f07f9a --- /dev/null +++ b/FormalConjectures/ErdosProblems/1074.lean @@ -0,0 +1,94 @@ +/- +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 1074 + +*Reference:* [erdosproblems.com/1074](https://www.erdosproblems.com/1074) +-/ + +open scoped Nat + +/-- The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there +exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$.-/ +abbrev Nat.EHSNumbers : Set ℕ := { m | 1 ≤ m ∧ ∃ p, ¬ p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} + +/-- The Pillai primes are those primes $p$ such that there exists an $m$ with +$p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$-/ +abbrev Nat.PillaiPrimes : Set ℕ := {p | p.Prime ∧ ∃ m, ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} + +namespace Erdos1074 + +open Nat + +/-- Let $S$ be the set of all $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such +that $m! + 1 \equiv 0\pmod{p}$. Does +$$ + \lim\frac{|S\cap[1, x]|}{x} +$$ +exist? What is it? -/ +@[category research open, AMS 11] +theorem erdos_1074.parts.i : (∃ c, EHSNumbers.HasDensity c) ↔ answer(sorry) := by + sorry + +/-- Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with +$p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then does +$$ + \lim\frac{|P\cap[1, x]|}{\pi(x)} +$$ +exist? What is it?-/ +@[category research open, AMS 11] +theorem erdos_1074.parts.ii : (∃ c, PillaiPrimes.HasDensity c {p | p.Prime}) ↔ answer(sorry) := by + sorry + +/-- Pillai [Pi30] raised the question of whether there exist any primes in $P$. This was answered +by Chowla, who noted that, for example, $14! + 1 \equiv 18! + 1 \equiv 0 \pmod{23}$.-/ +@[category test, AMS 11] +theorem erdos_1074.variants.mem_pillaiPrimes : 23 ∈ PillaiPrimes := by + norm_num + exact ⟨14, by decide⟩ + +/-- Erdős, Hardy, and Subbarao proved that $S$ is infinite. -/ +@[category research solved, AMS 11] +theorem erdos_1074.variants.EHSNumbers_infinite : EHSNumbers.Infinite := by + sorry + +/-- Erdős, Hardy, and Subbarao proved that $P$ is infinite. -/ +@[category research solved, AMS 11] +theorem erdos_1074.variants.PillaiPrimes_infinite : PillaiPrimes.Infinite := by + sorry + +/-- The sequence $S$ begins $8, 9, 13, 14, 15, 16, 17, ...$ -/ +@[category test, AMS 11] +theorem erdos_1074.variants.EHSNumbers_init : + nth EHSNumbers '' (Set.Icc 0 6) = {8, 9, 13, 14, 15, 16, 17} := by + sorry + +/-- The sequence $P$ begins $23, 29, 59, 61, 67, 71, ...$ -/ +@[category test, AMS 11] +theorem erdos_1074.variants.PillaiPrimes_init : + nth PillaiPrimes '' (Set.Icc 0 5) = {23, 29, 59, 61, 67, 71} := by + sorry + +/-- Regarding the first question, Hardy and Subbarao computed all EHS numbers up to $2^{10}$, and +write '...if this trend conditions we expect [the limit] to be around 0.5, if it exists.` -/ +@[category research open, AMS 11] +theorem erdos_1074.variants.EHSNumbers_one_half : EHSNumbers.HasDensity (1 / 2) := by + sorry + +end Erdos1074 From 73c29a379d3ede002900348b30c4adbe42e31e12 Mon Sep 17 00:00:00 2001 From: smmercuri Date: Thu, 16 Oct 2025 17:17:07 +0000 Subject: [PATCH 2/3] Suggestions --- FormalConjectures/ErdosProblems/1074.lean | 27 +++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/FormalConjectures/ErdosProblems/1074.lean b/FormalConjectures/ErdosProblems/1074.lean index fa0f07f9a..175640b87 100644 --- a/FormalConjectures/ErdosProblems/1074.lean +++ b/FormalConjectures/ErdosProblems/1074.lean @@ -26,7 +26,7 @@ open scoped Nat /-- The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$.-/ -abbrev Nat.EHSNumbers : Set ℕ := { m | 1 ≤ m ∧ ∃ p, ¬ p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} +abbrev Nat.EHSNumbers : Set ℕ := {m | 1 ≤ m ∧ ∃ p, ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} /-- The Pillai primes are those primes $p$ such that there exists an $m$ with $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$-/ @@ -43,7 +43,16 @@ $$ $$ exist? What is it? -/ @[category research open, AMS 11] -theorem erdos_1074.parts.i : (∃ c, EHSNumbers.HasDensity c) ↔ answer(sorry) := by +theorem erdos_1074.parts.i.i : (∃ c, EHSNumbers.HasDensity c) ↔ answer(sorry) := by + sorry + +/-- Let $S$ be the set of all $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such +that $m! + 1 \equiv 0\pmod{p}$. What is +$$ + \lim\frac{|S\cap[1, x]|}{x}? +$$ -/ +@[category research open, AMS 11] +theorem erdos_1074.parts.i.ii : ∃ c, c = answer(sorry) ∧ EHSNumbers.HasDensity c := by sorry /-- Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with @@ -51,9 +60,19 @@ $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then does $$ \lim\frac{|P\cap[1, x]|}{\pi(x)} $$ -exist? What is it?-/ +exist? What is it? -/ +@[category research open, AMS 11] +theorem erdos_1074.parts.ii.i : (∃ c, PillaiPrimes.HasDensity c {p | p.Prime}) ↔ answer(sorry) := by + sorry + +/-- Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with +$p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then what is +$$ + \lim\frac{|P\cap[1, x]|}{\pi(x)}? +$$ -/ @[category research open, AMS 11] -theorem erdos_1074.parts.ii : (∃ c, PillaiPrimes.HasDensity c {p | p.Prime}) ↔ answer(sorry) := by +theorem erdos_1074.parts.ii.ii : + ∃ c, c = answer(sorry) ∧ PillaiPrimes.HasDensity c {p | p.Prime} := by sorry /-- Pillai [Pi30] raised the question of whether there exist any primes in $P$. This was answered From c0506a3efef3a67f28996f647a9764ed6f676651 Mon Sep 17 00:00:00 2001 From: smmercuri Date: Tue, 28 Oct 2025 06:46:13 +0000 Subject: [PATCH 3/3] Suggestions --- FormalConjectures/ErdosProblems/1074.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/FormalConjectures/ErdosProblems/1074.lean b/FormalConjectures/ErdosProblems/1074.lean index 175640b87..faf17658f 100644 --- a/FormalConjectures/ErdosProblems/1074.lean +++ b/FormalConjectures/ErdosProblems/1074.lean @@ -26,7 +26,7 @@ open scoped Nat /-- The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$.-/ -abbrev Nat.EHSNumbers : Set ℕ := {m | 1 ≤ m ∧ ∃ p, ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} +abbrev Nat.EHSNumbers : Set ℕ := {m | 1 ≤ m ∧ ∃ p, p.Prime ∧ ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1} /-- The Pillai primes are those primes $p$ such that there exists an $m$ with $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$-/ @@ -41,7 +41,7 @@ that $m! + 1 \equiv 0\pmod{p}$. Does $$ \lim\frac{|S\cap[1, x]|}{x} $$ -exist? What is it? -/ +exist? -/ @[category research open, AMS 11] theorem erdos_1074.parts.i.i : (∃ c, EHSNumbers.HasDensity c) ↔ answer(sorry) := by sorry @@ -52,7 +52,7 @@ $$ \lim\frac{|S\cap[1, x]|}{x}? $$ -/ @[category research open, AMS 11] -theorem erdos_1074.parts.i.ii : ∃ c, c = answer(sorry) ∧ EHSNumbers.HasDensity c := by +theorem erdos_1074.parts.i.ii : EHSNumbers.HasDensity answer(sorry) := by sorry /-- Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with @@ -60,7 +60,7 @@ $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then does $$ \lim\frac{|P\cap[1, x]|}{\pi(x)} $$ -exist? What is it? -/ +exist? -/ @[category research open, AMS 11] theorem erdos_1074.parts.ii.i : (∃ c, PillaiPrimes.HasDensity c {p | p.Prime}) ↔ answer(sorry) := by sorry @@ -72,7 +72,7 @@ $$ $$ -/ @[category research open, AMS 11] theorem erdos_1074.parts.ii.ii : - ∃ c, c = answer(sorry) ∧ PillaiPrimes.HasDensity c {p | p.Prime} := by + PillaiPrimes.HasDensity answer(sorry) {p | p.Prime} := by sorry /-- Pillai [Pi30] raised the question of whether there exist any primes in $P$. This was answered