Worked solution: Mihăilescu's proof of Catalan's conjecture via cyclotomic fields (2002)

Frequently asked questions

Is this the only place in the whole proof that relies on a computer?

Essentially yes — as Bilu notes, this brief verification (and the related computation confirming $\min\{p,q\}>10^7$ ) is the only place electronic computation enters Mihăilescu's argument; every other step is a purely mathematical (if intricate) deduction, and Mihăilescu even found a way to make this particular step avoid computers too, in later work.

Source

Preda Mihăilescu, 2002

Primary cyclotomic units and a proof of Catalan's conjecture

Condensed summary

Step 5 of 7: A finite computation plus Tijdeman closes off

p\equiv1\pmod q

Previous step Next step

In plain words

One particular case turns out to be both dangerous and, fortunately, treatable: if $p$ happens to be congruent to $1$ modulo $q$ , several of the later algebraic arguments break down. Mihăilescu needed to rule this case out entirely before proceeding.

He did so by combining Tijdeman's logarithmic-forms technique from Step 3 with the Wieferich relation from Step 4 and a modest, genuinely finite computer verification (about one minute of computation, as Bilu reports), showing that $p\equiv1\pmod q$ together with a solution of Catalan's equation is simply impossible.

p \not\equiv 1\pmod{q}

Detailed analysis

Mihăilescu's proof needs, as a technical prerequisite used repeatedly later, the fact that $p\not\equiv1\pmod q$ for any solution of Catalan's equation (Bilu 2004, §4, Theorem 4.1). Assuming instead $p\equiv1\pmod q$ , Wieferich's relation from Step 4 upgrades this to $p\equiv1\pmod{q^2}$ ; since $p$ is odd, this rules out $p=q^2+1$ and $p=3q^2+1$ , and $p=2q^2+1$ is ruled out because it is then divisible by $3$ (an observation due to Mignotte), leaving $p>4q^2+1$ (Bilu 2004, §4.5).

On the other hand, an explicit refinement of Tijdeman's inequality (via the sharper Laurent–Mignotte–Nesterenko bounds on binary logarithmic forms) shows $p\le 4q^2$ whenever $q>28000$ (Bilu 2004, §4.5, Proposition 4.5.1) — directly contradicting $p>4q^2+1$ . This leaves only finitely many small $q\le 28000$ to check, which Mihăilescu did by a short computer verification (Bilu 2004, Remark 4.2, describing a PARI script running about one minute).

With $p\not\equiv1\pmod q$ (and symmetrically $q\not\equiv1\pmod p$ , by the same argument) now firmly established, the stage is set for the final, purely algebraic elimination of every remaining double Wieferich pair.