Back to Problems

not_first_and_secondHardyLittlewoodConjecture

Specification

Richards [Ri74] showed that only one of the two Hardy-Littlewood conjectures can be true. [Ri74] Richards, Ian (1974). _On the Incompatibility of Two Conjectures Concerning Primes_. Bull. Amer. Math. Soc. 80: 419–438.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem not_first_and_secondHardyLittlewoodConjecture :
    (∀ {k : ℕ} (m : Fin k.succ → ℕ), FirstHardyLittlewoodConjectureFor m) →
      ¬(∀ {x y : ℕ} (hx : 2 ≤ x) (hy : 2 ≤ y), SecondHardyLittlewoodConjectureFor x y)
ID: Wikipedia__HardyLittlewood__not_first_and_secondHardyLittlewoodConjecture
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.