Revision #1268 → #2028 · back to history
modifiedGoldbach's conjecturecccbb1c49952
| Field | From #1268 | To #2028 |
|---|
| note | Grep shows no Goldbach conjecture statement in Mathlib (the only 'Goldbach' hit is the unrelated Fermat-numbers theorem in NumberTheory/Fermat.lean). | Grep finds no Goldbach conjecture statement in Mathlib (the only 'Goldbach' hit is the unrelated Fermat-numbers reference in NumberTheory/Fermat.lean). |
addedWeak Goldbach conjecture (ternary)ef3eddb811ab
modifiedSchnirelmann's theorem (1930)44b30487b887
| Field | From #1268 | To #2028 |
|---|
| note | Schnirelmann density is defined in Combinatorics/Schnirelmann.lean, but the file's TODO explicitly lists 'Prove Schnirelmann's theorem' so the theorem itself is not yet formalized. | Schnirelmann density is defined in Combinatorics/Schnirelmann.lean (decl_exists confirmed), but the file's TODO explicitly lists 'Prove Schnirelmann's theorem' so the theorem itself is not yet formalized. |
addedHelfgott's proof of the weak conjecture (2013)4564fba6a2ac
addedPrime number theoremcd1f62412191
modifiedLagrange's four-square theorem850222e8efeb
| Field | From #1268 | To #2028 |
|---|
| note | Nat.sum_four_squares in NumberTheory/SumFourSquares.lean states ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n. | Nat.sum_four_squares in NumberTheory/SumFourSquares.lean states ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n (confirmed via decl_exists). |