The Hardy-Ramanujan number
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-12-06.
Last modified on 2024-01-14.
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
External links
- 1729 at Mathswitch
- 1729 (number) at Wikipedia
Recent changes
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).
- 2023-12-06. Egbert Rijke. The Hardy-Ramanujan number (#970).