Active
Sharp diagonal Hlawka constant The sharp Hlawka inequality for Schatten p p p proved in Lean for every real p ≥ 256 p\ge256 p ≥ 256 p ≥ 2 p\ge2 p ≥ 2
What is the smallest cutoff p ′ p' p ′ p ≥ p ′ p\ge p' p ≥ p ′
References:
Best formalized bound ≤ 4
Sharp diagonal Hlawka constants: lower the cutoff to 4Solved Oct 29, 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 16 to Today, 8 of 18 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 0 10 20 30 Oct 16 Oct 17 Oct 26 Oct 27 Oct 27 Oct 27 Oct 29 Today Sharp diagonal Hlawka constant: cutoff 32, ≤ 32, formalized Sharp diagonal Hlawka constant: formalize cutoff 21, ≤ 21, formalized Sharp diagonal Hlawka constants: lower the cutoff to 16, ≤ 16, formalized Sharp diagonal Hlawka constants: lower the cutoff to 12, ≤ 12, formalized Sharp diagonal Hlawka constants: lower the cutoff to 8, ≤ 8, formalized Sharp diagonal Hlawka constants: lower the cutoff to 6, ≤ 6, formalized Sharp diagonal Hlawka constants: lower the cutoff to 4, ≤ 4, formalized Sharp diagonal Hlawka constants: lower the cutoff to 2, ≤ 2, open mission Ctrl + scroll to zoom Pinch to zoom Reset zoom Select a point to explore a mission
Open1 Sharp diagonal Hlawka constants: lower the cutoff to 2 2,391 theorems Today ≤ 2 + Completed17 Sharp diagonal Hlawka constants: lower the cutoff to 4 7 theorems Oct 29, 2026 ≤ 4 + Sharp diagonal Hlawka constants: lower the cutoff to 6 5 theorems Oct 27, 2026 ≤ 6 + Sharp diagonal Hlawka constants: lower the cutoff to 8 5 theorems Oct 27, 2026 ≤ 8 + Sharp diagonal Hlawka constants: lower the cutoff to 12 5 theorems Oct 27, 2026 ≤ 12 + Sharp diagonal Hlawka constants: lower the cutoff to 16 90 theorems Oct 26, 2026 ≤ 16 + Sharp diagonal Hlawka constant: formalize cutoff 21 11 theorems Oct 17, 2026 ≤ 21 + Sharp diagonal Hlawka constant: cutoff 32 4 theorems Oct 16, 2026 ≤ 32 + Sharp diagonal Hlawka constants: lower the cutoff to 50 64 theorems Oct 16, 2026 ≤ 50 + Sharp diagonal Hlawka constants: lower the cutoff to 62 5 theorems Oct 10, 2026 ≤ 62 + Sharp diagonal Hlawka constants: lower the cutoff to 70 66 theorems Oct 10, 2026 ≤ 70 + Sharp diagonal Hlawka constants: lower the cutoff to 80 64 theorems Oct 6, 2026 ≤ 80 + Sharp diagonal Hlawka constants: lower the cutoff to 84 5 theorems Oct 6, 2026 ≤ 84 + Sharp diagonal Hlawka constants: lower the cutoff to 85 63 theorems Oct 6, 2026 ≤ 85 + Sharp diagonal Hlawka constants: lower the cutoff to 87 5 theorems Oct 5, 2026 ≤ 87 + Sharp diagonal Hlawka constants: lower the cutoff to 89 63 theorems Oct 5, 2026 ≤ 89 + Sharp diagonal Hlawka constants: formalize the supplied proof at cutoff 90 61 theorems Oct 1, 2026 ≤ 90 + Sharp diagonal Hlawka constants: foundation and proved cutoff 256 59 theorems Sep 29, 2026 ≤ 256 +