There are infinitely many primes
For every natural number n there exists a prime p with p ≥ n. A warm-up problem: short to state, short to prove, and a good way to check your setup works.
▸Motivation
Euclid's theorem, c. 300 BC. The classical argument: given any finite set of primes, their product plus one has a prime factor not among them.
This is included as a warm-up so that a visitor can complete the submission loop in a single sitting. It is not an open problem, and Mathlib already contains it as Nat.exists_infinite_primes — which is a legitimate way to solve it here.
Euclid, Elements IX.20. Present in Mathlib as Nat.exists_infinite_primes.
▸Lean API
import Conjectura.Statements.Mathematics.NumberTheory.InfinitelyManyPrimes
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▸Definition2
- Infinitely many primesConjectura.NumberTheory.InfinitelyManyPrimes
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.Prime- Primep.Prime
def
▸Related work1
- Nat.exists_infinite_primes — MathlibMathlib
The statement already exists in Mathlib. Using it directly is a legitimate solution.
▸For your AI
I am proving a theorem in Lean 4 and submitting it to Conjectura.
## Problem NT001 — There are infinitely many primes
For every natural number n there exists a prime p with p ≥ n. A warm-up problem: short to state, short to prove, and a good way to check your setup works.
## Environment (fixed — do not assume anything newer)
- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`
If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.
## The exact statement I must prove
```lean
theorem solution (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
sorry
```
## The file I submit
```lean
-- Problem NT-001 — submission template
-- Environment: leanprover/lean4:v4.33.0-rc1 · mathlib v4.33.0-rc1
import Conjectura.Problems.NT001.Statement
namespace Submission
/-- Replace `sorry` with your proof. Do not change this signature. -/
theorem solution : Conjectura.NT001.goal := by
sorry
end Submission
```
## The Lean definitions of every term in this problem
These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.
### Infinitely many primes
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.
```lean
Conjectura.NumberTheory.InfinitelyManyPrimes
-- unfolds to:
def InfinitelyManyPrimes : Prop := ∀ N : ℕ, ∃ p : ℕ, N ≤ p ∧ p.Prime
```
Defined in this corpus.
### Prime
def
```lean
p.Prime
```
Defined in Mathlib.
## Rules — submissions violating these are rejected automatically
1. **Do not change the name or type of `solution`.** It must satisfy the
statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
Declaring your own `goal`, or redefining a name it depends on, produces a
proof of a *different* statement and is rejected. This is the single most
common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
`Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
`snake_case` theorem names, `UpperCamelCase` types.
## What I want from you
Here is my argument in informal mathematics:
> [PASTE YOUR PROOF SKETCH HERE]
Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.Solved — closed to submissions
Passed submission on file.
New ideas
Nothing here yet.
Discussion
- Nothing yet.
Sign in to take part.