Nuprl Lemma : 33-is-sum-of-three-cubes
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = 33 ∈ ℤ)
Proof
Definitions occuring in Statement :
exists: ∃x:A. B[x],
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
exists: ∃x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
top: Top,
subtype_rel: A ⊆r B
Lemmas referenced :
mul-associates,
istype-void,
mul-commutes,
add-swap,
add-associates,
add-commutes,
int_subtype_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :dependent_pairFormation_alt,
natural_numberEquality,
minusEquality,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
Error :isect_memberEquality_alt,
voidElimination,
hypothesis,
Error :equalityIstype,
Error :inhabitedIsType,
hypothesisEquality,
baseApply,
closedConclusion,
baseClosed,
applyEquality,
sqequalBase,
equalitySymmetry,
Error :productIsType,
because_Cache
Latex:
\mexists{}a,b,c:\mBbbZ{}. (((a * a * a) + (b * b * b) + (c * c * c)) = 33)
Date html generated:
2019_06_20-PM-02_42_48
Last ObjectModification:
2019_03_16-PM-00_59_30
Theory : num_thy_1
Home
Index