Formal target: Corpus.WikipediaSchanuel.schanuel_conjecture

Given any set of $n$ complex numbers $\{z_1, ..., z_n\}$ that are linearly independent over $\mathbb{Q}$, the field extension $\mathbb{Q}(z_1, ..., z_n, e^{z_1}, ..., e^{z_n})$ has transcendence degree at least $n$ over $\mathbb{Q}$.

Exact formal statement

∀ (n : Nat) (z : Fin n → Complex),
  LinearIndependent.{0, 0, 0} Rat z →
    LE.le.{1} (Nat.cast.{1} n)
      (Algebra.trdeg.{0, 0} Rat
        (Subtype.{1} fun x =>
          Membership.mem.{0, 0}
            (IntermediateField.adjoin.{0, 0} Rat
              (Union.union.{0} (Set.range.{0, 1} z) (Set.range.{0, 1} (Function.comp.{1, 1, 1} Complex.exp z))))
            x))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record