search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Pi is irrational #15860

Open mcdoll opened 2 years ago

mcdoll commented 2 years ago

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

Zulip

YaelDillies commented 2 years ago

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

vihdzp commented 2 years ago

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

mcdoll commented 2 years ago

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 commented 2 years ago

Bhavik's work is at irrational-pi

jcommelin commented 2 years ago

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