Stream: math-comp users

Topic: infinitude of primes via reglang?

Karl Palmskog (May 25 2020 at 12:49):

This looks like a sketchy proof that, if correct, could be done formally without too much effort using MathComp+RegLang (was mentioned by Buzzard on Twitter): https://arxiv.org/abs/2005.10372v1 https://twitter.com/XenaProject/status/1264554149259157504

Funny proof of infinitude of primes https://arxiv.org/abs/2005.10372v1 via Myhill-Nerode theorem. For natural n>=1, the language L_n := "words in letters {a,b} with number of a's - number of b's = multiple of n" is regular, but the union over all p of L_p is not so can't be a finite union.

- The Xena Project (@XenaProject)

Christian Doczkal (May 25 2020 at 19:11):

Well, I got curious so I took a look: I suppose all the ingredients are there. On the other hand, the proof explicitly appeals to "every number bigger than one has a prime divisor". This isn't hard, in mathcomp this falls out of prime factorization (whose proof is nontrivial). From there, proving that there is a prime larger than any (given) natural number takes three lines, using nothing other than that the divisors of "m!" are all the numbers up to "m". So, frankly, I do not see the point of using complicated machinery to prove simple facts.

Karl Palmskog (May 25 2020 at 19:17):

thanks for the analysis. I think the "point" would just be to see whether the de Bruijn factor for the proof is large (I suspect not), and also, many proofs of something can be useful for machine learning and mining, etc. I honestly would not mind if there was a list somewhere with probably straightforward but essentially pointless proofs that people could do for fun (using MathComp + additional libraries).

Last updated: Oct 13 2024 at 01:02 UTC