Yao Xu

A Lean 4 formalization of Catalan's conjecture

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 annih...