Back to Problems

infinitely_many_even_perfect

Specification

**Infinitely many even perfect numbers conjecture.** Are there infinitely many even perfect numbers? This is equivalent to asking whether there are infinitely many Mersenne primes, since by the Euclid–Euler theorem an even number is perfect if and only if it has the form $2^{p-1}(2^p - 1)$ where $2^p - 1$ is a Mersenne prime. *Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Perfect_number)

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem infinitely_many_even_perfect :
    answer(sorry) ↔ {n : ℕ | Perfect n ∧ Even n}.Infinite
ID: Wikipedia__PerfectNumbers__infinitely_many_even_perfect
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.