Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Pi is irrational #15860

Open
mcdoll opened this issue Aug 4, 2022 · 5 comments
Open

Pi is irrational #15860

mcdoll opened this issue Aug 4, 2022 · 5 comments
Labels
good-first-project t-analysis Analysis (normed *, calculus)

Comments

@mcdoll
Copy link
Member

mcdoll commented Aug 4, 2022

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

Zulip
@mcdoll mcdoll added good-first-project t-analysis Analysis (normed *, calculus) labels Aug 4, 2022
@YaelDillies
Copy link
Collaborator

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

@vihdzp
Copy link
Collaborator

vihdzp commented Aug 13, 2022

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

@mcdoll
Copy link
Member Author

mcdoll commented Aug 13, 2022

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
Copy link
Member

Bhavik's work is at irrational-pi

@jcommelin
Copy link
Member

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
good-first-project t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@alexjbest @jcommelin @YaelDillies @mcdoll @vihdzp