Infinitude of primes
InfinitelyManyPrimesdef
Infinitely many primes: for every bound there is a prime beyond it. Euclid's theorem; present here as the smallest non-trivial statement in the corpus, useful as a worked example.
def InfinitelyManyPrimes : Prop := ∀ N : ℕ, ∃ p : ℕ, N ≤ p ∧ p.PrimeUsed by
From Mathlib
import Conjectura.Statements.Mathematics.NumberTheory.InfinitelyManyPrimes · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors