Revision #2404 → #3110 · back to history
modifiedGoldbach's conjecturecccbb1c49952
| Field | From #2404 | To #3110 |
|---|
| note | Grep finds no Goldbach conjecture statement in Mathlib; the only 'Goldbach' hit is the unrelated Fermat-numbers reference in NumberTheory/Fermat.lean line 98. | Grep confirms the only 'Goldbach' hit in Mathlib is an unrelated Fermat-numbers comment in NumberTheory/Fermat.lean; the conjecture is not stated. |
modifiedSchnirelmann densityfa8aaf8de896
| Field | From #2404 | To #3110 |
|---|
| note | Schnirelmann density is defined in Mathlib.Combinatorics.Schnirelmann as `schnirelmannDensity`. | decl_exists confirms `schnirelmannDensity` in Mathlib.Combinatorics.Schnirelmann. |
modifiedPrime number theoremcd1f62412191
| Field | From #2404 | To #3110 |
|---|
| mathlib.module_note | — | — |
modifiedTwin prime conjecture461ecaf9b81b
| Field | From #2404 | To #3110 |
|---|
| note | Grep for TwinPrime/twin.prime returns no hits; the twin prime conjecture is not formalized in Mathlib. | Grep for TwinPrime/twin_prime returns no hits; the twin prime conjecture is not formalized in Mathlib. |
modifiedLagrange's four-square theorem850222e8efeb
| Field | From #2404 | To #3110 |
|---|
| note | Nat.sum_four_squares in NumberTheory/SumFourSquares.lean states ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n. | decl_exists confirms Nat.sum_four_squares in Mathlib.NumberTheory.SumFourSquares. |
addedHardy–Littlewood prime tuple conjecture6efa2e50bf12
addedGoldbach's comet2f5a77039fa6
addedBusy Beaver function BB(n)039ecea51583