monogate.dev / challenges / i (strict grammar)
i (strict grammar)
PROVED IMPOSSIBLE
Construct i = √−1 from terminal {1} under strict principal-branch grammar. Under extended-reals convention this is solved (K=75, pveierland). Under strict grammar it remains open.
Result
Proved impossible under the strict real grammar (principal-branch ln, ln(0) throws). Theorem T17, machine-verified in Lean 4: no finite real EML tree from {1} evaluates to i = sqrt(-1). Under the extended-reals grammar the problem remains open.
ProofT17
Grammar
Allowed
✓eml(x, y) = exp(x) − ln(y) — the single operator
✓Terminal: constant 1
✓Terminal: variable x (for function challenges)
✓Compositions: any finite binary tree over the above
Forbidden
✗ln(0) — undefined, throws RangeError
✗Math.sin, Math.cos, Math.PI, or any Math.* shortcut
✗Any function outside the EML grammar
✗Extended-reals convention (ln(0) = −∞) — not this grammar
Under extended-reals grammar (pveierland/eml-eval), i is solved at K=75. This challenge is the strict grammar variant where ln(0) throws.
Leaderboard — 0 valid constructions
#
Author
Nodes
Depth
Date
No valid constructions yet. Be the first.