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

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]