Topic: Formally verified factoring
Kevin Buzzard (Aug 16 2019 at 21:12):
How does all this work? If I want to find a 100 digit prime number as part of some class demonstration on factoring I'd just ask pari-gp to give me a 100 digit prime and not care about formal verification because it's probably right. What would need to happen before I could ask Lean what the next prime after was, and get a formally proved answer?
Floris van Doorn (Aug 16 2019 at 21:13):
the next prime after
It shouldn't be too hard to prove that's
Floris van Doorn (Aug 16 2019 at 21:15):
I guess we would have to formally verify one of those polynomial-time prime checking algorithms.
Do you also want to know that all numbers between your number and the prime number are non-primes? Then we could certify those with a factorization, I guess.
Andrew Ashworth (Aug 16 2019 at 21:16):
You know what would be cool is if someone implemented the Miller-Rabin primality test in Lean, and proved it correct.
Andrew Ashworth (Aug 16 2019 at 21:18):
But wikipedia says people don't really use it for deterministic checking, so maybe something else would be appropriate...
Andrew Ashworth (Aug 16 2019 at 21:22):
hmm... wikipedia claims the state-of-the-art in prime number certificates is the Atkin–Goldwasser–Kilian–Morain certificate, which can hopefully be output by pari-gp or similar program
Kevin Buzzard (Aug 16 2019 at 22:22):
Kevin Buzzard (Aug 16 2019 at 22:23):
That would be a really cool project @William Stein
Chris Hughes (Aug 16 2019 at 22:35):
Will there ever be vaguely fast kernel computation in Lean?
Last updated: May 12 2021 at 08:14 UTC