Stanford University

Formalizing the future of mathematics.

We are a community of researchers and students at Stanford dedicated to advancing the use of AI in Lean theorem proving.

proof.lean

theorem infinitude_of_primes :

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

-- Let N be a natural number...

have : p.Prime := by

...

Stanford

Lean 4

Mathlib

Autoformalization