From dc36cf6009723e60f62ec5166944841dca869394 Mon Sep 17 00:00:00 2001
From: Aleksandr_NFA <sanexxx777@gmail.com>
Date: Wed, 1 Jul 2026 13:34:10 +1000
Subject: [PATCH] =?UTF-8?q?feat(GreensOpenProblems/64):=20formalize=20?=
 =?UTF-8?q?=CE=A9(p-2)=20odd=20infinitude=20question?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Green's open problem 64: do there exist infinitely many primes p for
which p - 2 has an odd number of prime factors (counted with
multiplicity)? Stated as `answer(sorry) ↔ {p | p.Prime ∧ Odd (Ω (p-2))}.Infinite`.

Adds three decidable `category test` witnesses: 5 and 7 satisfy the
condition (p-2 prime ⇒ Ω = 1 odd), while 11 does not (9 = 3^2, Ω = 2).
---
 FormalConjectures/GreensOpenProblems/64.lean | 68 ++++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 FormalConjectures/GreensOpenProblems/64.lean

diff --git a/FormalConjectures/GreensOpenProblems/64.lean b/FormalConjectures/GreensOpenProblems/64.lean
new file mode 100644
index 0000000000..05e6f840d9
--- /dev/null
+++ b/FormalConjectures/GreensOpenProblems/64.lean
@@ -0,0 +1,68 @@
+/-
+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
+
+/-!
+# Green's Open Problem 64
+
+*Reference:* [Ben Green's Open Problems](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.64)
+
+Do there exist infinitely many primes $p$ for which $p - 2$ has an odd number of prime factors,
+counted with multiplicity?
+
+Writing $\Omega(n)$ for the number of prime factors of $n$ counted with multiplicity, the question
+asks whether the set of primes $p$ with $\Omega(p - 2)$ odd is infinite.
+-/
+
+open ArithmeticFunction
+
+open scoped ArithmeticFunction.Omega
+
+namespace Green64
+
+/--
+Do there exist infinitely many primes $p$ for which $p - 2$ has an odd number of prime factors,
+counted with multiplicity (i.e. $\Omega(p - 2)$ is odd)?
+-/
+@[category research open, AMS 11]
+theorem green_64 :
+    answer(sorry) ↔ {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))}.Infinite := by
+  sorry
+
+/-- $5$ satisfies the condition: $5$ is prime and $5 - 2 = 3$ is prime, so $\Omega(3) = 1$ is odd. -/
+@[category test, AMS 11]
+theorem green_64_mem_five : 5 ∈ {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))} := by
+  refine ⟨by norm_num, ?_⟩
+  rw [show (5 : ℕ) - 2 = 3 by norm_num, cardFactors_apply_prime (by norm_num)]
+  exact odd_one
+
+/-- $7$ satisfies the condition: $7$ is prime and $7 - 2 = 5$ is prime, so $\Omega(5) = 1$ is odd. -/
+@[category test, AMS 11]
+theorem green_64_mem_seven : 7 ∈ {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))} := by
+  refine ⟨by norm_num, ?_⟩
+  rw [show (7 : ℕ) - 2 = 5 by norm_num, cardFactors_apply_prime (by norm_num)]
+  exact odd_one
+
+/-- $11$ does *not* satisfy the condition: although $11$ is prime, $11 - 2 = 9 = 3 ^ 2$ has
+$\Omega(9) = 2$ prime factors, which is even. This shows the condition is non-trivial. -/
+@[category test, AMS 11]
+theorem green_64_not_mem_eleven : 11 ∉ {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))} := by
+  rintro ⟨-, hodd⟩
+  rw [show (11 : ℕ) - 2 = 3 ^ 2 by norm_num, cardFactors_apply_prime_pow (by norm_num)] at hodd
+  exact (by decide : ¬ Odd 2) hodd
+
+end Green64