# The Hardy-Ramanujan number

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-06.

module elementary-number-theory.hardy-ramanujan-number where

Imports
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.taxicab-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unit-type


## Idea

The Hardy-Ramanujan number is the number 1729. This number is the second taxicab number, i.e., it is the least natural number that can be written as a sum of cubes of positive natural numbers in exactly two distinct ways. Specifically, we have the identifications

  1³ + 12³ ＝ 1729    and    9³ + 10³ ＝ 1729.


## Definition

### The Hardy-Ramanujan number

Hardy-Ramanujan-ℕ : ℕ
Hardy-Ramanujan-ℕ = 1729


## Properties

### Two decompositions of the Hardy-Ramanujan number into sums of cubes of two positive natural numbers

first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
pr1 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
(1 , is-nonzero-one-ℕ)
pr1 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
(12 , is-nonzero-succ-ℕ 11)
pr1 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
star
pr2 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
refl

second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
pr1 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
(9 , is-nonzero-succ-ℕ 8)
pr1 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
(10 , is-nonzero-succ-ℕ 9)
pr1 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
star
pr2 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
refl