## Stream: maths

### 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 $10^100$ was, and get a formally proved answer?

#### Floris van Doorn (Aug 16 2019 at 21:13):

the next prime after $10^100$

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

#### 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

Use sage

#### 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