Documentation

FormalConjectures.Wikipedia.Taxicab

Taxicab numbers #

A taxicab number for natural numbers $k, m, n$ is the smallest number $x$ that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways. The most famous taxicab number is $ 1729 = 1³ + 12³ = 9³ + 10³, $ also known as the Hardy–Ramanujan number.

However, a taxicab number is not known for $k=5$, $m=2$, and any $n ≥ 2$: No positive integer is known that can be written as the sum of two 5th powers in more than one way, and it is not known whether such a number exists.

In particular, it is not known whether there exists a taxicab number for $k=5$, $m=2$, and $n=2$.

References:

source
def Taxicab.IsTaxicabFor' (k m n x : ℕ) :
Prop

$x$ is a candidate for being a taxicab number for $k, m, n$ if there exists a (finite) set of at least $n$ distinct, pairwise disjoint, non-empty, non-zero lists of length $m$, such that the sum of the $k$-th powers of the elements of each list is $x$. The disjointness condition ensures that the representations do not share any common terms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Taxicab.taxicab_1729 :
    IsTaxicabFor' 3 2 2 1729

    $1729$ is a possible taxicab number for $k=3, m=2, n=2$.

    source
    def Taxicab.IsTaxicabFor (k m n x : ℕ) :
    Prop

    $x$ is a taxicab number if it is the smallest number that can be expressed as a sum of $m$ positive $k$-th powers in at least $n$ distinct ways.

    Equations
    Instances For
      source
      theorem Taxicab.taxicab_4' :
      IsTaxicabFor' 1 2 2 4
      source
      theorem Taxicab.taxicab_4 :
      IsTaxicabFor 1 2 2 4

      Using Aristotle (Harmonic) we get a compact proof that 4 is the taxicab number for $k=1, m=2, n=2$.

      source
      theorem Taxicab.taxicab_for_5_2_2 :
      True ↔ ∃ (x : ℕ), IsTaxicabFor 5 2 2 x

      Taxicab number for $k=5$, $m=2$, and $n=2$ is not known. Whether such a number exists is also not known.

      source
      theorem Taxicab.taxicab_for_5_2_n :
      True ↔ ∃ n ≥ 2, ∃ (x : ℕ), IsTaxicabFor 5 2 n x

      Taxicab number for $k=5$ and $m=2$ is not-known for any $n ≥ 2$. Whether such a number exists is also not known.