Revision #2028 → #2404 · back to history
modifiedGoldbach's conjecturecccbb1c49952
| Field | From #2028 | To #2404 |
|---|
| note | Grep finds no Goldbach conjecture statement in Mathlib (the only 'Goldbach' hit is the unrelated Fermat-numbers reference 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 line 98. |
modifiedSchnirelmann's theorem (1930)44b30487b887
| Field | From #2028 | To #2404 |
|---|
| note | 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. | Schnirelmann density is defined in Combinatorics/Schnirelmann.lean, but the theorem itself (bounded representation by primes) is not yet formalized. |
addedSchnirelmann densityfa8aaf8de896
modifiedPrime number theoremcd1f62412191
| Field | From #2028 | To #2404 |
|---|
| note | decl_exists confirms no `PrimeNumberTheorem` decl and no Mathlib/NumberTheory/LSeries/PrimeNumberTheorem.lean file; only prerequisites are present (Nat.primeCounting, Chebyshev bounds like Chebyshev.eventually_primeCounting_le, and zeta non-vanishing in LSeries/Nonvanishing.lean which explicitly calls itself a PNT prerequisite), so PNT itself is not yet formalized. | Only PNT prerequisites (Nat.primeCounting, Chebyshev bounds, zeta non-vanishing) are present in Mathlib; the asymptotic π(n) ~ n/log n is not yet stated as a theorem. |
addedVinogradov's asymptotic (c ≥ 3)5a377e0658c1
addedTwin prime conjecture461ecaf9b81b
modifiedLagrange's four-square theorem850222e8efeb
| Field | From #2028 | To #2404 |
|---|
| note | 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). | Nat.sum_four_squares in NumberTheory/SumFourSquares.lean states ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n. |
addedWaring's problem745a6f5f16e7
modifiedLemoine's (Levy's) conjectureb1dd3898467a
| Field | From #2028 | To #2404 |
|---|
| note | Lemoine/Levy's conjecture is not present in Mathlib. | Grep for Lemoine returns no hits; the conjecture is not present in Mathlib. |