Formally verified factoring

Stream: maths

[Kevin Buzzard]

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]

the next prime after $10^100$

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

[Floris van Doorn]

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]

You know what would be cool is if someone implemented the Miller-Rabin primality test in Lean, and proved it correct.

[Andrew Ashworth]

But wikipedia says people don't really use it for deterministic checking, so maybe something else would be appropriate...

[Andrew Ashworth]

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]

Use sage

[Kevin Buzzard]

That would be a really cool project @William Stein

[Chris Hughes]

Will there ever be vaguely fast kernel computation in Lean?