Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Problem NT-001

Conjectura.Problems.NT001.Statement

/-
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
-/
import Conjectura.Statements.Mathematics.NumberTheory.InfinitelyManyPrimes

/-! # Problem NT-001

Problem NT-001 — Infinitude of primes

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.NT001

/-- For every `n` there is a prime at least as large as `n`. -/
def goal : Prop := Conjectura.NumberTheory.InfinitelyManyPrimes

end Conjectura.NT001