log2_log3_irrational
Provedalgebraalgebraic-geometrydiophantinelogarithmslogicnumber-theoryready-to-formalizetranscendental-number-theory
Irrationality of log₃(2) = log(2)/log(3): Is log(2)/log(3) irrational? By Gelfond-Schneider, it IS transcendental (it's an irrational algebraic power, so the result applies). But the full statement that log(2)/log(3) is irrational is a consequence of the algebraic independence of log 2 and log 3, which is open (Schanuel's conjecture).
Preamble
import Mathlib
Formal statement
import Mathlib
theorem log2_log3_irrational :
Irrational (Real.log 2 / Real.log 3) := by
sorrySource