Nuprl Lemma : sum-of-three-cubes-iff

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

∀k:ℕ
  (∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
  ⇐⇒ ∃d,n:ℕ
       ((↑is_power(3;((2 * d) * ((d * d) + (3 * n * n))) - k))

       ∨ (↑is_power(3;(((2 * d) + 1) * (((d * (d + 1)) + (3 * n * (n + 1))) + 1)) - k))))

Proof

Definitions occuring in Statement : is_power: is_power(n;z), nat: ℕ, assert: ↑b, all: ∀x:A. B[x], exists: ∃x:A. B[x], iff: P ⇐⇒ Q, or: P ∨ Q, multiply: n * m, subtract: n - m, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], member: t ∈ T, iff: P ⇐⇒ Q, and: P ∧ Q, implies: P ⇒ Q, exists: ∃x:A. B[x], subtype_rel: A ⊆r B, nat: ℕ, uall: ∀[x:A]. B[x], so_lambda: λ₂x.t[x], so_apply: x[s], uimplies: b supposing a, rev_implies: P ⇐ Q, or: P ∨ Q, nat_plus: ℕ⁺, ge: i ≥ j , decidable: Dec(P), not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), top: Top, prop: ℙ, false: False, sq_type: SQType(T), guard: {T}, int_nzero: ℤ^-^o, true: True, nequal: a ≠ b ∈ T , exp: i^n, primrec: primrec(n;b;c), primtailrec: primtailrec(n;i;b;f), subtract: n - m, remainder: n rem m, squash: ↓T, cand: A c∧ B
Lemmas referenced : sum-of-three-cubes-iff-4, istype-int, int_subtype_base, set_subtype_base, le_wf, istype-assert, is_power_wf, nat_properties, decidable__lt, full-omega-unsat, intformnot_wf, intformless_wf, itermConstant_wf, int_formula_prop_not_lemma, istype-void, int_formula_prop_less_lemma, int_term_value_constant_lemma, int_formula_prop_wf, istype-less_than, subtract_wf, istype-nat, mod2-cases, decidable__le, intformand_wf, intformle_wf, itermVar_wf, intformeq_wf, itermMultiply_wf, int_formula_prop_and_lemma, int_formula_prop_le_lemma, int_term_value_var_lemma, int_formula_prop_eq_lemma, int_term_value_mul_lemma, subtype_base_sq, itermAdd_wf, int_term_value_add_lemma, mod2-is-zero, mod2-is-one, decidable__equal_int, div-cancel2, nequal_wf, istype-le, assert-is_power, add_nat_wf, multiply_nat_wf, equal_wf, squash_wf, true_wf, istype-universe, rem_invariant, subtype_rel_self, iff_weakening_equal, bool_wf, bool_subtype_base, nat_plus_wf, divide-exact, rem-exact
Rules used in proof : cut, introduction, extract_by_obid, sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, hypothesis, sqequalHypSubstitution, dependent_functionElimination, thin, hypothesisEquality, independent_pairFormation, productElimination, independent_functionElimination, sqequalRule, Error :productIsType, because_Cache, Error :equalityIstype, baseApply, closedConclusion, baseClosed, applyEquality, isectElimination, intEquality, Error :lambdaEquality_alt, natural_numberEquality, Error :inhabitedIsType, independent_isectElimination, sqequalBase, equalitySymmetry, Error :unionIsType, Error :dependent_set_memberEquality_alt, setElimination, rename, unionElimination, approximateComputation, Error :dependent_pairFormation_alt, Error :isect_memberEquality_alt, voidElimination, Error :universeIsType, multiplyEquality, addEquality, equalityTransitivity, int_eqEquality, promote_hyp, instantiate, cumulativity, Error :inlFormation_alt, Error :inrFormation_alt, applyLambdaEquality, imageElimination, universeEquality, imageMemberEquality

Latex:
\mforall{}k:\mBbbN{} (\mexists{}a,b,c:\mBbbZ{}. (((a * a * a) + (b * b * b) + (c * c * c)) = k) \mLeftarrow{}{}\mRightarrow{} \mexists{}d,n:\mBbbN{} ((\muparrow{}is\_power(3;((2 * d) * ((d * d) + (3 * n * n))) - k)) \mvee{} (\muparrow{}is\_power(3;(((2 * d) + 1) * (((d * (d + 1)) + (3 * n * (n + 1))) + 1)) - k)))) Date html generated: 2019_06_20-PM-02_42_43 Last ObjectModification: 2019_03_19-PM-00_29_52 Theory : num_thy_1 Home Index