$4$ has EML complexity at most 21

Proved

EmlComplexity.attains_four

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

elementary-functionseml-complexityexpression-complexity

The integer $4$ is the value of a valid closed EML tree with twenty-one nodes: $e^{e} - \ln\big(\exp(e^{e} - 4)\big)$ , where $e^{e} - 4$ is reached by four subtractions of $1$ from $e^{e}$ . Real-branch enumeration to size 20 finds no smaller tree; that lower bound is a separate open statement.

Preamble

import Definitions.Def_EmlComplexity

Formal statement

namespace EmlComplexity
theorem attains_four : Attains ((4 : ℝ)) 21 := 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

444 has EML complexity at most 21

$4$ has EML complexity at most 21