# Proving that e.g. 421 is prime in a formal system

I'm working in the formal system Metamath, and in the course of learning about number theory I've become acquainted with theorems, such as Bertrand's postulate, that require hand-calculation that a given set of numbers up to 4000 is prime. What would be the most efficient method for doing such a proof? Working with specific numbers is quite difficult in a formal system, since proving that the number $n=((\dots(1+1)\dots+1)+1)$ is even a natural number requires $O(n)$ steps. Numbers up to 10 are defined this way in Metamath, and this style is convenient for its uniformity, which allows you to write a single inference schema $k\in\Bbb N\to k+1\in\Bbb N$ and apply it $n$ times to prove $n\in\Bbb N$.

For large numbers, it becomes convenient to represent them in other forms, say $2^k+m$ where $k$ and $m$ are specified as above. Thus you could prove that such a large number is a natural number in only $O(k+m)$ steps, and more generally you could use a form of decimal notation, i.e. $a+10\cdot(b+10\cdot(c+10\cdot d)))$ to achieve $O(\log n)$ steps in the long run.

This is how you would tackle the problem of proving closure for large numbers, but what is the most efficient way to prove primality? For the range I'm talking about (still "small" numbers as far as number theorists are concerned), the most efficient method is probably the sieve of Erastothenes, which builds up a complete list of all primes less than some number (so there is no avoiding at least $n$ assertions of the form $k\in\Bbb P$ or $k\notin\Bbb P$), and building the $n$-th assertion requires using at least the first $\sqrt n$ assertions, so we're looking at $O(n^{3/2})$ total steps in a proof that $n\in\Bbb P$.

Is there any better approach here? The strength of the system is in proving general assertions once and reusing them to achieve better compression of this process, the same way a human would, so it's not necessarily as brain-dead as a computer verification, but since prime numbers are so erratic, I don't see how you could achieve much savings off the brute-force approach. In particular, I'd like to avoid too many assertions that certain numbers are composite, but it is usually not clear that certain number is composite unless it is a multiple of the base (assuming you are using the decimal notation described above). There is nothing stopping you from using whatever notational system is convenient for the given number, but then converting between systems is overhead. Any ideas?

Note: I'm not asking for an actual proof here that some big number is prime, but rather an efficient approach to the problem, since the numbers involved are big enough that the big-O is going to dominate the overall length of the complete proof. The specifics of the Metamath system are also irrelevant, for the most part; what matters is that you can't just draw lines on a grid and take that as the proof, like one would do in a "regular" proof that a given number around 100 is prime. (Actually most people just brush this issue under the rug, which is why I'm asking this question for advice on how to tackle the problem.)

-
Does this problem become more tractable by applying Wilson's Theorem? It seems like the factorial could be an $O(n\log n)$ operation... – abiessu Feb 3 '14 at 18:13
@abiessu If I understand you correctly, are you suggesting that I calculate $x_0=1$; $x_k=k x_{k-1}\bmod n$ explicitly until I get to $x_{n-1}=n-1$ (assuming that I know in advance that $n$ is prime and I'm proving it)? Or perhaps I could manually select the correct multiplicative inverses to simplify the calculation... In the end it boils down to checking that the numbers $1$ thru $n-1$ have multiplicative inverses, i.e. do not divide $n$, at which point I am no better off than the definition. – Mario Carneiro Feb 3 '14 at 23:01
Now that I come to think about it, I am looking for a computationally efficient primality test, where we know in advance all relevant facts and just need to state them. This is somewhat different from the standard quality measure for primality tests, where we don't know in advance which divisors to pick and so on. It's like we have an oracle for number theory, except that you still need to compute a fact even if you know it. Not sure how to translate that into computational complexity terms. – Mario Carneiro Feb 3 '14 at 23:10
Aha! en.wikipedia.org/wiki/Primality_certificate I think this is the concept I am looking for. Anyone want to suggest an implementation? – Mario Carneiro Feb 3 '14 at 23:15
Just for clarification -- are you interested in proving primality of all the numbers from the set, or a particular one? The "cost" of proving multiple numbers at the same time can be considerably lower thanks to the re-use of already proved ones (e.g. the $O(n^{3/2})$ complexity you mentioned covers all the primes in the range; so the per-number cost is "just" $O(\sqrt{n})$, which looks much better) – Peter Košinár Feb 4 '14 at 23:18

As you pointed out in the comments, a primality certificate is essentially what you're looking for: it's a compression of the proof that a particular number is prime. The Pratt certificate for $N$, for instance, relies on a witness $a < N$, the prime factorization $q_1^{a_1}q_2^{a_2}\ldots q_k^{a_k}=N-1$, and the following facts:

• $a$ is coprime to $N$
• $q_i$ is prime for each $i$
• $a^{N-1}=1$ (mod $N$)
• $a^{(N-1)/q_i}\neq 1$ (mod $N$) for each $i$.

Once you had proved the general result that these facts guarantee the primality of $N$, you would need to prove the specific results involved in the certificate. For $421$, for instance, $23$ is a witness: $420=2^2\cdot 3 \cdot 5 \cdot 7$, all of $\{2,3,5,7\}$ are prime, $23$ is coprime to $421$, $23^{420}=1$ (mod $421$), and $23^{420/q}\neq 1$ (mod $421$) for $q \in \{2,3,5,7\}$. In practice, $N-1$ may have large prime factors that need witnesses as well, so there's some recursion; a set of small primes proved using brute force are useful to bottom out the recursion early.

-
Thanks for the answer. I think I've got the general idea, although the project itself is still going to take a lot of preparation. The hardest part is probably the calculation of $a$ and its powers mod large primes, using addition chain exponentiation. As for primes with large factors in $n-1$, it's not as big a concern as I thought it was going to be at first. (con't) – Mario Carneiro Feb 7 '14 at 0:44
... For Bertrand's postulate, my plan is to use the sequence $$2, 3, 5, 7, 13, 17, 19, 37, 73, 137, 271, 541, 1009, 2017, 4001$$ (the main proof covers the case $n>4000$), for which each number has only small factors except $137=2^3\cdot17+1$, and all of which are covered earlier in the sequence. Since I've got a bounty out, I didn't think it would be appropriate to answer my own question, but if I ever get the proof done, I'll post it here. – Mario Carneiro Feb 7 '14 at 0:49
By the way, you don't need your first bullet point, because the third implies it. (If $a^{N-1}=1\pmod N$ then $a^{N-1}$ is coprime to $N$, so $a$ is coprime to $N$.) Also, $2$ is also a witness for $421$, and I'm guessing that smaller witnesses will be easier to work with. – Mario Carneiro Feb 7 '14 at 1:20