Miller–Rabin Primality Test

Stream: general

[Thomas Zhu]

Hi all, I implemented the Miller–Rabin primality test, and proved that the Miller–Rabin primality test on composite n is correct to 3/4 of the bases. Here is my code: https://github.com/hanwenzhu/primality-tests

Main results:

/-- Fast modular exponentiation, tail recursive -/
def pow {n : ℕ} (x : ZMod n) (m : ℕ) : ZMod n

/-- `n` is a *Fermat probable prime* to base `a` if `a ^ (n - 1) = 1`. -/
def FPP (n : ℕ) (a : ZMod n) : Prop :=
  a ^ (n - 1) = 1

def FPP.Carmichael (n : ℕ) : Prop :=
  ∀ a : (ZMod n)ˣ, FPP n a

/-- `n` is a *strong probable prime* to base `a`, if `a ^ d = 1` or `a ^ (2^s * d) = -1`, where
`d` is odd, `s < s'`, and `s'` is such that `n - 1 = 2^s' * d`. -/
def SPP (n : ℕ) (a : ZMod n) : Prop :=
  a ^ oddPart (n - 1) = 1 ∨
  ∃ s : ℕ, s < val₂ (n - 1) ∧ a ^ (2 ^ s * oddPart (n - 1)) = -1

/-- A prime is a strong probable prime to any nonzero base. -/
theorem SPP.of_prime {p : ℕ} [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) :
  SPP p a

