Revision #968 → #3332 · back to history
modifiedTaxicab number (1729)15dd2005e918
| Field | From #968 | To #3332 |
|---|
| note | No taxicab-number definition or instance for 1729 found in Mathlib. | Grep for 'Taxicab' in Mathlib returns no results; no taxicab-number definition exists. |
modifiedRamanujan/Hardy–Ramanujan number3ed6268ae1cc
| Field | From #968 | To #3332 |
|---|
| note | Grepping for `Ramanujan` only yields modular forms / Chudnovsky references, not a Hardy–Ramanujan number definition. | The only 'Ramanujan' hits in Mathlib are Chudnovsky's π formula and modular-forms derivatives, not the Hardy–Ramanujan number. |
modified1729 is composite, taxicab, and Carmichael09a4efab74e9
| Field | From #968 | To #3332 |
|---|
| note | Mathlib's `Carmichael` is the reduced-totient function, not the Carmichael-number property; FermatPsp.lean explicitly notes Carmichael numbers are not yet defined. | Mathlib's `ArithmeticFunction.carmichael` is the reduced-totient function and `FermatPsp.lean` states Carmichael numbers are 'not yet defined'; no taxicab notion either. |
modifiedSmallest absolute Euler pseudoprime0fe0c61fcf08
| Field | From #968 | To #3332 |
|---|
| note | No Euler-pseudoprime or absolute-Euler-pseudoprime declaration exists in Mathlib (only Fermat pseudoprimes). | Grep for 'Euler.*[Pp]seudoprime' finds nothing; only Fermat pseudoprimes are defined in Mathlib. |
modifiedDimension of Fourier transform for fast multiplication484a9b76d171
| Field | From #968 | To #3332 |
|---|
| note | Mathlib does not formalize the Harvey–van der Hoeven multiplication algorithm or its 1729-dim Fourier transform. | No Harvey–van der Hoeven multiplication algorithm or associated 1729-dimensional Fourier transform is present in Mathlib. |
modifiedGalactic algorithm examplee87241550d77
| Field | From #968 | To #3332 |
|---|
| note | No notion of 'galactic algorithm' is present in Mathlib. | Grep for 'galactic' returns no results in Mathlib. |
modifiedSchiemann's quadratic form result6b27223fe78b
| Field | From #968 | To #3332 |
|---|
| note | No reference to Schiemann or this isospectral-quadratic-form result is in Mathlib. | Grep for 'Schiemann' returns no results; the isospectral-quadratic-form result is not in Mathlib. |
modifiedFirst Fermat near missae1343b52be5
| Field | From #968 | To #3332 |
|---|
| note | The 'Fermat near miss' concept (a^3 + b^3 = c^3 ± 1) has no formalization in Mathlib. | Grep for 'Fermat.*[Nn]ear' returns no hits; the a^3+b^3=c^3±1 near-miss concept is not formalized. |
modified1729 as second taxicab numbera3112e0dd64a
| Field | From #968 | To #3332 |
|---|
| note | Without a taxicab-number definition in Mathlib, the statement that 1729 = Ta(2) is not formalized. | Without a taxicab-number definition or Ta(n) function in Mathlib, the statement 1729 = Ta(2) is not formalized. |