1. FormalConjectures
  2. Wikipedia
  3. BealConjecture
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Beal conjecture

Reference: Wikipedia

namespace BealConjecture def bealConjecture : Prop := ∀ {A B C x y z : ℕ}, A ≠ 0 → B ≠ 0 → C ≠ 0 → 2 < x → 2 < y → 2 < z → A^x + B^y = C^z → 1 < Finset.gcd {A, B, C} id

The Beal Conjecture: if we are given positive integers $A, B, C, x, y, z$ such that $x, y, z > 2$ and $A^x + B^y = C^z$ then $A, B, C$ have a common divisor.

@[category research open, AMS 11] theorem declaration uses 'sorry'beal_conjecture : bealConjecture := ⊢ bealConjecture All goals completed! 🐙

The Beal Conjecture implies Fermat's last theorem

@[category textbook, AMS 11] theorem flt_of_beal_conjecture (H : bealConjecture) : FermatLastTheorem := H:bealConjecture⊢ FermatLastTheorem intro n H:bealConjecturen:ℕhn:n ≥ 3⊢ FermatLastTheoremFor n H:bealConjecturen:ℕhn:n ≥ 3x:ℕ⊢ ∀ (b c : ℕ), x ≠ 0 → b ≠ 0 → c ≠ 0 → x ^ n + b ^ n ≠ c ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕ⊢ ∀ (c : ℕ), x ≠ 0 → y ≠ 0 → c ≠ 0 → x ^ n + y ^ n ≠ c ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕ⊢ x ≠ 0 → y ≠ 0 → z ≠ 0 → x ^ n + y ^ n ≠ z ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0⊢ y ≠ 0 → z ≠ 0 → x ^ n + y ^ n ≠ z ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0⊢ z ≠ 0 → x ^ n + y ^ n ≠ z ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0⊢ x ^ n + y ^ n ≠ z ^ n H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ n⊢ False H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ n⊢ x * y * z = 0 H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0⊢ False obtain ⟨hx, hy, hz⟩ : x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 := H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0⊢ x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 All goals completed! 🐙 H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd id⊢ False H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / G⊢ False H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / G⊢ False H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ False obtain ⟨hGx, hGy, hGz⟩ : G ∣ x ∧ G ∣ y ∧ G ∣ z := H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ x ∧ G ∣ y ∧ G ∣ z H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ xH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ yH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ z H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ xH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ yH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ z apply Finset.gcd_dvd (H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ z ∈ {x, y, z} All goals completed! 🐙) obtain ⟨hx', hy', hz'⟩ : x' ≠ 0 ∧ y' ≠ 0 ∧ z' ≠ 0 := H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0 ∧ y' ≠ 0 ∧ z' ≠ 0 H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ y' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z' ≠ 0 H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ y' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z' ≠ 0 apply Nat.div_ne_zero_iff_of_dvd (H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ∣ z All goals completed! 🐙) |>.mpr ⟨(H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z ≠ 0 All goals completed! 🐙), _⟩ H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0 All goals completed! 🐙 have Hxyz' : x'^n + y'^n = z'^n := H:bealConjecture⊢ FermatLastTheorem rwa [Nat.div_pow hGx, Nat.div_pow hGy, Nat.div_pow hGz, ←Nat.add_div_of_dvd_right, Nat.div_left_inj (dvd_add _ _)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n + y ^ n = z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ y ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ n all_goals H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ∣ x ; All goals completed! 🐙 H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n := Eq.mpr (id (congrArg (fun _a => _a + y' ^ n = z' ^ n) (Nat.div_pow hGx))) (Eq.mpr (id (congrArg (fun _a => x ^ n / G ^ n + _a = z' ^ n) (Nat.div_pow hGy))) (Eq.mpr (id (congrArg (fun _a => x ^ n / G ^ n + y ^ n / G ^ n = _a) (Nat.div_pow hGz))) (Eq.mpr (id (congrArg (fun _a => _a = z ^ n / G ^ n) (Eq.symm (Nat.add_div_of_dvd_right (pow_dvd_pow_of_dvd hGx n))))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Nat.div_left_inj (dvd_add (pow_dvd_pow_of_dvd hGx n) (pow_dvd_pow_of_dvd hGy n)) (pow_dvd_pow_of_dvd hGz n))))) h))))⊢ 1 = {x', y', z'}.gcd id All goals completed! 🐙 end BealConjecture