Formal target: Corpus.WikipediaExponentials.four_exponentials_conjecture

**Four exponentials conjecture** Let $x_0, x_1$ and $y_0, y_1$ be $\mathbb Q$-linearly independent pairs of complex numbers, then some $e^{x_i y_j}$ is transcendental.

Exact formal statement

∀ (x y : Fin 2 → Complex),
  LinearIndependent.{0, 0, 0} Rat x →
    LinearIndependent.{0, 0, 0} Rat y →
      Exists.{1} fun i => Exists.{1} fun j => Transcendental.{0, 0} Rat (Complex.exp (HMul.hMul.{0, 0, 0} (x i) (y j)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record