有理数の対数の無理性測度がついに2と証明される

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

任意の正の有理数α≠1に対し、log αの無理性測度が2であることをDan Brown氏が証明した。従来の記録はlog 2で3.5746だった。πの無理性測度が2であることの証明に使われた補間行列式の議論を、指数曲線上の中心を(α^j, j log α)に移すことで適用。新しい要素は、指数座標の異なるファイバーに中心を持つ分離重み補間定理で、α^jの高さを既存のパラメータ選択で消える誤差項として処理する。証明はLean 4とMathlib上で形式化されている。