Formal target: Corpus.WikipediaAbc.abc
For every positive real number ε, there exist only finitely many triples (a, b, c) of coprime positive integers, with a + b = c, such that c > rad(abc)^(1+ε)
Exact formal statement
∀ (ε : Real),
LT.lt.{0} 0 ε →
Set.Finite.{0}
(Set.ofPred.{0} fun x =>
Corpus.WikipediaAbc.abc.match_1.{1} (fun x => Prop) x fun a b c =>
And (LT.lt.{0} 0 a)
(And (LT.lt.{0} 0 b)
(And (LT.lt.{0} 0 c)
(And
(Set.Pairwise.{0} (Insert.insert.{0, 0} a (Insert.insert.{0, 0} b (Singleton.singleton.{0, 0} c)))
Nat.Coprime)
(And (Eq.{1} (HAdd.hAdd.{0, 0, 0} a b) c)
(LT.lt.{0}
(HPow.hPow.{0, 0, 0}
(Nat.cast.{0} (Corpus.WikipediaAbc.radical (HMul.hMul.{0, 0, 0} (HMul.hMul.{0, 0, 0} a b) c)))
(HAdd.hAdd.{0, 0, 0} 1 ε))
(Nat.cast.{0} c)))))))This target is a formal statement, not a proof of the problem.
Environment availability: available.