Zulip Chat Archive

Stream: maths

Topic: Formally verified factoring


view this post on Zulip 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 1010010^100 was, and get a formally proved answer?

view this post on Zulip Floris van Doorn (Aug 16 2019 at 21:13):

the next prime after 1010010^100

It shouldn't be too hard to prove that's 2.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 16 2019 at 22:22):

Use sage

view this post on Zulip Kevin Buzzard (Aug 16 2019 at 22:23):

That would be a really cool project @William Stein

view this post on Zulip 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