mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Pi is irrational

Open mcdoll opened this issue 2 years ago • 5 comments

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

Zulip

mcdoll avatar Aug 04 '22 13:08 mcdoll

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

YaelDillies avatar Aug 13 '22 14:08 YaelDillies

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

vihdzp avatar Aug 13 '22 14:08 vihdzp

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.

mcdoll avatar Aug 13 '22 14:08 mcdoll

Bhavik's work is at irrational-pi

alexjbest avatar Oct 10 '22 23:10 alexjbest

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

jcommelin avatar Oct 11 '22 00:10 jcommelin