Stanford University

Formalizing the future of mathematics.

We are a community of researchers and students at Stanford dedicated to advancing the formalization of mathematics in Lean.

proof.lean

theorem infinitude_of_primes :

∀ N, ∃ p, p ≥ N ∧ p.Prime := by

-- Let N be a natural number...

have : p.Prime := by

...