Mills' Theorem

There exists a real $A > 1$ such that $\lfloor A^{3^n}\rfloor$ is prime for every positive integer $n$, where $\lfloor\cdot\rfloor$ denotes the floor function.

The least such $A$ is known as Mills' constant. It is irrational, and assuming the Riemann hypothesis it is approximately $1.3063778838\ldots$.

References:

• Wikipedia, Mills' constant
• A prime-representing function by W. H. Mills, Bull. Amer. Math. Soc. 53 (1947), 604.
• Mills' constant on Wolfram MathWorld.
• Mills' constant is irrational by Kota Saito, Mathematika 71 (2025), no. 3, e70027, arXiv:2404.19461.
• Determining Mills' Constant .. by Chris K. Caldwell and Yuanyou Cheng, J. Integer Seq. 8 (2005), Article 05.4.1.
• OEIS A051021 (decimal expansion of Mills' constant)

@[reducible, inline]

abbrev Mills.IsMills (A : ℝ) : Prop

Given any real $A$, IsMills A encodes the statement that $\lfloor A^{3^n}\rfloor,n > 0$ is prime.

Equations

• Mills.IsMills A = ∀ (n : ℕ+), Prime ⌊A ^ 3 ^ ↑n⌋₊

theorem Mills.exists' : ∃ A > 1, IsMills A

Mills' theorem (Mills, 1947). There is a real number $A > 1$ such that $\lfloor A^{3^n}\rfloor$ is prime.

@[reducible, inline]

abbrev Mills.IsMinMills (A : ℝ) : Prop

For a real $A$, IsMinMills A is the smallest value satisfying IsMills A.

Equations

• Mills.IsMinMills A = IsLeast {x : ℝ | x > 1 ∧ Mills.IsMills x} A

theorem Mills.exists_least : ∃ (A : ℝ), IsMinMills A

Mills' constant. There is a least Mills number.

theorem Mills.irrational {A : ℝ} (hA : IsMinMills A) : Irrational A

Mills' constant is irrational (Saito, 2024).

theorem Mills.lower_bound_of_RH (hRH : RiemannHypothesis) {A : ℝ} (hA : IsMinMills A) : A ∈ Set.Ioo 1.3063778838 1.3063778839

Mills' constant lower bound (Caldwell–Cheng, 2005): assuming the Riemann hypothesis, Mills' constant begins at $1.3063778838\ldots$.