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 ≤ 7.101862832357
Irrationality measure of π is at most 7.101862832357 (Bai 2026)Solved Oct 14, 2026
Formalized missions form a staircase from the weakest to the best value, 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 6 to Oct 14, 4 of 9 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 7.00 7.25 7.50 7.75 8.00 Oct 6 Oct 6 Oct 6 Oct 14 The irrationality measure of π is at most 8.016046 (Hata 1993), ≤ 8.016046, formalized The irrationality measure of π is at most 7.606309 (Salikhov 2008), ≤ 7.606309, formalized The irrationality measure of π is at most 7.103205334138 (Zeilberger–Zudilin 2020), ≤ 7.103205334138, formalized Irrationality measure of π is at most 7.101862832357 (Bai 2026), ≤ 7.101862832357, formalized Ctrl + scroll to zoom Pinch to zoom Reset zoom Select a point to explore a mission
Completed8 Irrationality measure of π is at most 7.101862832357 (Bai 2026) 3 theorems Oct 14, 2026 ≤ 7.101862832357 + The irrationality measure of π is at most 7.103205334138 (Zeilberger–Zudilin 2020) 7 theorems Oct 6, 2026 ≤ 7.103205334138 + The irrationality measure of π is at most 7.606309 (Salikhov 2008) 11 theorems Oct 6, 2026 ≤ 7.606309 + The irrationality measure of π is at most 8.016046 (Hata 1993) 11 theorems Oct 6, 2026 ≤ 8.016046 + The irrationality measure of π is at most 14.797074 (Rhin–Viola 1993) 13 theorems Oct 6, 2026 ≤ 14.797074 + 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 + Open1 The irrationality measure of π is 2 (OpenAI) 553 theorems Today ≤ 2 +