The Hardy-Ramanujan number

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-12-06.
Last modified on 2024-10-16.

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

Recent changes