Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Add the first piece

Even one lemma helps. Whoever finishes this later shares the pool with everyone who got them there.

contrib new wikipedia-hardylittlewood-first-hardy-littlewood-conjecture

Command line, then a pull request on GitHub.

Formal statement

Proof target

import FormalConjectures.Wikipedia.HardyLittlewood
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "HardyLittlewood.first_hardy_littlewood_conjecture" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ {k : ℕ} (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m

Original conjecture source: FormalConjectures/Wikipedia/HardyLittlewood.lean

Source type SHA-256: sha256:115d3ca4efee8567e3fd85b1b525c3a55dfc0282397397bf3b4872ff2d4d1f25
Task id: fc-6a786f99-hardylittlewood-first-hardy-littlewood-conjecture-367be1c96b-formalized-v1
Task commitment: sha256:01c34dff2b869a49867d8c6c45fab763b0c6b1c4dd128e9ad92551beba3735e7

References

Hardy Littlewood - first hardy littlewood conjecture · Conjectures.io

Every problem here was open when it entered the pool.

Hardy Littlewood - first hardy littlewood conjecture

Solve it

Add the first piece

What has been built

Where this lives