# Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?

Remark 1. The following counting formula can be derived using arithmetic properties of inequalities, properties of floor / ceiling, inclusion-exclusion, sieve-of-Eratosthenes, and the inclusion-exclusion counting principle for OR-logic. To give an idea of what would be needed on the proof assistant side.

Definition 1. Define the twin prime (average) counting function to be, for any $$x \in \Bbb{R}$$:

$$F(x) := T(f)(x) = \sum_{d \mid N_x\#} \mu(d)\sum_{r^2 = 1 \mod d} f(d,r,x)$$

where $$N_x = \sqrt{|x| + 1}\#$$ (primorial), where $$T$$ is the transformation of functions $$f \in \{ \Bbb{N}^2 \times \Bbb{R} \to \Bbb{Z}\}$$ given by the present double summation; and finally where $$f$$ is specifically $$f(d,r,x) :=\left\lfloor\frac{x - r}{d} \right\rfloor - \delta_1(d)$$. Note all the $$-\delta_1(d)$$ does is simply add a $$-1$$ into the total summation. The need for it can be found in a derivation of such counting function.

It is known for $$x \geq 0$$ to count the number of twin prime averages occurring in the shifting, growing interval $$[p_n + 2, x]$$ with $$n = \pi (\sqrt{x + 1})$$. The reason it doesn't count the earlier averages is because they naturally get cancelled out by the inherent Sieve-of-Eratosthenes. You could state in terms of the interval $$[0, x]$$ but you'd say additionally "twin prime averages $$a$$ such that $$a \pm 1 \notin \{ p_1, \dots, p_n\}$$."

Definition 2. Given our function space transformation $$T: \{\Bbb{N}^2 \times \Bbb{R}\to \Bbb{Z}\} \to \{\Bbb{R} \to \Bbb{Z}\}$$, and since these function spaces are $$\Bbb{Z}$$-modules themselves, we define the limit kernel to be just what it sounds like:

$$\lim\ker T = \{ f \in \text{dom}(T) : \lim_{x \to \infty} T(f)(x) = 0 \}$$

That is the set of all domain functions which vanish in the limit after $$T$$ is applied, as $$x \to \infty$$.

Lemma 1. The limit kernel of $$T$$ is a $$\Bbb{Z}$$-submodule. Thus $$\lim \ker T$$ is closed under $$+,-$$ and scalar $$\cdot$$ .

Proof. This follows simply from $$T$$ being defined as a double summation, where of course this is the case. Though a more rigorous proof should be made since a limit is taken, which one usually does not see in basic linear algebra.

Lemma 2. For $$x \in \Bbb{R}$$ and $$x \lt 0$$ we have:

$$-(|f(|x|)| + 2) \leq f(x) \leq |f(|x|)|$$. In other words, we have almost that $$f(x) = - f(|x|)$$ except for an additive constant of $$2$$ on the lower bound side.

Code.

from sympy import *

def F(x):
S = -1
s = int(sqrt(abs(x) + 1))
if s in {0, 1}:
P = 1
else:
P = primorial(s, nth=False)

for d in divisors(P):
for r in range(0, d):
if (r ** 2 - 1) % d == 0:
S += (-1) ** primeomega(d) * floor((x - r)/d)

return S

X = 200

for x in range(0, X):
pos = F(x)
neg = F(-x)

print(x, pos, neg)

assert -abs(pos) -2 <= neg <= abs(pos)


Lemma 3. $$\sum_{i = 0}^{md - 1} \left\lfloor\frac{x - i}{d} \right\rfloor = mx - \frac{m(m + 1)}{2} d + m$$

Code.

from sympy import *

N = 10

for d in range(1, N):
for m in range(1, N):
for x in range(-d, d):
S = 0

for i in range(0, m*d):
S += floor((x-i)/d)

print(d, x, S)

assert S == m * x - (m * d) * (m + 1) // 2 + m


Lemma 4. The twin prime conjecture is false if and only if $$f \in K = \lim \ker T$$.

Proof. This is because if false, the counter function as $$x \to \infty$$ which is $$F(x) \geq 0$$ must vanish. And vice versa.

Lemma 5. We have already that:

$$G(d,r,x) =\sum_{i = 0}^{N_x -1} \left\lfloor\frac{x -i- r}{d} \right\rfloor - N_x\delta_1(d) - \sum_{i = 0}^{N_x} f(x - i)\delta_1(d)$$ sits in $$K = \lim\ker T$$. We simply compute $$f(x-i)$$ using our formula and then subtract $$f(x-i)$$ using the coefficient of $$\delta_1(d)$$. Then sum up everything.

Lemma 6. If the twin prime conjecture is false, there exists a natural number $$N_0$$ such that for all $$|x| \geq N_0$$ we have that $$f(x) = 0$$.

Corollary 1. This mean there exists a constant $$C \in \Bbb{Z}$$ and a constant $$M_0 \in \Bbb{N}$$ such that for all $$x \geq M_0$$ we have that:

$$g(d, r,x) = \sum_{i = 0}^{N_x - 1} \left\lfloor\frac{x-i-r}{d} \right\rfloor - N_x \delta_1(d) + C$$

Lemma 7. $$\lim T$$ basically eats constant functions, or in other words $$\lim_{x \to \infty}T( C)(x) = 0$$ for any constant $$C \in \Bbb{Z}$$.

Proof. Can be proved by elementary means, expanding $$T( C)(x)$$.

Corollary 8. If the twin prime conjecture is false, then:

$$\lim_{x \to \infty}T(g)(x) = \lim_{x \to \infty}\left(-(N_x + 1) + \sum_{d \mid N_x}\mu(d)\sum_{r^2 = 1 \mod d} \left\lfloor\frac{x - i - r}{d} \right\rfloor\right)$$

Lemma 8. If the twin prime conjecture is false, then by Lemma 3:

$$\lim_{x \to \infty} T(g)(x) = \\ \ \\ \lim_{x \to \infty}\sum_{d \mid N_x}\mu(d)\sum_{r^2 = 1 \mod d}\left(-(N_x + 1) +\sum_{d \mid N_x}\mu(d)\sum_{r^2 = 1 \mod d}\left(\frac{N_x}{d}x - \frac{N_x(\frac{N_x}{d}+1)}{2} +\frac{N_x}{d}\right)\right) \\ \tag{1}$$
Corollary 8. By rearranging the formula at tag (1), we have:

$$\lim_{x \to \infty} T(g)(x) = \\ -1 +\lim_{x \to \infty} N_x\left( \sum_{d \mid N_x}\mu(d)\sum_{r^2 = 1 \mod d}\left(1 + \frac{x}{d} -\frac{N_x}{2d} -\frac{1}{2}+ \frac{1}{d}\right)\right) \\ \ = -3 + \lim_{x \to \infty} N_x\left( x - \frac{N_x}{2} +1\right) \sum_{d \mid N_x}\mu(d)\sum_{r^2 = 1 \pmod d}\frac{1}{d} \\ \tag{2}$$
Lemma 9. The double sum formula at tag (2) can be elegantly handled via Merten's third theorem.

But thinking much simpler: as $$x \to \infty$$ we obviously would have $$T(g)(x) \to -\infty$$, but this is impossible since by Lemma 5 we showed that necessarily we have that $$\lim_{x\to \infty} T(g)(x) = 0$$, since the summation defining $$G$$ must sit in the limit kernel of $$T$$ when we suppose a finite number of twin primes.

Obviously it is too big of a question to ask the community to proof-check this sketch. So I have a really good question instead.

Question.

Is the above theory encodable in Coq or not yet?

I mention Coq because I just installed it, I'm learning about it in order to understand presenters at ANR coREACT seminars, and its awesome to me that it has a standalone IDE. I'm open though to both Lean4 and Isabelle. Preferring Coq right now though.

• I am new to Coq. Not seeing any main references saying "click here to learn number theory in Coq". Commented Jul 28 at 10:56
• I’m not clear if you are open to Lean or Isabelle, but I think they both have a bunch of the stuff you need (but probably not all). You could use Moogle.ai to check what is already in Lean’s mathlib and SERaPIS for Isabelle’s AFP. Also, with any theorem prover you could add background lemmas so the main challenge is just if one can state all the theorem statements and statements of the main lemmas. Commented Jul 28 at 11:15
• @JasonRute thanks for your response. Lean4 or CoqIDE and why? Is Lean4 having more Unicode support? Commented Jul 28 at 11:20
• I don’t understand the question “Lean4 or CoqIDE and why?” Commented Jul 28 at 15:07
• You shouldn't be picking a proof assistant based on how much UTF8 support it has. (They all do, by the way.) Commented Jul 29 at 8:08

First, any modern proof assistant should be able to encode these lemmas, but it will be easier if the relevant definitions and background theory are already in the proof assistant.

I'm not an expert on this area of math and what is already in the main libraries, but generally you are going to be looking for a proof assistant and a math library that has both good coverage of algebra and analysis, and such that the two areas of math play well together in the proof assistant.

The three main libraries you should look into are Coq's mathcomp, Lean's MathLib, and Isabelle/HOL's AFP. They are all libraries containing algebra and analysis. Coq also has a number of other libraries, like Coquelicot for real numbers, but you need to check if it works with the algebra in mathcomp. I don't know for sure.

What I'm going to say now, is more speculative and should be taken with a grain of salt. I think Lean's Mathlib would have all the definitions you need, and there is a great deal of concern with making sure analysis, algebra, and category theory play well together, so I think you would find that at least stating the results would go smoothly. (As for how to state the kernel limit of modules, it would probably help to ask on the Lean Zulip, but I think it is in Mathlib or something very close.) But I also doubt things like Merten's third theorem would be in Mathlib, so you would likely have to prove it yourself (but then PR it to Mathlib so others could use it). You can search for theorems using moogle.ai.

As for the Isabelle/HOL AFP, I think I've heard it has really good coverage of analysis, so it is most likely of the three to have Merten's third theorem, for example. Algebra is (maybe?) trickier in Isabelle/HOL because it doesn't have dependent types, but that isn't a large deal and there are ways to make it ergonomic. I know others have developed a lot of algebra in Isabelle/HOL's AFP. You can search for theorems with SERaPIS.

As for Coq, I know the least about MathComp, so you would have to do your own investigation to see if it has modules and the kernel limit, etc. But they have built a big algebraic hierarchy, so it might have the algebra you need.

(To the extent that what you are doing is similar to proofs of the prime number theorem, note there is a proof of the Prime number theorem in Isabelle, and there is a current project to do a few proofs of the Prime Number Theorem in Lean.)

Now, you also ask about usability. Like any programming language, that is a contentious topic. Here are some other posts on that matter:

But one comment: You conflate CoqIDE and Lean 4. Lean 4 is a proof assistant language. The usual editor for it is the Lean 4 VS Code plugin (but there is also an Emacs plugin). Coq is a proof assistant language as well, and CoqIDE is just one of many editors. (I am not sure it is the one I'd recommend, but it is probably a matter of taste.) There are other Coq editors in Emacs and VS Code for example.

• Lean4 I’ll go with for now. See you on Zulip! Thanks for the detailed and expert response. Commented Jul 29 at 19:12