/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilGoldbach's conjecture
namespace GoldbachConjecture
Can every even integer greater than 2 be written as the sum of two primes?
@[category research open, AMS 11]
theorem goldbach :
answer(sorry) ↔ ∀ n : ℕ, 2 < n → Even n → ∃ p q, Prime p ∧ Prime q ∧ n = p + q := ⊢ True ↔ ∀ (n : ℕ), 2 < n → Even n → ∃ p q, Prime p ∧ Prime q ∧ n = p + q
All goals completed! 🐙
end GoldbachConjecture
namespace TernaryGoldbachConjecture
Can every odd integer greater than 5 be written as the sum of three primes? (A prime may be used more than once.)
NB. While Harald Helfgott's solution is not published in a peer-reviewed journal yet, his results seem generally accepted.
@[category research solved, AMS 11]
theorem ternaryGoldbach (n : ℕ) (hn : 5 < n) (hn_odd : Odd n) :
∃ p q r, Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r := n:ℕhn:5 < nhn_odd:Odd n⊢ ∃ p q r, Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r
All goals completed! 🐙
end TernaryGoldbachConjecture