Open Research Index

A Lean 4 formalization of Catalan's conjecture (Mihăilescu's theorem)

Yao Xu

Palomar Registrypalomar/PALOMAR-2026-10-06-000009Oct 6, 2026math.NTscore 0

A complete Lean 4 formalization of Catalan's conjecture, proved by Preda Mihăilescu: 8 and 9 are the only consecutive positive proper perfect powers. The formal proof follows the cyclotomic proof in Yuri Bilu's expositions. Cassels' relations, Stickelberger annihilation, and height and counting estimates exclude the case in which one exponent is congruent to 1 modulo the other. Thaine's theorem on circular units, together with a Runge-type approximation argument, settles the remaining case. The class-field-theoretic input comes from a fixed, vendored subset of the ClassFieldTheory library.…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-06-000009
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000009/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000009/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'