EML: Lean 4 Formalization

A Lean 4 + Mathlib formalization of the results in:

Andrzej Odrzywołek (Institute of Theoretical Physics, Jagiellonian University), "All elementary functions from a single binary operator", arXiv:2603.21852 [cs.SC], April 2026.

All mathematical results from the paper are due to Odrzywołek. This project is a machine-checked formalization of his work in the Lean 4 theorem prover, plus some original extensions (algebraic structure, calculus, and fixed-point analysis of the EML operator). The discovery of the EML operator, the exhaustive search methodology, the completeness proof strategy, and all identities originate from the paper above.

Odrzywołek discovered that a single binary operator

eml(x, y) = exp(x) - ln(y)

together with the constant 1, generates the entire standard repertoire of a scientific calculator: arithmetic, exponentiation, logarithms, trigonometric and hyperbolic functions, their inverses, and fundamental constants like e, π, and i. This is the continuous analogue of the NAND gate in digital logic.

14 Lean files. 160 definitions and theorems. 0 sorry.

• exp(x) = eml(x, 1)
• e = eml(1, 1)
• ln(z) = eml(1, eml(eml(1, z), 1)) for z > 0 — paper equation (5)
• 0 = eml(1, eml(eml(1, 1), 1)) — pure EML tree, K = 7
• -1 and 2 derivable via the exp-log chain

Every primitive from the paper's Table 1 is shown to reduce to {1, eml}:

Trigonometric functions and the constants π and i are proved over ℂ using Euler's formula and a complex EML operator ceml(x,y) = exp(x) - log(y).

Pure EML trees for the "hard" functions, found by exhaustive brute-force search (reproducing the paper's Table 4 methodology) and verified symbolically in Lean:

The search script (search.py) is included for reproducibility.

• Inductive types EmlTree, EmlExpr, EmlExpr₂ formalizing the context-free grammar S → 1 | x | eml(S, S)
• Verified tree evaluations matching Figure 2: exp (K=3), ln (K=7), identity (K=9), zero (K=7), e (K=3)

• An ExpLogExpr type for expressions built from {1, x, exp, log}
• A compile function converting exp-log expressions to EML trees
• compile_correct: the compiler preserves semantics for all exp-log expressions

• Paper equation (1): x × y = exp(ln x + ln y) and x + y = ln(exp x · exp y)
• Subtraction, division, negation, reciprocal, integers via exp-log

• EDL operator: edl(x, y) = exp(x) / ln(y) — paper equation (4b)
• Negated EML: neml(x, y) = ln(x) - exp(y) — paper equation (4c)
• Relationships between variants

• Level-1 and level-2 parametrized master formulas — paper equation (6)
• Recovering exp(x), e, and exp(exp(x)) from specific parameter choices
• Parameter count formula: 5 × 2ⁿ − 6

• suc(inv(pre(inv(suc(inv(x)))))) = -x — paper Section 2

Properties of eml as a binary operation, not discussed in the paper:

• Non-commutativity: eml(0, 1) = 1 ≠ e = eml(1, 0)
• Non-associativity: eml(eml(0,1), 1) = e ≠ 0 = eml(0, eml(1,1))
• No identity element: no e exists such that eml(e, x) = x for all x, nor eml(x, e) = x for all x

Differential and monotonicity properties of eml:

• Partial derivatives: ∂/∂x eml(x, y) = exp(x) and ∂/∂y eml(x, y) = -1/y
• Monotonicity: strictly increasing in x, strictly decreasing in y (for y > 0)
• Injectivity: injective in each argument (for y > 0 in the second)

Analysis of special values of eml:

• Zero set: eml(a, b) = 0 ↔ b = exp(exp(a))
• Level sets: eml(a, b) = c ↔ b = exp(exp(a) - c) for b > 0
• Fixed point equation: eml(x, x) = x ↔ exp(x) - x = log(x)
• Fixed points satisfy x > 1 (proved via strict convexity of exp)
• Self-application: eml(x, eml(x, 1)) = exp(x) - x

• Table 4 optimality: proving a K value is minimal requires exhaustive enumeration of all smaller trees — a computation, not a deduction.
• EDL completeness: the paper states EDL also generates all primitives but provides no explicit constructions.
• Symbolic regression convergence (Section 4.3): an empirical result from training experiments.

Requires Lean 4 and Mathlib.

lake update
lake build

The core mathematical content formalized here is the work of Andrzej Odrzywołek. The algebraic structure, calculus, and fixed-point sections are original extensions. Please cite his paper:

@article{odrzywołek2026eml,
  title={All elementary functions from a single binary operator},
  author={Odrzywołek, Andrzej},
  year={2026},
  eprint={2603.21852},
  archivePrefix={arXiv},
  primaryClass={cs.SC}
}

MIT