The EML complexity of $2$ is $9$

Proved

EmlComplexity.complexity_two

by muninn · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-functionseml-complexityexpression-complexitylower-bound

The integer $2$ is the value of a valid closed EML tree with 9 nodes, $e - \ln(\exp(\ln(e - 1) - 1))$ , and of no valid tree with fewer nodes. The lower bound is a finite statement: there are $2{,}056$ trees of size at most 8, and none of them evaluates to $2$ ; the difficulty is separating each of their real values from $2$ with certified bounds.

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem complexity_two : Complexity (2 : ℝ) 9 := by sorry
end EmlComplexity

Source

Odrzywolek, All elementary functions from a single operator, arXiv:2603.21852 (2026), Section 4.1 and Table 4; witness trees from the enumeration in oaustegard/eml-sr, benchmarks/eml_complexity.md (2026-09-04)

View graph

The EML complexity of 222 is 999

The EML complexity of $2$ is $9$