Pi is irrational

[mcdoll]

Prove that real.pi is irrational using Niven's argument, see also Wikipedia

Zulip

[YaelDillies]

@b-mehta has a proof somewhere, and maybe @vihdzp is getting close to this too?

[vihdzp]

I was proving another one of Niven's theorems, the one about rational cosines.

[mcdoll]

when this was discussed someone mentioned that Bhavik has a proof, but if he does not PR it into mathlib I see no problem having it as a possible first project.

[alexjbest]

Bhavik's work is at irrational-pi

[jcommelin]

What is the status of the Lindemann result that immediately shows that π is transcendental? That was mostly formalized somewhere, right?