Richards: the two Hardy–Littlewood conjectures are incompatible
ProvedHardyLittlewood.richards_incompatibilityRichards' theorem: the first Hardy–Littlewood conjecture, asserted for every tuple, and the second Hardy–Littlewood conjecture, asserted for every pair x, y ≥ 2, cannot both be true. The first conjecture produces, in a short interval, more primes than the subadditivity of the second conjecture permits. At most one of the two 1923 conjectures survives.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- Richards' incompatibility theorem: the first Hardy–Littlewood conjecture,
asserted for every tuple, and the second Hardy–Littlewood conjecture, asserted
for every pair x, y ≥ 2, cannot both be true. -/
theorem richards_incompatibility
(h1 : ∀ (k : ℕ) (m : Fin k.succ → ℕ), firstHardyLittlewoodFor m)
(h2 : ∀ (x y : ℕ), 2 ≤ x → 2 ≤ y → secondHardyLittlewoodFor x y) :
False := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: it is impossible that both of the following hold — first, that for every natural number k and every function m from {0, 1, ..., k} to the natural numbers, the first Hardy–Littlewood conjecture holds for m (whenever m evaluated at 0 is 0 and m is injective, the counting sequence of admissible constellations is asymptotic to the singular-series constant times the logarithmic integral); and second, that for all natural numbers x and y with x at least 2 and y at least 2, the number of primes at most x + y is at most the number of primes at most x plus the number of primes at most y.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.