A Lean 4 formalization of Catalan's conjecture

Abstract

We present a complete Lean 4 formalization of Catalan's conjecture, proved by Mihăilescu: 8 and 9 are the only consecutive positive proper perfect powers. The formalization follows the cyclotomic proof in Bilu's expositions. We describe how Cassels' relations, Stickelberger annihilation, and height and counting estimates exclude the case in which one exponent is congruent to 1 modulo the other, and how the remaining case is settled by Thaine's theorem on circular units together with a Runge-type approximation argument. The class-field-theoretic input comes from a fixed subset of the ClassFieldTheory library, and we explain the bridges from its reciprocity theorems to the prime-selection statements that the proof needs: the selection theorem replaces the Chebotarev density theorem by a centralizer condition on the automorphism, and a localization lemma for group-ring powers of units is stated over an arbitrary number field. We also classify the solutions with nonzero integer bases of either sign and compare the final declarations with the consecutive-power and Formal Conjectures statements. The public results depend only on Lean's standard axioms, and a kernel replay in a fresh environment rechecks their dependency cone.