Logarithms of Rational Numbers Have Irrationality Measure Exactly 2
The logarithms of rational numbers have irrationality exponent 2 [pdf]
For every positive rational α ≠ 1, the irrationality measure of log α is exactly 2. This improves the previous bound for log 2 from 3.5746 to 2, matching the known result for π. The proof adapts an interpolation-determinant argument by moving interpolation centers onto the exponential curve, with a new separated-weight theorem for centers in distinct fibers. The work is formalized in Lean 4 over Mathlib and also gives bounds for logarithms of real algebraic numbers.
For every positive rational α ≠ 1 the irrationality measure of log α equals 2: for every ν > 2, |log α − p/q| ≥ q^{−ν} for all integers p, q with q sufficiently large.
- WalterGR
15 comments here: https://news.ycombinator.com/item?id=49961538
Mostly about the claim and not the (purported?) author.
- jdb1729
This is a Lean-verified variation of the OpenAI proof for pi.
- elromulous
I love this footnote
∗Author of The Da Vinci Code.