What are the primes less than 10000000?

Stream: lean4

[Kevin Buzzard]

docs#Nat.primesBelow sends n : Nat to the finset of primes less than n. A passing mathematician might idly think "so what are the primes less than 10000000?" (or, more likely, "let's check my new conjecture about prime numbers for all primes less than 10000000"). In pari I just type forprime(p=0,10000000,print(p)) and a few seconds later I have the answer. But I just typed #eval primesBelow 10000000 into Lean and it crashed. There are plenty of mathematicians out there who use computer algebra systems to just do basic calculations like this, it would be interesting if this could be supported somehow in Lean.

[Kevin Buzzard]

The recent breakthrough work of Newton and Thorne on high symmetric power functoriality for GL(2) uses a one crucial point an explicit calculation of the 2-adic eigencurve which was all worked out conjecturally by me and others just by playing with power series with coefficients in the 2-adic numbers in pari-gp (and then all proved by me and others on paper)

[Rida Hamadani]

A similar thought has occurred to me before, in general, I think it would be awesome to have more CAS features in lean!

[Adam Topaz]

It’s certainly possible to implement this function using a basic sieve then prove the two are the same (and tag the proof with csimp)

[Junyan Xu]

I think this is done here.
However #eval primes 1000000 (one less zero) crashes in web editor. (apparently a stack overflow error)

[Eric Wieser]

I think that's just a printing issue

[Eric Wieser]

#eval (primes 1000000).size is fast

[Eric Wieser]

As is #eval toString (primes 1000000); the problem is with the Formatter

[Number Eighteen]

This may be faster if you need high numbers. But a segmentation scheme needs to be added to the code if you must get far beyond 2^32.

[Kevin Buzzard]

I went with 10^8 because experimentation showed that I could print all the primes less than that in just a few seconds on the command line using pari, so I knew it was not a computationally unreasonable ask

[Ivan Gonzalez]

Te vas a regalar gato podrido

[Eric Wieser]

Junyan Xu said:

I think this is done here.
However #eval primes 1000000 (one less zero) crashes in web editor. (apparently a stack overflow error)

Should @Mario Carneiro's code here be PR'd?

[Mario Carneiro]

I suppose we could have Mathlib.Data.Nat.Prime.Sieve or something

[Mario Carneiro]

There are definitely ways to push the code further, e.g. using a bitset instead of two arrays