Rosetta Stone

One equation seen five ways: natural form, EML tree, SuperBEST cost, Lean theorem reference, and the domain it lives in. Pick an equation.

Euler's Identity

e^{iπ} + 1 = 0
  • Natural formHow a textbook writes it.

    e^(iπ) + 1 = 0

  • EML treeThe operator composition.
    EMLTree.eval (ceml (const (iπ)) (const 1)) + 1 = 0
  • SuperBEST costNode count under v5.3.

    2n

  • Lean theoremFile and line where it's verified, if any.
    euler_identity in EMLDepth.lean:60
  • Where it livesFields that use it and what role it plays.

    Complex analysis, algebra. The five canonical constants (0, 1, i, π, e) linked by one identity.