OP-00002 Open

The twin prime conjecture

Are there infinitely many primes p such that p + 2 is prime?

Source: The gap-2 case of de Polignac's conjecture (C. R. Acad. Sci. Paris 29, 1849); stated for prime pairs by Glaisher (1878) and listed by Landau at the 1912 ICM. See Guy, Unsolved Problems in Number Theory, A8.

Classification

Primary: NT — Number Theory
Keywords: Landau's problems, prime gaps

References

@article{polignac1849,
  author = {de Polignac, Alphonse},
  title = {Recherches nouvelles sur les nombres premiers},
  journal = {Comptes Rendus de l'Acad{\'e}mie des Sciences, Paris},
  volume = {29},
  pages = {397--401},
  year = {1849}
}

@inproceedings{landau1912,
  author = {Landau, Edmund},
  title = {Gel{\"o}ste und ungel{\"o}ste Probleme aus der Theorie der Primzahlverteilung und der Riemannschen Zetafunktion},
  booktitle = {Proceedings of the Fifth International Congress of Mathematicians (Cambridge, 1912)},
  volume = {1},
  pages = {93--108},
  year = {1913}
}

@book{guy2004,
  author = {Guy, Richard K.},
  title = {Unsolved Problems in Number Theory},
  edition = {3},
  publisher = {Springer},
  year = {2004}
}

@article{polymath8b,
  author = {Polymath, D. H. J.},
  title = {Variants of the {S}elberg sieve, and bounded intervals containing many primes},
  journal = {Research in the Mathematical Sciences},
  volume = {1},
  pages = {12},
  year = {2014}
}

@misc{wikipedia,
  title = {Twin prime},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/Twin_prime}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/Wikipedia/TwinPrimes.lean#L33},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00002.

/-- OP-00002: The twin prime conjecture -/
def Problem_OP_00002 : Prop :=
  {p | Prime p ∧ Prime (p + 2)}.Infinite

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00002

theorem resolution : RegistryProblems.Problem_OP_00002 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00002"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00002 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00002, "The twin prime conjecture", clopen.solutions.