Mills Theorem

[franzhusch]

What is the conjecture

Mills' theorem asserts the existence of a real constant $A$ (called Mills' constant) such that $\lfloor A^{3^n} \rfloor$ is prime for all positive integers $n$, where $\lfloor \cdot \rfloor$ denotes the floor function. The theorem was proved by William Harold Mills in 1947. The sequence generated by Mills' constant is known as Mills' primes.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

• https://en.wikipedia.org/wiki/Mills%27_constant, https://mathworld.wolfram.com/MillsConstant.html, https://arxiv.org/abs/1010.4883, https://cs.uwaterloo.ca/journals/JIS/VOL8/Caldwell/caldwell78.pdf

Prerequisites needed

Formalizability Rating: 1/5 (0 is best) (as of 2026-01-21)

Mills' theorem requires formalizing the statement about the existence of a real constant with a prime-generating property. Mathlib provides extensive support for prime numbers, real numbers, and basic properties like the floor function. However, the formalization would need to define Mills' constant formally (or work with its existence property), establish the sequence of Mills primes, and connect these through the exponential function. Some auxiliary lemmas about prime checking and properties of double exponential sequences may be needed, but the core mathematical infrastructure exists in Mathlib.

AMS categories

• ams-11

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else

---

This issue was generated by an AI agent and reviewed by me.

See more information here: link

Feedback on mistakes/hallucinations: link