Master’s practical course, Master’s thesis, or IDP
There are many different tests to determine if a natural number is prime. Most of these are *probabilistic* and always recognise a prime number as prime, but, with some probability, also mistakenly classify composites as primes. Some of these tests (Fermat, Miller–Rabin, Solovay–Strassen) are already formalised in Isabelle.
In this project, more primality tests are to be formalised, e.g.:
- Frobenius test (randomised)
- Lucas and Fibonacci pseudoprimes (randomised)
- Lucas–Lehmer test for Mersenne primes (deterministic)
- AKS test (deterministic)
Additionally, one could prove a better bound for the error probability in the Miller–Rabin test (1/4 instead of 1/2).
Prerequisites:
Students need basic familiarity with Isabelle. Some knowledge of number theory and algebra (groups/rings) would be desirable.
Advisor:
Manuel Eberl, email {eberlm} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]