10.1. The exact target🔗

Take two pairs of complex numbers. Each pair must be linearly independent over the rational numbers. The conjecture states that at least one of their four exponential products is transcendental. A transcendental number is not a root of a nonzero polynomial with rational coefficients.

/-- The full complex Four Exponentials Conjecture. This definition is not a proof. -/
def Conjecture : Prop :=
  ∀ x y : Fin 2 → ℂ, LinearIndependent ℚ x → LinearIndependent ℚ y →
    ∃ i j, Transcendental ℚ (Complex.exp (x i * y j))

Move the pointer over the Lean terms to see their checked types. This definition states a proposition. It does not provide a proof.