The Goldbach conjecture
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Maša Žaucer.
Created on 2022-01-26.
Last modified on 2023-05-13.
module elementary-number-theory.goldbach-conjecture where
Imports
open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.parity-natural-numbers open import elementary-number-theory.prime-numbers open import elementary-number-theory.strict-inequality-natural-numbers open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels
Conjecture
Goldbach-conjecture : UU lzero Goldbach-conjecture = ( n : ℕ) → (le-ℕ 2 n) → (is-even-ℕ n) → Σ ℕ (λ p → (is-prime-ℕ p) × (Σ ℕ (λ q → (is-prime-ℕ q) × (p +ℕ q = n))))
Recent changes
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-18. Egbert Rijke and Maša Žaucer. Central elements in semigroups, monoids, groups, semirings, and rings; ideals; nilpotent elements in semirings, rings, commutative semirings, and commutative rings; the nilradical of a commutative ring (#516).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).