Formal target: Corpus.WikipediaCatalan.pillais_conjecture

For positive integers a, b, and c, there are only finitely many positive solutions (x, y, m, n) to the equation $ax^n - by^m = c$ where $(m, n) \neq (2, 2)$ and $x, y > 1$.

Exact formal statement

∀ (a b c : Nat),
  LT.lt.{0} 0 a →
    LT.lt.{0} 0 b →
      LT.lt.{0} 0 c →
        Set.Finite.{0}
          (Set.ofPred.{0} fun x =>
            Corpus.WikipediaCatalan.pillais_conjecture.match_1.{1} (fun x => Prop) x fun x y m n =>
              And (LT.lt.{0} 1 x)
                (And (LT.lt.{0} 1 y)
                  (And (LT.lt.{0} 1 m)
                    (And (LT.lt.{0} 1 n)
                      (And (Ne.{1} (Prod.mk.{0, 0} m n) (Prod.mk.{0, 0} 2 2))
                        (Eq.{1}
                          (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} a (HPow.hPow.{0, 0, 0} x n))
                            (HMul.hMul.{0, 0, 0} b (HPow.hPow.{0, 0, 0} y m)))
                          c))))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record