Computational primality testing

Stream: Is there code for X?

[Simon Dima]

I'm quite certain this must exist somewhere, but I'm not sure how to search efficiently. I'm looking for a function essentially of type Nat -> Bool with the (proven) property that the result is true iff the argument is prime.
Ideally this would have better runtime than naïvely checking all numbers between 2 and n.
Is there code for my X?

[Kenny Lau]

I don't think we have good prime tests yet. You're welcome to write one!

[Yaël Dillies]

@Bhavik Mehta wrote one, actually

[Kenny Lau]

and where would one be able to find it?

[Yaël Dillies]

Let's wait for him to tell us :slight_smile:

[Kenny Lau]

on the other hand we already have Nat.prime_def_le_sqrt to reduce the complexity to O(sqrt(N))

[Aaron Liu]

While we wait I found this message on an old thread

Bhavik Mehta said:

As I mentioned earlier in the thread, I have a tactic which does this, which you can see on this example here: https://github.com/b-mehta/mathlib4/blob/large-prime/Mathlib/V2/Prime.lean#L622 The thing itself has the ability to call mathematica to generate and self-replace with a certificate, or sage (except that the sage server went down after I made it) or compute it natively (although this is too slow for this example), or you can just paste in a certificate from mathematica. That file also contains proofs for much larger primes

[Simon Dima]

Mathlib's decidablePrime and decidablePrime' seem to be respectively the "check until n" and "check until √n" algorithms

[Simon Dima]

If I'm understanding Bhavik's code right, it looks like it runs as meta code during tactic time, and I'm not sure how easy it would be to obtain a regular function from it.

[Kenny Lau]

@Simon Dima why do you need such a function?

[Simon Dima]

I'm working on comparing various methods of generating executable code from proof assistants, currently benchmarking a hand-rolled extraction to (basically) OCaml compared to Lean's compiler.
I'm looking for computational code which has some propositional content mixed in to prove it correct but which is later removed by the compilation/extraction process, in order to have benchmarks which actually correspond to the "write verified code in a proof assistant, get correct executables" workflow. The existing benchmarks of Lean as a programming language basically don't use propositional content. Verified primality testing came to mind as a function which is easy to specify and which, I hoped, might have a preexisting proven implementation with a nontrivial algorithm

[Simon Dima]

The goal being to compile a program which takes a number on standard input and outputs whether it was prime, using (a) the Lean compiler and (b) my janky setup which goes through OCaml, and measuring the runtime of both on some large numbers

[Simon Dima]

I don't have any particular reason to be interested specifically in primality testing, though, so if you know of any other functions (on simple types like Nat or Bool) that have interesting computational behavior and also are proven correct, that would certainly be an interesting benchmark to look at!

[Bhavik Mehta]

Simon Dima said:

If I'm understanding Bhavik's code right, it looks like it runs as meta code during tactic time, and I'm not sure how easy it would be to obtain a regular function from it.

This is correct, what I built was a tactic which verified a prime certificate generated elsewhere (failing if the elsewhere thinks it's not prime), rather than code which checks primality

[Bhavik Mehta]

On the other hand, there's #general > new monadic program verification framework @ 💬, which is still trial division, but does have this property. It's checking up to the square root though, so it's slightly better than the most naive algorithm. Scrolling in that thread, you can find my proof of correctness for it, and a shorter proof for the version which doesn't stop at the square root.

[Simon Dima]

Bhavik Mehta said:

This is correct, what I built was a tactic which verified a prime certificate generated elsewhere (failing if the elsewhere thinks it's not prime), rather than code which checks primality

This bit looks somewhat like a Lean function to generate such a certificate, or am I mistaken?

[Bhavik Mehta]

It is! "elsewhere" has three options: mathematica, sage, or Lean (so I suppose "elsewhere" was a bad term to use). I suppose one could verify correctness of this function

[Simon Dima]

I see, so given the current state one could compose together the certificate generation and verification to get a function which either outputs "n is certainly prime" (guaranteed to be correct) or an error where the certificate generator generated an invalid certificate

[Bhavik Mehta]

Right. The intention was to have a tactic which, given a prime, produces a proof of correctness for that specific prime, which is what's in the file you're looking at