Discussion: Verified primality testing

Stream: general

[Bas Spitters]

Nice! How does it compare to Coq prime, which was likely one of the first applications of heavy computation in type theory?
https://github.com/thery/coqprime
I believe this is the related publication: https://www-sop.inria.fr/marelle/Laurent.Thery/pub3.pdf

[Notification Bot]

A message was moved here from #announce > Verified primality testing by Floris van Doorn.

[Siddhartha Gadgil]

Thanks @Bas Spitters for the reference.

So far this was a quick project without much testing or optimisation. For instance, pari is restarted for each command instead of keeping it running. Perhaps of greater consequence we have not yet made a Lean executable that generates the code instead of running in the interpreter. Will work on these things.

[Bhavik Mehta]

Siddhartha mentioned that his and mine diverged in various ways; mine is currently in preparation for PRing to mathlib, and has some performance and usability optimisations; meaning it works in under a second for all primes around 50 digits, and can work for specifically chosen primes around 400 digits, and can use mathematica or sage or Lean to compute the certificate.

[Bhavik Mehta]

However I expect it still won't be as performant (for large primes) as the one in that paper, since that uses a more mathematically sophisticated primality certificate