Logarithmen rationaler Zahlen haben Irrationalitätsmaß 2

The logarithms of rational numbers have irrationality exponent 2 [pdf]

Für jede positive rationale Zahl α ≠ 1 ist das Irrationalitätsmaß von log α gleich 2. Der Beweis überträgt die Interpolationsdeterminanten-Methode, die μ(π)=2 liefert, auf die Exponentialkurve, indem die Interpolationszentren von (1, 2πij) nach (α^j, j log α) verschoben werden. Für log 2 verbessert dies die bisherige Schranke 3,5746 auf 2. Der Beweis wurde in Lean 4 über Mathlib formalisiert.