Revision #3110 → #3613 · back to history
modifiedGoldbach's conjecturecccbb1c49952
| Field | From #3110 | To #3613 |
|---|
| note | Grep confirms the only 'Goldbach' hit in Mathlib is an unrelated Fermat-numbers comment in NumberTheory/Fermat.lean; the conjecture is not stated. | Confirmed: the only Mathlib hit for 'Goldbach' is an unrelated comment in NumberTheory/Fermat.lean. |
addedDensity zero of Goldbach exceptionse9bcd74702ae
modifiedTwin prime conjecture461ecaf9b81b
| Field | From #3110 | To #3613 |
|---|
| note | Grep for TwinPrime/twin_prime returns no hits; the twin prime conjecture is not formalized in Mathlib. | Grep for twin.?[Pp]rime returns no hits; the twin prime conjecture is not formalized in Mathlib. |
modifiedBusy Beaver function BB(n)039ecea51583
| Field | From #3110 | To #3613 |
|---|
| note | The Busy Beaver function is not defined in Mathlib. | Grep for busy.?beaver returns no hits; the Busy Beaver function is not defined in Mathlib. |