OP-00003 Open

Legendre's conjecture

Does there always exist at least one prime between consecutive perfect squares?

Source: Landau, ICM Cambridge 1912, one of his four problems; named after Legendre, Essai sur la théorie des nombres (2nd ed., 1808), who claimed a stronger statement with a flawed argument.

Classification

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

References

@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{legendre1808,
  author = {Legendre, Adrien-Marie},
  title = {Essai sur la th{\'e}orie des nombres},
  edition = {2},
  publisher = {Courcier},
  address = {Paris},
  year = {1808}
}

@misc{wikipedia,
  title = {Legendre's conjecture},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/Legendre%27s_conjecture}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/Wikipedia/LegendreConjecture.lean#L34},
  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_00003.

/-- OP-00003: Legendre's conjecture -/
def Problem_OP_00003 : Prop :=
  ∀ n ≥ 1, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

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_00003

theorem resolution : RegistryProblems.Problem_OP_00003 := by
  sorry

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

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

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

theorem disproof : ¬ RegistryProblems.Problem_OP_00003 := 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.

Status history

When	Change	By	Reason
2026-09-29	Partially resolved → Open	clemens-admin	"A great Test Submission" removed by an admin.
2026-09-28	Open → Partially resolved	—	A great Test Submission v1 announced.

Citing this problem

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

OP-00003, "Legendre's conjecture", clopen.solutions.