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.)
 A: 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.
