pi is irrational?

Stream: mathlib4

[Kim Morrison]

Does anyone have a proof that pi is irrational on hand, that they could PR?

I know that there is a PR in process #6718, containing the much stronger result that it is transcendental, but there may be a way to go before that is merged.

It feels a little embarrassing at this point in time to still not have this in. :-)

[Riccardo Brasca]

The proof here (Niven's proof) should be rather easy to formalize.

[Ruben Van de Velde]

I wouldn't be surprised if someone did it already. (If anyone has thoughts on #6718, do let me know :innocent:)

[Eric Wieser]

I think @Bhavik Mehta had a lean 3 PR with this result, and perhaps a lean4 translation locally?

[Kim Morrison]

@Bhavik Mehta, would you be able to translate https://github.com/leanprover-community/mathlib3/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean and PR it?

[Violeta Hernández]

Is our plan to have two separate proofs of irrationality? Or rather to have a proof of irrationality with less imports than the one for trascendentality?

[Daniel Weber]

Do we have Apéry's theorem? Something very similar also works for $\zeta(2)$

[Kevin Buzzard]

I met someone at AMSS in China who said they were working on it. I'll dig out their name when I'm at a computer

[Riccardo Brasca]

Violeta Hernández said:

Is our plan to have two separate proofs of irrationality? Or rather to have a proof of irrationality with less imports than the one for trascendentality?

This seems reasonable, irrationality is a rather elementary argument.

[Kevin Buzzard]

@Lihong Zhi is it you who is doing $\zeta(3)$ in Lean? Can you also do $\zeta(2)$? We already have $\zeta(2)=\pi^2/6$ thanks to David Loeffler, so this would be enough.

[Lihong Zhi]

Kevin Buzzard said:

Lihong Zhi is it you who is doing $\zeta(3)$ in Lean? Can you also do $\zeta(2)$? We already have $\zeta(2)=\pi^2/6$ thanks to David Loeffler, so this would be enough.

Yes. my student @ahhwuhu (Junqi Liu) and @Jujian Zhang are proving $\zeta(3)$ is irrational in Lean. It should be easy to adjust their proof to show $\zeta(2)$ is irrational. They will do it later.

[Bhavik Mehta]

Kim Morrison said:

Bhavik Mehta, would you be able to translate https://github.com/leanprover-community/mathlib3/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean and PR it?

Sure, I have a ported version lying around somewhere. I never really viewed it as high priority since people are working on generalised versions already, but I don't mind doing it. (Similarly I did $\zeta(2) = \pi^2 / 6$ about four years ago, but never bothered upstreaming it because David's work gives a more general result!)

[Kim Morrison]

(There's been some "we have this stuff but Lean doesn't" going around, and it seems easier to explain "well actually it does, see Mathlib", rather than "well actually it does, see Bhavik's un-PR'd work on this branch of an archived repository".)

[Johan Commelin]

I think we can have a bit of community effort to get

feat: Lindemann-Weierstrass Theorem #6718

into mathlib in the near future. Ruben Van de Velde already started :octopus:

[Bhavik Mehta]

There's a PR at #17103 now, with help from Eric!

[Bhavik Mehta]

This one should be ready for review - I added quite a bit of explanation for the proof, I hope it is clear.

[Johan Commelin]

Thanks! Borsified

[Junqi Liu]

@Kevin Buzzard we have completed the proof of the irrationality of $\zeta(3)$ in Lean! We'll adjust our proof to show $\zeta(2)$ is irrational!

[Lihong Zhi]

Congratulations to Junqi and Jujian!

[Kevin Buzzard]

If we have irrationality of $\zeta(3)=\prod_p(1-p^{-3})^{-1}$ then we can deduce infinitude of primes :-) (RHS is clearly rational if there are only finitely many primes)

[Riccardo Brasca]

Very nice!! And we surely want this in mathlib :)

[Jujian Zhang]

ahhwuhu said:

Kevin Buzzard we have completed the proof of the irrationality of $\zeta(3)$ in Lean! We'll adjust our proof to show $\zeta(2)$ is irrational!

To be clear, the proof still relies on pi_alt from PrimeNumberTheoremAnd project so technically it is not sorry free yet.

[Junqi Liu]

We have done pi_alt yet. It is sorry free now! We'll make a PR later.