lean_workbook_plus_44749

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $a=\frac{\sqrt{6}+\sqrt{2}}{\sqrt{6}-\sqrt{2}},\ b=\frac{\sqrt{6}-\sqrt{2}}{\sqrt{6}+\sqrt{2}}.$ Find the values of $a-b,\ ab,\ a^2+b^2$ and $a^3-b^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44749 (a b : ℝ) (ha : a = (Real.sqrt 6 + Real.sqrt 2) / (Real.sqrt 6 - Real.sqrt 2)) (hb : b = (Real.sqrt 6 - Real.sqrt 2) / (Real.sqrt 6 + Real.sqrt 2)) : a - b = (Real.sqrt 6 + Real.sqrt 2) / (Real.sqrt 6 - Real.sqrt 2) - (Real.sqrt 6 - Real.sqrt 2) / (Real.sqrt 6 + Real.sqrt 2) ∧ a * b = (Real.sqrt 6 + Real.sqrt 2) / (Real.sqrt 6 - Real.sqrt 2) * (Real.sqrt 6 - Real.sqrt 2) / (Real.sqrt 6 + Real.sqrt 2) ∧ a ^ 2 + b ^ 2 = (Real.sqrt 6 + Real.sqrt 2) ^ 2 / (Real.sqrt 6 - Real.sqrt 2) ^ 2 + (Real.sqrt 6 - Real.sqrt 2) ^ 2 / (Real.sqrt 6 + Real.sqrt 2) ^ 2 ∧ a ^ 3 - b ^ 3 = (Real.sqrt 6 + Real.sqrt 2) ^ 3 / (Real.sqrt 6 - Real.sqrt 2) ^ 3 - (Real.sqrt 6 - Real.sqrt 2) ^ 3 / (Real.sqrt 6 + Real.sqrt 2) ^ 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph