The twin prime conjecture follows from the first Hardy–Littlewood conjecture
ProvedHardyLittlewood.twin_primes_from_firstSpecializing the first Hardy–Littlewood conjecture to the twin offsets (0, 1): if the conjecture holds for the constellation (p, p + 2), then there are infinitely many twin primes — for every N there is a prime p ≥ N with p + 2 also prime.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The twin prime conjecture follows from the first Hardy–Littlewood
conjecture for the twin offsets (0, 1): there are twin primes p, p + 2 with
arbitrarily large p. -/
theorem twin_primes_from_first
(h : firstHardyLittlewoodFor (![0, 1] : Fin 2 → ℕ)) (N : ℕ) :
∃ p : ℕ, N ≤ p ∧ p.Prime ∧ (p + 2).Prime := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: if the first Hardy–Littlewood conjecture holds for the tuple assigning offsets 0 and 1 to the indices 0 and 1 — meaning the counting function of twin-constellation base points is asymptotic to the singular series of the twin offsets times the integral of 1/(log t)² from 2 to n — then for every natural number N there exists a natural number p at least N such that p is prime and p + 2 is prime.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.