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 →

Goldbach conjecture

GoldbachConjecturePropdef

The Goldbach conjecture: every even number greater than two is a sum of two primes.

def GoldbachConjectureProp : Prop :=
  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ n = p + q

Used by

From Mathlib

import Conjectura.Statements.Mathematics.NumberTheory.GoldbachConjecture · 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

Full credits