/-- The proportion of Miller–Rabin nonwitnesses of composite `n` is at most 1/4. -/
theorem SPP.card_SPP_of_not_prime {n : ℕ} [Fact (n ≥ 2)] (ho : Odd n) (hnp : ¬n.Prime) :
  Fintype.card {a // SPP n a} * 4 ≤ n - 1

/-- The *Miller–Rabin* primality test on input `n`, run `r` times. -/
def millerRabin {gen : Type*} [RandomGen gen] (g : gen) (n r : ℕ) : Bool × gen

def runMillerRabin (n r : ℕ) : IO Bool

Also IMO there are one or two results in PrimalityTests/Lemmas.lean that should be in mathlib.

I really hope to extend this:

1. Show millerRabin g n r is correct to a probability arbitrarily close to 1 exponentially in r, assuming the random number generator g is random enough. This is already immediate conceptually from existing results, though is very tricky to formulate (integrating measure-theoretic probability with RandomGen, potentially; I don't have a clear idea). This will be helpful to eventually implementing some cryptography algorithms in Lean efficiently and proving their soundness
2. Verifying primality certificates so we can use large primes in math proofs (like docs#lucas_primality)
3. Implement other probabilistic primality tests (like Baillie–PSW)

Suggestions/PRs are very welcome! I hope some would find this work useful.

There was a previous attempt to implement Miller–Rabin, but the proof is very incomplete AFAIK. There was also a discussion on formalizing the correctness of probabilistic algorithms, though that was even before Random

[Kevin Buzzard]

Completely stupid question: can this code be compiled and run, so you can test if a number like 561 is prime or not?

[Henrik Böving]

Yes you can compile the code: https://github.com/hanwenzhu/primality-tests/blob/main/PrimalityTests/MillerRabin.lean#L9

But keep in mind its only a probability based test so it's not like we could integrate this as a decision procedure that ships with a proof that something is a prime. @Kevin Buzzard

[Kevin Buzzard]

And what happens if you try with a ten digit number? Is it instant or does it take forever?

[Henrik Böving]

But it's still a pretty good test, in computer science we use it to get primes for asymmetric encryptions on numbers between 2k and 4k bits so numbers that look like this: 13182040934309431001038897942365913631840191610932727690928034502417569281128344551079752123172122033140940756480716823038446817694240581281731062452512184038544674444386888956328970642771993930036586552924249514488832183389415832375620009284922608946111038578754077913265440918583125586050431647284603636490823850007826811672468900210689104488089485347192152708820119765006125944858397761874669301278745233504796586994514054435217053803732703240283400815926169348364799472716094576894007243168662568886603065832486830606125017643356469732407252874567217733694824236675323341755681839221954693820456072020253884371226826844858636194212875139566587445390068014747975813971748114770439248826688667129237954128555841874460665729630492658600179338272579110020881228767361200603478973120168893997574353727653998969223092798255701666067972698906236921628764772837915526086464389161570534616956703744840502975279094087587298968423516531626090898389351449020056851221079048966718878943309232071978575639877208621237040940126912767610658141079378758043403611425454744180577150855204937163460902512732551260539639221457005977247266676344018155647509515396711351487546062479444592779055555421362722504575706910949376.

[Henrik Böving]

Kevin Buzzard said:

And what happens if you try with a ten digit number? Is it instant or does it take forever?

I guess that answers the question :P although I am not sure how good the implementation above is but it is very much a practical thing that your computer can do with a good implementation

[Eric Rodriguez]

It can deterministically say a number is composite however.

[Alex Kontorovich]

Nice! Long ago, I asked an undergrad REU student to prove that the Miller-Rabin witnesses become equidistributed for large composite $n$ (an observation which I couldn't find in the literature, though I doubted it was original to me?). Could be a fun project to formalize? https://arxiv.org/pdf/1608.07317.pdf

[Kevin Buzzard]

Henrik Böving said:

Kevin Buzzard said:

And what happens if you try with a ten digit number? Is it instant or does it take forever?

I guess that answers the question :P although I am not sure how good the implementation above is but it is very much a practical thing that your computer can do with a good implementation

Yes I'm well aware of that! What I am asking is whether @Thomas Zhu 's implementation can deal with numbers this large (although I started smaller than you :-) )

[Thomas Zhu]

Kevin Buzzard said:

And what happens if you try with a ten digit number? Is it instant or does it take forever?

To answer your question: it tests this number in under a second on my computer
image.png

[Thomas Zhu]

Eric Rodriguez said:

It can deterministically say a number is composite however.

Yes, essentially one would obtain a compositeness proof from the contrapositive of SPP.of_prime, and for most large composite numbers checking to one or a few bases already suffices

[Thomas Zhu]

Alex Kontorovich said:

Nice! Long ago, I asked an undergrad REU student to prove that the Miller-Rabin witnesses become equidistributed for large composite $n$ (an observation which I couldn't find in the literature, though I doubted it was original to me?). Could be a fun project to formalize? https://arxiv.org/pdf/1608.07317.pdf

This could be a good project to formalize indeed!

[Henrik Böving]

Thomas Zhu said:

Kevin Buzzard said:

And what happens if you try with a ten digit number? Is it instant or does it take forever?

To answer your question: it tests this number in under a second on my computer
image.png

Just out of curiosity: Could you maybe take a prime from some RSA private key and try to factorize that at the same certainty as the C code that generates them (idk how many rounds they do?) does?

[Jireh Loreaux]

Wait, C code doesn't only generates primes to a provided certainty. It eventually uses a deterministic check to verify they are prime. Or do you mean, the level of certainty from Miller-Rabin prior to doing a deterministic check?

[Henrik Böving]

Yeah in general to the degree that C code does use miller rabin, to see if its somewhat competetive in terms of speed

[Mauricio Collares]

Last I checked, RSA key generation in OpenSSH doesn't check primality using a deterministic test, just Miller-Rabin.

[Henrik Böving]

Well then someone should probably also figure that out lol.

[Frédéric Dupuis]

Yeah, only using Miller-Rabin is pretty standard I think. Keep in mind that RSA is much older than the first deterministic poly-time algorithm for primality testing!

[Jireh Loreaux]

Well, PRIMES is in P is only from 2004, but there was a deterministic algorithm which runs in $(\log n)^{O(\log \log \log n)}$ from 1983, so well before open ssh, and (I think) is suitable for use for modern key sizes.

[Eric Rodriguez]

I thought AKS was super slow in practice?

[Kevin Buzzard]

I think they got it down to $O((\log n)^6)$?

[Thomas Zhu]

Henrik Böving said:

Thomas Zhu said:

Kevin Buzzard said:

And what happens if you try with a ten digit number? Is it instant or does it take forever?

To answer your question: it tests this number in under a second on my computer
image.png

Just out of curiosity: Could you maybe take a prime from some RSA private key and try to factorize that at the same certainty as the C code that generates them (idk how many rounds they do?) does?

It would be interesting to compare the speed, though I suspect Lean would be slower in CPU time — I can try to do that at some time

[Yuyang Zhao]

There are some deterministic primality test that are faster than AKS in practice, but they are much more complex than Miller-Rabin.

[Matthew Ballard]

When I implemented Miller Rabin (on leanprover/lean4:nightly-2023-06-10 :fear: ) I brute force iterated for witnesses for a 13 digit number to get make speed comparisons more pronounced. I was pleased to see that the binary performed as well as the Go version I made while teaching cryptography last year.

As a plus for backward compatibility, elan just pulled that toolchain fine and then still just worked.

[Jireh Loreaux]

@Eric Rodriguez Yes, I think AKS is still too slow to be useful. I'm just saying that I think we've had stuff that's fast enough for a while. (But maybe I'm wrong; I'm no cryptographer!)

[Matthew Ballard]

Speaking of benchmarking, I would love to see Lean here

[Jireh Loreaux]

By the way, I think #8885 should make the fast modular exponentiation above unnecessary. (Or rather, it already implements it)

[Thomas Zhu]

AKS is not used in practice at all AFAIK, it is much slower than BPSW for less than 2^64 in which BPSW was shown to be correct, and for larger than that AKS is already getting prohibitive. Other methods like ECPP is not shown to by poly-time, but in practice much faster. I think if you need a large prime in a math proof, you can also just use an external ECPP to generate a primality certificate, and then verify that in Lean, similar to docs#lucas_primality

[Thomas Zhu]

Jireh Loreaux said:

By the way, I think #8885 should make the fast modular exponentiation above unnecessary. (Or rather, it already implements it)

Thanks! I was not aware of that. Indeed it implements the modular exponentiation above

[Thomas Zhu]

In practice you can easily run Miller–Rabin say 100 times, so you at least have a 4^-100 confidence, which is already much lower than probability of a hardware failure. This is certainly good enough for cryptography, but it doesn't produce a proof of n.Prime

[Bolton Bailey]

Thomas Zhu said:

In practice you can easily run Miller–Rabin say 100 times, so you at least have a 4^-100 confidence, which is already much lower than probability of a hardware failure. This is certainly good enough for cryptography, but it doesn't produce a proof of n.Prime

This is a problem that has been pretty frustrating to me in the past. I think it would be cool if we could avoid it by introducing a new axiom to derandomize specific tests like this.

[Bolton Bailey]

Some discussion on this happened around here

[Yuyang Zhao]

Jireh Loreaux said:

By the way, I think #8885 should make the fast modular exponentiation above unnecessary. (Or rather, it already implements it)

I was going to make something similar after std4#314.

[Thomas Zhu]

Bolton Bailey said:

Thomas Zhu said:

In practice you can easily run Miller–Rabin say 100 times, so you at least have a 4^-100 confidence, which is already much lower than probability of a hardware failure. This is certainly good enough for cryptography, but it doesn't produce a proof of n.Prime

This is a problem that has been pretty frustrating to me in the past. I think it would be cool if we could avoid it by introducing a new axiom to derandomize specific tests like this.

It would be very cool to do so, but I'm not sure how to set up this axiom. Maybe it has to state that StdGen (or some more random generator) is random enough, but then one might be able to craft counterexamples by engineering on the seed or something, and then derive falsehood. Another way is to argue that some pseudorandom generators are indistinguishable from true uniform in poly-time, then prove MR is somehow correct against poly-time attacks, but I don't know enough about cryptography to comment on how to do that, and it would be more for cryptography than for use in math

[Thomas Zhu]

Yuyang Zhao said:

Jireh Loreaux said:

By the way, I think #8885 should make the fast modular exponentiation above unnecessary. (Or rather, it already implements it)

I was going to make something similar after std4#314.

Cool! Given the number of divisions by 2 and parity tests in modular exponentiation and Miller–Rabin, I think divisions and parity tests based on bit manipulations would be faster

[Yuyang Zhao]

Currently Nat.binaryRec in my PR is implemented via · >>> 1 and 1 &&& ·. If Lean has a efficient Nat.testBit I think it could be faster. (I didn't check if GMP bignum supports it.)

[Bolton Bailey]

Thomas Zhu said:

Bolton Bailey said:

Thomas Zhu said:

In practice you can easily run Miller–Rabin say 100 times, so you at least have a 4^-100 confidence, which is already much lower than probability of a hardware failure. This is certainly good enough for cryptography, but it doesn't produce a proof of n.Prime

This is a problem that has been pretty frustrating to me in the past. I think it would be cool if we could avoid it by introducing a new axiom to derandomize specific tests like this.

It would be very cool to do so, but I'm not sure how to set up this axiom. Maybe it has to state that StdGen (or some more random generator) is random enough, but then one might be able to craft counterexamples by engineering on the seed or something, and then derive falsehood. Another way is to argue that some pseudorandom generators are indistinguishable from true uniform in poly-time, then prove MR is somehow correct against poly-time attacks, but I don't know enough about cryptography to comment on how to do that, and it would be more for cryptography than for use in math

Cryptography is indeed exactly what I am thinking of using here, and it's in cryptography where I have mainly seen the need for formally certified primes. There are also some applications in math, but they seem to be more rare.

[Thomas Zhu]

@Bolton Bailey I think this is quite an interesting. Do you have in mind an exact formulation of the axiom? And how would you state "n is probably a prime" in lean?

[Bolton Bailey]

Here is a relatively simple version of something adapted from a draft I have been working on, H is meant to be a cryptographic pseudorandomness generator

axiom probabilistic_miller_rabin
  (p : Nat)
  (hn : forall i in Finset.range 256, not_miller_rabin_compositeness_witness p ((H p i) % p) :
  p.Prime

[Bolton Bailey]

There are a variety of small issues with this approach, some of which can be fixed, and some not. For example, maybe H will have some structure that lets you prove this axiom is false, potentially without even explicitly determining what value of p it's false for.

[Bolton Bailey]

But if you come up with a bit of a more rigorous version, like

axiom probabilistic_miller_rabin
  (p : Nat)
  (hp : p < 2^2048)
  (hn : forall i in Finset.range 2048, not_miller_rabin_compositeness_witness p ((SHA3 (outputbits:= 2048) p i) % p) :
  p.Prime

You can get something which seems very plausibly true, and also lets you resolve primality goals.

[Kevin Buzzard]

The first axiom is surely definitely false, you'll surely be able to use the Chinese remainder theorem and quadratic reciprocity to find some absolutely gigantic counterexample whatever your choice of H (if something like this were true then it would be an extremely efficient test for primality). The second might be true but it might be the case that to check it you'll just have to do the brute force calculation which is of course completely unfeasable, you may as well just list all the primes less than 2^2048 and then do a look up :-)

[Bolton Bailey]

Kevin Buzzard said:

The first axiom is surely definitely false, you'll surely be able to use the Chinese remainder theorem and quadratic reciprocity to find some absolutely gigantic counterexample whatever your choice of H (if something like this were true then it would be an extremely efficient test for primality). The second might be true but it might be the case that to check it you'll just have to do the brute force calculation which is of course completely unfeasable, you may as well just list all the primes less than 2^2048 and then do a look up :-)

Wait, are you saying you could prove the first one is false for SHA3? I can definitely think of at least one example of a (of course relatively inefficient) H for which it's not false, namely, an H that deterministically checks if p is prime, and then finds only examples of witnesses that confirm that fact.

[Eric Rodriguez]

I was thinking the axiom wasn't going to be so specific but instead something like "if P(event) < 10^-100 then ¬event"

[Bolton Bailey]

I agree that it is almost definitely false for SHA3, but I'm not sure it could be proved. For a non-cryptographic PRNG, maybe there could be a number-theoretic proof it's false.

[Thomas Zhu]

Hmm, I was thinking more like proving that if H is a (random enough) pseudorandom number generator, then there is no efficient (maybe poly-time) algorithm to produce counterexamples to Miller–Rabin

[Thomas Zhu]

For large prime p, I don't actually think you need axioms to show p.Prime, since you can get away with good deterministic primality tests that generate certificates that can be checked in Lean. But this might have applications for other probabilistic tests

[Kevin Buzzard]

@Bolton Bailey your first axiom has no bounds on p. I don't know what SHA3 is but I know that there are infinitely many composite numbers.

[Bolton Bailey]

Thomas Zhu said:

For large prime p, I don't actually think you need axioms to show p.Prime, since you can get away with good deterministic primality tests that generate certificates that can be checked in Lean. But this might have applications for other probabilistic tests

What deterministic primality certificate generator are you think of and what is it's time complexity? When I was reviewing this the best I could find were elliptic curve-based tests that were slower than Miller-Rabin.

[Thomas Zhu]

Bolton Bailey said:

Thomas Zhu said:

For large prime p, I don't actually think you need axioms to show p.Prime, since you can get away with good deterministic primality tests that generate certificates that can be checked in Lean. But this might have applications for other probabilistic tests

What deterministic primality certificate generator are you think of and what is it's time complexity? When I was reviewing this the best I could find were elliptic curve-based tests that were slower than Miller-Rabin.

I think elliptic curve-based tests are good enough. It's not proven to be polynomial but in practice acts polynomially. I'm not sure how large are the primes people want to prove Nat.Prime holds (maybe in number theory) but it's probably something ECPP can still handle?

[Bolton Bailey]

Kevin Buzzard said:

Bolton Bailey your first axiom has no bounds on p. I don't know what SHA3 is but I know that there are infinitely many composite numbers.

I am not sure what quadratic reciprocity can do to help us analyze SHA3 here.

[Bolton Bailey]

Thomas Zhu said:

Bolton Bailey said:

Thomas Zhu said:

For large prime p, I don't actually think you need axioms to show p.Prime, since you can get away with good deterministic primality tests that generate certificates that can be checked in Lean. But this might have applications for other probabilistic tests

What deterministic primality certificate generator are you think of and what is it's time complexity? When I was reviewing this the best I could find were elliptic curve-based tests that were slower than Miller-Rabin.

I think elliptic curve-based tests are good enough. It's not proven to be polynomial but in practice acts polynomially. I'm not sure how large are the primes people want to prove Nat.Prime holds (maybe in number theory) but it's probably something ECPP can still handle?

I take your point. I guess what I am riding on here is that as long as there is some gap in complexity between the deterministic and randomized tests, then there is some size of prime and some amount of compute for which you can carry out the proof with Miller-Rabin, but not any deterministic method.

[Thomas Zhu]

Yes, there are definitely primes too large for deterministic tests but ok for MR, but I'm not sure when that's needed: if you're doing cryptography, you are most likely using MR anyway (and using many probabilistic things elsewhere), and if you're proving something in number theory that needs a huge prime, it's still usually manageable with ECPP

[Thomas Zhu]

I might be wrong though - do people actually need very large primes that can only be shown probabilistically outside of cryptography?

[Bolton Bailey]

I guess the only thing I know about is this Helfgott proof of the odd Goldbach conjecture, where he had to prove numbers on the order of 10^27 were prime, but didn't need to prove specific number prime, so he could use certificates that were much more efficient.

[Bolton Bailey]

I am also curious about potential number theory applications - when/do number theorists have to prove specific large numbers are prime, and how large are they?

[Bolton Bailey]

Incidentally, Kevin's comment has gotten me curious: Is it true/known that the sum over composite n from n = 1 to infinity of the fraction of k < n that are non Miller-Rabin witnesses diverges? Or if that sequence when raised to the power of 256/ some other value diverges?

[Bolton Bailey]

If not, I am suddenly not even sure that the first version of the axiom even is false.

[Thomas Zhu]

There is probably an answer to this specific question, since the fraction of MR witnesses is well studied I would imagine

[Bolton Bailey]

I know that 3/4 is only achieved for very specific composites, I think composites of the form p * (2p + 1) for prime p.
It's p * (2p - 1) for which it approaches 3/4.

[Bolton Bailey]

I guess there are infinitely many of those? Edit it's conjectured, but apparently not proven.

[Thomas Zhu]

The first axiom is definitely true for some H: just let H p i be the compositeness witness of p if p is composite. The question is more if it's true for a specific computable H, like SHA3 for primes < 2 ^ 4096

[Thomas Zhu]

Bolton Bailey said:

Incidentally, Kevin's comment has gotten me curious: Is it true/known that the sum over composite n from n = 1 to infinity of the fraction of k < n that are non Miller-Rabin witnesses diverges? Or if that sequence when raised to the power of 256/ some other value diverges?

Well, for this specific series, it of course diverges because -1 is a nonwitness for every composite number, so the fraction is at least 1/n

[Bolton Bailey]

Right. The cryptographic justification would be that H is some very random-looking function that we can approximate by a "random oracle" - that is, a function whose outputs are independently random for any input. So I am wondering what the probability of the statement being false if for a random H.

[Bolton Bailey]

Thomas Zhu said:

Bolton Bailey said:

Incidentally, Kevin's comment has gotten me curious: Is it true/known that the sum over composite n from n = 1 to infinity of the fraction of k < n that are non Miller-Rabin witnesses diverges? Or if that sequence when raised to the power of 256/ some other value diverges?

Well, for this specific series, it of course diverges because -1 is a nonwitness for every composite number, so the fraction is at least 1/n

Ah good point. But if we repeat the test, we raise the fraction to a power and the series 1/n^2 doesn't diverge, so this doesn't prove that there is no number of repetitions for which it diverges.

[Frédéric Dupuis]

axiom definitely doesn't look like the right tool for the job here. It shouldn't be too hard to define the probability distribution of the output of Miller-Rabin on a given composite number, and then prove that the error probability goes down exponentially with the number of rounds.

[Mario Carneiro]

I recall the Starkware certification by @Jeremy Avigad included a probabilistic claim of exactly this form. It was stated as saying that the size of the bad set was smaller than some explicit small bound

[Mario Carneiro]

https://github.com/starkware-libs/formal-proofs/blob/d0edfe9f3601bfd073c10ad8fc14d0ec7c77fc7f/src/starkware/cairo/lean/semantics/air_encoding/final_correctness.lean#L37-L81

[Thomas Zhu]

Frédéric Dupuis said:

axiom definitely doesn't look like the right tool for the job here. It shouldn't be too hard to define the probability distribution of the output of Miller-Rabin on a given composite number, and then prove that the error probability goes down exponentially with the number of rounds.

I agree we shouldn't need axioms. We would indeed be able to prove that "if we try MR r times on composite n, there only prob. 4^-r that it still returns true". The axiom gets us the "contrapositive": "if we try MR r times on n and it returns true, n is probably prime (with prob 1-4^-r, conceptually)". But we can't say a number is "probably prime" because it's either prime or composite.

For a theorem T depending on primality of p that is only possible to test with MR, instead of showing "T" we can show instead "If T is false, we can prove it's false with prob. 1/2", and this doesn't need any axioms.

If anything one might state an axiom that Baillie PSW is right - it's deterministic, as fast as MR, and we haven't found a counterexample despite many targeted searches, and it's shown correct for under 2^64.

[Mario Carneiro]

axiomatizing that a probabilistic algorithm is correct will usually result in a short proof of false, and axiomatizing that a probabilistic algorithm is correct for less than some big but fixed value of n (larger than anything that has been actually proved) is gambling with unclear odds

[Bolton Bailey]

Thomas Zhu said:

Frédéric Dupuis said:

axiom definitely doesn't look like the right tool for the job here. It shouldn't be too hard to define the probability distribution of the output of Miller-Rabin on a given composite number, and then prove that the error probability goes down exponentially with the number of rounds.

I agree we shouldn't need axioms. We would indeed be able to prove that "if we try MR r times on composite n, there only prob. 4^-r that it still returns true". The axiom gets us the "contrapositive": "if we try MR r times on n and it returns true, n is probably prime (with prob 1-4^-r, conceptually)". But we can't say a number is "probably prime" because it's either prime or composite.

For a theorem T depending on primality of p that is only possible to test with MR, instead of showing "T" we can show instead "If T is false, we can prove it's false with prob. 1/2", and this doesn't need any axioms.

I have considered this approach too. You can even define a general transform that turns any proposition you want into a type of probabilistic tests of that proposition, and then combine probabilistic tests at will, then run a test at any time you want for confirmation.

I still think there's value in the axiom approach, though, since that way you don't have to carry this mildly weird new type with you after you test your result.

[Yuyang Zhao]

Yuyang Zhao said:

Jireh Loreaux said:

By the way, I think #8885 should make the fast modular exponentiation above unnecessary. (Or rather, it already implements it)

I was going to make something similar after std4#314.

I found my branch and made #9154. But it depends on too many other PRs. It may take a while before it can be merged.

[Thomas Zhu]

To answer the speed comparison: on my laptop, verifying the primality probable primality of 2^3217-1 using 500 rounds of Miller–Rabin takes 27 seconds on Lean (my implementation), 6 seconds on C (using OpenSSL BN_is_prime_ex), and 20 seconds on C if Montgomery multiplication is disabled (again OpenSSL).

[Kevin Buzzard]

Just to be clear, you're not claiming to actually verify the primality here right?

[Richard Copley]

Why not? Medium sized numbers like that (but randomer) are pretty useful! If anything 6s seems like a long time, even from 500 rounds. It's instantaneous here, using the sample code from the GMP source code.

[Richard Copley]

Oh, mathematically. That might take a little longer. The consensus seems to be that cryptography programs needn't bother.

[Thomas Zhu]

Kevin Buzzard said:

Just to be clear, you're not claiming to actually verify the primality here right?

No :) just that 500 rounds of MR doesn't find that it's composite, not that it proves it's prime

[Thomas Zhu]

All 3 tests are 500 rounds of MR