Active
The irrationality measure of π The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
Best formalized bound ≤ 19.8899945
The irrationality measure of π is at most 19.8899945 (Chudnovsky 1982)Solved Oct 3, 2026
Formalized missions form a staircase in recorded order, one slot per mission at uniform spacing. Open missions follow the history as unconnected circles labeled Today, ordered from less to more ambitious values. Select a point to highlight its mission on this page. Showing Oct 3, 2 of 7 missions. Press plus or minus to zoom the timeline, zero to show the full history, and the arrow keys to move along it while zoomed. Upper bound 19.8 20.0 20.2 20.4 20.6 Oct 3 Oct 3 The irrationality measure of π is at most 20.6 (Mignotte 1974), ≤ 20.6, formalized The irrationality measure of π is at most 19.8899945 (Chudnovsky 1982), ≤ 19.8899945, formalized Ctrl + scroll to zoom Pinch to zoom Reset zoom Select a point to explore a mission
Completed3 The irrationality measure of π is at most 19.8899945 (Chudnovsky 1982) 2 theorems Oct 3, 2026 ≤ 19.8899945 + The irrationality measure of π is at most 20.6 (Mignotte 1974) 2 theorems Oct 3, 2026 ≤ 20.6 + Mahler's irrationality bound for π: 42 3 theorems Oct 1, 2026 ≤ 42 + Open4 The irrationality measure of π is at most 14.797074 (Rhin–Viola 1993) 13 theorems Today ≤ 14.797074 + The irrationality measure of π is at most 8.016046 (Hata 1993) 11 theorems Today ≤ 8.016046 + The irrationality measure of π is at most 7.606309 (Salikhov 2008) 11 theorems Today ≤ 7.606309 + The irrationality measure of π is at most 7.103205334138 (Zeilberger–Zudilin 2020) 2 theorems Today ≤ 7.103205334138 +