Machine Logic

An irrationality proof involving cube roots

08 Feb 2023

According to myth, the discovery that √2 was irrational so horrified the students of Pythagoras that it was kept secret upon pain of death. Its irrationality was thought to be paradoxical because √2 could be constructed as the hypotenuse of a right triangle, and therefore definitely “existed”, while all numbers were assumed to be rational. A while back, I formalised a new proof of the irrationality of √2. Just recently, I stumbled upon an exam question: to prove the irrationality of ∛2+∛3. Its proof uses different techniques, but it’s not at all hard. Why not pause for a moment to prove it for yourself before looking at the formal treatment below?

The informal proof

Let’s begin by defining $x = \sqrt[3]2+\sqrt[3]3$. It’s natural to see what happens if we cube both sides. Multiplying out and collecting the terms on the right hand side, we find that $x^3 = 5 + 3x\sqrt[3]6$. But this can’t be right: if $x$ is rational then so is $x^3$, which equals the right hand side, which must also be rational. In that case, $\sqrt[3]6$ is a rational number. It obviously isn’t.

Formalising this argument in Isabelle/HOL, we get a nice Isar proof.

The calculation

We begin by stating the desired claim. A rather obscure feature of Isar syntax is the ability to make a definition right in the theorem statement. Any such definitions will be expanded in the final theorem, once we have proved it.

lemma cuberoot_irrational:
  defines "x ≡ root 3 2 + root 3 3"
  shows "x ∉ ℚ"

Now we commence the proof. Another Isar fine point: omitting the proof method after the proof keyword calls for the default method, which in this case is to assume the formula, stripped of its initial negation. In order to obtain the number 5 without complications, we pre-evaluate the cube roots of 8 and 27. As in the informal proof, we quickly deduce that the right-hand side is rational.

proof
  assume "x ∈ ℚ"
  moreover
  have "root 3 8 = 2" "root 3 27 = 3"
    by auto
  then have xcubed: "x^3 = 5 + 3 * x * root 3 6"
    by (simp add: x_def algebra_simps eval_nat_numeral flip: real_root_mult)
  ultimately have Q: "5 + 3 * x * root 3 6 ∈ ℚ"
    by (metis Rats_power ‹x ∈ ℚ›)

A nested proof

We could have proved that $\sqrt[3]6$ is irrational separately, but we can just as easily embed it in the larger proof. The argument should be familiar: we write $\sqrt[3]6$ as $a/b$, the ratio of two coprime integers. We then demonstrate that both $a$ and $b$ are divisible by two. See if you can follow the reasoning in the Isar text below.

  have "root 3 6 ∉ ℚ"
  proof
    assume "root 3 6 ∈ ℚ"
    then obtain a b where "a / b = root 3 6" and cop: "coprime a b" "b≠0"
      by (smt (verit, best) Rats_cases')
    then have "(a/b)^3 = 6"
      by auto
    then have eq: "a^3 = 2*3 * b^3"
      using of_int_eq_iff by (fastforce simp: divide_simps ‹b≠0›)
    then have p: "2 dvd a"
      by (metis coprime_left_2_iff_odd coprime_power_right_iff dvd_triv_left mult.assoc)
    then obtain c where "a = 2*c"
      by blast
    with eq have "2 dvd b"
      by (simp add: eval_nat_numeral) (metis even_mult_iff even_numeral odd_numeral)
    with p and cop show False
      by fastforce
  qed

Finishing up

We know that the right side of our calculation above must be rational, although $\sqrt[3]6$ is irrational. Just a tiny bit more work remains. We need to show that $3x$ is nonzero as well as rational. Given that extra fact, the contradiction is found automatically, thanks to Sledgehammer.

  moreover have "3*x ∈ ℚ - {0}"
    using xcubed  by (force simp: ‹x ∈ ℚ›)
  ultimately have "3 * x * root 3 6 ∉ ℚ"
    using Rats_divide by force
  with Q show False
    by (metis Rats_diff Rats_number_of add.commute add_uminus_conv_diff diff_add_cancel)
qed

Another Isar fine point: note how moreover is used to collect facts. Each instance of moreover records the fact just proved, and this sequence terminates with ultimately, when all the recorded facts are made available to the next proof method. Above, ultimately delivers two facts (that $\sqrt[3]6$ is irrational and that $3x$ is a nonzero rational) to conclude that $3x\sqrt[3]6$ is irrational. The point of moreover/ultimately is to reduce our reliance on labels.

The Isabelle theory file is available to download. You can also check out a much more sophisticated proof, that exponentials are irrational.