Nuprl Lemma : 33-is-sum-of-three-cubes-implies

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 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).⋅

d,n:ℕ
 ((∃c:ℤ((((2 d) ((d d) (3 n))) 33) (c c) ∈ ℤ))
 ∨ (∃c:ℤ(((((2 d) 1) (((d (d 1)) (3 (n 1))) 1)) 33) (c c) ∈ ℤ)))


Proof




Definitions occuring in Statement :  nat: exists: x:A. B[x] or: P ∨ Q multiply: m subtract: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) not: ¬A implies:  Q false: False uall: [x:A]. B[x] iff: ⇐⇒ Q nat_plus: + rev_implies:  Q ge: i ≥  exists: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) guard: {T} exp: i^n primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) subtract: m
Lemmas referenced :  sum-of-three-cubes-iff istype-void istype-le nat_properties decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf istype-int int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than subtract_wf set_subtype_base le_wf int_subtype_base 33-is-sum-of-three-cubes subtype_base_sq decidable__equal_int intformeq_wf itermMultiply_wf itermVar_wf int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma assert-is_power
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin Error :dependent_set_memberEquality_alt,  natural_numberEquality independent_pairFormation sqequalRule Error :lambdaFormation_alt,  voidElimination hypothesis isectElimination hypothesisEquality productElimination setElimination rename unionElimination independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :isect_memberEquality_alt,  Error :universeIsType,  multiplyEquality addEquality because_Cache Error :productIsType,  Error :equalityIstype,  baseApply closedConclusion baseClosed applyEquality intEquality Error :inhabitedIsType,  sqequalBase equalitySymmetry Error :unionIsType,  Error :inlFormation_alt,  instantiate cumulativity equalityTransitivity int_eqEquality Error :inrFormation_alt

Latex:
\mexists{}d,n:\mBbbN{}
  ((\mexists{}c:\mBbbZ{}.  ((((2  *  d)  *  ((d  *  d)  +  (3  *  n  *  n)))  -  33)  =  (c  *  c  *  c)))
  \mvee{}  (\mexists{}c:\mBbbZ{}.  (((((2  *  d)  +  1)  *  (((d  *  (d  +  1))  +  (3  *  n  *  (n  +  1)))  +  1))  -  33)  =  (c  *  c  *  c))))



Date html generated: 2019_06_20-PM-02_42_54
Last ObjectModification: 2019_04_11-AM-09_53_09

Theory : num_thy_1


Home Index