What is the conjecture
Define the sequence of Catalan-Mersenne numbers recursively by $c_0 = 2$ and $c_{n+1} = 2^{c_n} - 1$ for $n \geq 0$. Catalan conjectured that the first five terms of this sequence are all prime: $c_0 = 2, c_1 = 3, c_2 = 7, c_3 = 127, c_4 = 2^{127} - 1$. For $n \geq 5$, the primality of $c_n$ remains unknown. The numbers grow extremely rapidly: $c_5$ has more than $10^{38}$ digits and has no known prime factors below $10^{51}$.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-03-24)
Building blocks (1-3; from search results):
Nat.Prime and primality predicates in Mathlib- Natural number arithmetic and exponentiation
- Recursive function definitions
Missing pieces (exactly 2; unclear/absent from search results):
- A formal definition/type for the Catalan-Mersenne sequence (simple recursive definition, but needs to be set up)
- Notation or helper lemmas for the specific recursion $c_{n+1} = 2^{c_n} - 1$
Rating justification (1-2 sentences): The statement uses only standard Mathlib concepts (Nat, Prime, recursive definitions). Formalizing the conjecture statement itself requires only minor helper definitions to set up the recursive sequence, as primality testing and natural number exponentiation are already available in Mathlib.
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link
What is the conjecture
Define the sequence of Catalan-Mersenne numbers recursively by$c_0 = 2$ and $c_{n+1} = 2^{c_n} - 1$ for $n \geq 0$ . Catalan conjectured that the first five terms of this sequence are all prime: $c_0 = 2, c_1 = 3, c_2 = 7, c_3 = 127, c_4 = 2^{127} - 1$ . For $n \geq 5$ , the primality of $c_n$ remains unknown. The numbers grow extremely rapidly: $c_5$ has more than $10^{38}$ digits and has no known prime factors below $10^{51}$ .
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 1/5 (0 is best) (as of 2026-03-24)
Building blocks (1-3; from search results):
Nat.Primeand primality predicates in MathlibMissing pieces (exactly 2; unclear/absent from search results):
Rating justification (1-2 sentences): The statement uses only standard Mathlib concepts (Nat, Prime, recursive definitions). Formalizing the conjecture statement itself requires only minor helper definitions to set up the recursive sequence, as primality testing and natural number exponentiation are already available in Mathlib.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link