Artifact · conjectured
Strong Goldbach conjecture
This page records one proposition and the evidence attached to it. Text from the source ledger is shown as record data.
- Identifier
- F:goldbach-strong
- Proof route
- Not assigned
- External status
- open
- Axiom footprint
- Empty
Recorded description
Every even natural number that is at least 4 is the sum of two primes.
theorem Goldbach.strong : ((n : AxNat) -> ((h4 : AxNat.le (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))) n) -> ((heven : AxNat.dvd (AxNat.succ (AxNat.succ AxNat.zero)) n) -> Exists.{1} AxNat (fun (p : AxNat) => Exists.{1} AxNat (fun (q : AxNat) => And (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) p) ((d : AxNat) -> ((hd : AxNat.dvd d p) -> Or (Eq.{1} AxNat d (AxNat.succ AxNat.zero)) (Eq.{1} AxNat d p)))) (And (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) q) ((d : AxNat) -> ((hd : AxNat.dvd d q) -> Or (Eq.{1} AxNat d (AxNat.succ AxNat.zero)) (Eq.{1} AxNat d q)))) (Eq.{1} AxNat (AxNat.add p q) n)))))))Dependencies
The graph shows direct ledger edges. Follow a node to open its artifact page.
0 direct dependencies 0 direct dependents
Evidence
Provenance
{
"date": "2026-08-14",
"established_by": "not established in this ledger",
"source": "proposition extracted from the S:number strand of the math-education concept graph; statement authored here, nothing copied",
"prior_art": [
{
"citation": "Goldbach to Euler, 1742",
"establishes": "the conjecture; still open"
}
]
}