The assume-eval specification

The public specification: how a case is graded, every function a case may use, and how their translations are checked.

How it works

Each makes one claim, LHS = RHS, about numbers under assumptions; a system says whether it holds at every point. Everything is over ℂ, with explicit .

From case to outcome

Hover, focus or tap a step (or any dotted word) for the details.

Three labels

true

LHS = RHS at every admissible point

given x > 0: √(x²) = x

correct answer: true

false

LHS ≠ RHS at every admissible point (one counterexample is not enough)

given x ∈ ℝ: exp(x) = 0

correct answer: false

contingent

equal at some admissible point, unequal at another

given x ∈ ℝ: √(x²) = x

correct answer: null

A system answers true, false or ; is a label, never an answer, and on a contingent case null is correct. Outcomes are counted separately, with no combined score; see . Where systems differ by convention, the spec lists and the labels hold under all of them.

Key terms

The functions

The and every library function, generated from spec/ on every request; .

Core

The hand-written : every library function below is defined from these.

i

the imaginary unit

defined always

gen-lean writes it as AE.i

defined in spec/core.lean
def i : ℂ := Complex.I
built into Lean / Mathlib
Complex.I : ℂ

π

π, as a complex number

defined always

gen-lean writes it as AE.pi

defined in spec/core.lean
def pi : ℂ := (Real.pi : ℂ)
built into Lean / Mathlib
Real.pi : ℝ

a + b

Mathlib's addition on ℂ, componentwise

defined always

gen-lean writes it as (a + b)

built into Lean / Mathlib
Complex.add_re : ∀ (z w : ℂ), (z + w).re = z.re + w.re
Complex.add_im : ∀ (z w : ℂ), (z + w).im = z.im + w.im

a − b, −a

Mathlib's subtraction and negation on ℂ

defined always

gen-lean writes it as (a - b), (-a)

built into Lean / Mathlib
Complex.sub_re : ∀ (z w : ℂ), (z - w).re = z.re - w.re
Complex.sub_im : ∀ (z w : ℂ), (z - w).im = z.im - w.im
Complex.neg_re : ∀ (z : ℂ), (-z).re = -z.re
Complex.neg_im : ∀ (z : ℂ), (-z).im = -z.im

a·b

Mathlib's multiplication on ℂ

defined always

gen-lean writes it as (a * b)

built into Lean / Mathlib
Complex.mul_re : ∀ (z w : ℂ), (z * w).re = z.re * w.re - z.im * w.im
Complex.mul_im : ∀ (z w : ℂ), (z * w).im = z.re * w.im + z.im * w.re

a/b

division: a times the inverse b⁻¹

defined when b ≠ 0

gen-lean writes it as (a * AE.inv b)

defined in spec/core.lean
def inv (a : ℂ) : ℂ := a⁻¹
built into Lean / Mathlib
div_eq_mul_inv : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
inv_zero : ∀ {G₀ : Type u} [inst : GroupWithZero G₀], 0⁻¹ = 0
Complex.inv_re : ∀ (z : ℂ), z⁻¹.re = z.re / Complex.normSq z
Complex.inv_im : ∀ (z : ℂ), z⁻¹.im = -z.im / Complex.normSq z

Mathlib's 0⁻¹ = 0 (inv_zero) is never used: a/b is only defined when b ≠ 0.

exp(a)

the complex exponential

defined always

gen-lean writes it as (AE.exp a)

defined in spec/core.lean
def exp (a : ℂ) : ℂ := Complex.exp a
built into Lean / Mathlib
Complex.exp : ℂ → ℂ

log(a)

the principal logarithm: Im log(a) ∈ (−π, π], so log(−1) = iπ

defined when a ≠ 0

gen-lean writes it as (AE.log a)

defined in spec/core.lean
def log (a : ℂ) : ℂ := Complex.log a
theorem log_im_mem (a : ℂ) : (Complex.log a).im ∈ Set.Ioc (-Real.pi) Real.pi :=
  ⟨Complex.neg_pi_lt_log_im a, Complex.log_im_le_pi a⟩
theorem log_neg_real (x : ℝ) (hx : x < 0) : (Complex.log (x : ℂ)).im = Real.pi := by
  rw [Complex.log_im, Complex.arg_ofReal_of_neg hx]
built into Lean / Mathlib
Complex.log : ℂ → ℂ

Mathlib's log 0 = 0 is never used: log a is only defined when a ≠ 0.

conj(a)

the complex conjugate

defined always

gen-lean writes it as (AE.conj a)

defined in spec/core.lean
def conj (a : ℂ) : ℂ := (starRingEnd ℂ) a

Re(a)

the real part (as a complex number)

defined always

gen-lean writes it as (AE.re a)

defined in spec/core.lean
def re (a : ℂ) : ℂ := (a.re : ℂ)

Im(a)

the imaginary part (as a complex number)

defined always

gen-lean writes it as (AE.im a)

defined in spec/core.lean
def im (a : ℂ) : ℂ := (a.im : ℂ)

⌊a⌋

the greatest integer ≤ a

defined when a is real

gen-lean writes it as (AE.floor a)

defined in spec/core.lean
def floor (a : ℂ) : ℂ := ((Int.floor a.re : ℤ) : ℂ)

a = b, a ≠ b

Lean's equality Eq and Ne (a ≠ b is ¬(a = b))

defined always

gen-lean writes it as (a = b), (a ≠ b)

built into Lean / Mathlib
Eq : {α : Sort u_1} → α → α → Prop
Ne : {α : Sort u} → α → α → Prop
Complex.ext_iff : ∀ {z w : ℂ}, z = w ↔ z.re = w.re ∧ z.im = w.im

a < b, a ≤ b, a > b, a ≥ b

comparison of real numbers

defined when a and b are real

gen-lean writes it as (AE.lt a b), (AE.le a b), (AE.gt a b), (AE.ge a b)

defined in spec/core.lean
def lt (a b : ℂ) : Prop := a.re < b.re
def le (a b : ℂ) : Prop := a.re ≤ b.re
def gt (a b : ℂ) : Prop := b.re < a.re
def ge (a b : ℂ) : Prop := b.re ≤ a.re

p and q, p or q, not p, p ⇒ q

Lean's And, Or, Not, and implication (the function arrow → between propositions)

defined when p and q are defined (short-circuit: q only where p holds for and / ⇒, where p fails for or)

gen-lean writes it as (p ∧ q), (p ∨ q), (¬p), (p → q)

built into Lean / Mathlib
And : Prop → Prop → Prop
Or : Prop → Prop → Prop
Not : Prop → Prop

(v₁ if c₁, …, else v)

the value of the first branch whose condition holds

defined when some branch condition holds

gen-lean writes it as (if c₁ then v₁ else … AE.undef)

defined in spec/core.lean
def undef : ℂ := 0

x ∈ ℝ, x ∈ ℤ, x ∈ ℚ

the parameter types and variable domains real, integer, rational

defined always

gen-lean writes it as AE.IsReal x, AE.IsInt x, AE.IsRat x

defined in spec/core.lean
def IsReal (a : ℂ) : Prop := a.im = 0
def IsInt (a : ℂ) : Prop := ∃ n : ℤ, a = (n : ℂ)
def IsRat (a : ℂ) : Prop := ∃ q : ℚ, a = (q : ℂ)
spec/core.lean in full
/-
  assume-eval: core semantics (hand-written; the only hand Lean besides primitives).

  Every expression of the benchmark format denotes a complex number (or a Prop),
  built from the operations below.  Mathlib totalises partial functions with junk
  values (Complex.log 0 = 0, a / 0 = 0, Real.sqrt (-1) = 0, ...).  These junk
  values must never leak into the meaning of a case, so:

    * we work over ℂ throughout (no Real.sqrt / Real.log);
    * every expression e comes with a definedness predicate D(e), generated
      alongside each library function (`AE.f.D`, see spec/generated/), and every
      case statement assumes / proves definedness explicitly;
    * the partial core operations and their definedness conditions are:
        inv a      defined iff a ≠ 0
        log a      defined iff a ≠ 0      (principal branch, Im ∈ (-π, π])
        floor a    defined iff a is real
        lt/le/...  defined iff both sides are real
        piecewise  defined iff some branch condition holds (else-branch optional)

  Imports.  This module is the one place that imports Mathlib; everything else (the
  generated module, spec/lemmas/, case-proof files, --lean-lib modules) gets Mathlib
  through `import core`.  Not `import Mathlib` as a whole: every Lean process loads
  the environment of its imports first, and all of Mathlib takes 15-60 s and several
  GB per process, this subset about 2 s.  The list is
    * the modules `#min_imports` reports for the spec, spec/lemmas/, the demo proofs
      and the simplipy-cases proofs and lemma modules when they import all of
      Mathlib (including instances and simp lemmas that the proofs use without
      naming them: real/star order, C*-algebra classes, pi bounds, ...);
    * the spec's vocabulary and the usual proof tactics, listed explicitly so that new
      case proofs find them (most are already imported by the first group).
  A proof that needs more Mathlib adds the module here (or, for an external case
  set, imports it in its own --lean-lib module).
-/
-- found by #min_imports
import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Algebra.Order.Star.Real
import Mathlib.Algebra.Ring.IsFormallyReal
import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Analysis.Real.Pi.Bounds
import Mathlib.Analysis.SpecialFunctions.Arcosh
import Mathlib.Analysis.SpecialFunctions.Arsinh
import Mathlib.Analysis.SpecialFunctions.Artanh
import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
import Mathlib.Data.Int.Star
import Mathlib.RingTheory.SimpleRing.Principal
-- vocabulary: complex exp / log / arg, trig and inverses, real powers and roots, primes
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
import Mathlib.Analysis.SpecialFunctions.Complex.Arctan
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.NumberTheory.Real.Irrational
-- tactics
import Mathlib.Tactic.Bound
import Mathlib.Tactic.Common
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

open Classical
noncomputable section

namespace AE

def i : ℂ := Complex.I
def pi : ℂ := (Real.pi : ℂ)

def inv (a : ℂ) : ℂ := a⁻¹
def exp (a : ℂ) : ℂ := Complex.exp a
/-- Principal logarithm.  Only meaningful when `a ≠ 0`. -/
def log (a : ℂ) : ℂ := Complex.log a
def conj (a : ℂ) : ℂ := (starRingEnd ℂ) a
def re (a : ℂ) : ℂ := (a.re : ℂ)
def im (a : ℂ) : ℂ := (a.im : ℂ)
/-- Floor of a real number (only meaningful when `IsReal a`). -/
def floor (a : ℂ) : ℂ := ((Int.floor a.re : ℤ) : ℂ)

/-- Value of a piecewise expression when no branch applies; its definedness
    predicate is `False`, so this junk value is never observed. -/
def undef : ℂ := 0

def IsReal (a : ℂ) : Prop := a.im = 0
def IsInt (a : ℂ) : Prop := ∃ n : ℤ, a = (n : ℂ)
def IsRat (a : ℂ) : Prop := ∃ q : ℚ, a = (q : ℂ)

/-- Real comparisons, only meaningful when both sides are real. -/
def lt (a b : ℂ) : Prop := a.re < b.re
def le (a b : ℂ) : Prop := a.re ≤ b.re
def gt (a b : ℂ) : Prop := b.re < a.re
def ge (a b : ℂ) : Prop := b.re ≤ a.re

/-- The principal logarithm has imaginary part in (-π, π]. -/
theorem log_im_mem (a : ℂ) : (Complex.log a).im ∈ Set.Ioc (-Real.pi) Real.pi :=
  ⟨Complex.neg_pi_lt_log_im a, Complex.log_im_le_pi a⟩

/-- On the negative real axis the principal log takes the value with Im = π. -/
theorem log_neg_real (x : ℝ) (hx : x < 0) : (Complex.log (x : ℂ)).im = Real.pi := by
  rw [Complex.log_im, Complex.arg_ofReal_of_neg hx]

end AE

end

Powers & roots

pow(z: complex, w: complex) → complex

Principal power z^w.

Lean (spec/generated/All.lean, )
def AE.pow (z w : ℂ) : ℂ := if z = 0 then 0 else AE.exp (w * AE.log z)
def AE.pow.D (z w : ℂ) : Prop := z ≠ 0 ∨ AE.gt (AE.re w) 0
definition
0if z = 0
exp(w·log(z))otherwise
z ≠ 0 or Re(w) > 0
systemtranslation check
SymPyPow({z}, {w})
WolframPower[{z}, {w}]
Maxima({z})^({w})
Source (spec/functions/pow.sexp)
(defun pow ((z complex) (w complex)) complex
  (doc "Principal power z^w."
       "z^w = exp(w log z); 0^w = 0 for re w > 0 (also for non-real w: |z^w| <= |z|^(re w) e^(pi |im w|) -> 0 as z -> 0; Wolfram 14.3 agrees, e.g. 0^(1+i) = 0) and undefined otherwise (incl. 0^0).  SymPy (<= 1.15-dev) and mpmath return nan for 0**w with any non-real w (SymPy Zero._eval_power, a rule from 2012 discussed in sympy/sympy#16478), treating ** as multi-valued only at 0 while SymPy's Pow is principal-valued everywhere else (e.g. (-1)**I = exp(-pi)); the spec follows the principal value.")
  (defined (or (!= z 0) (> (re w) 0)))
  (expand (piecewise ((= z 0) 0) (else (exp (* w (log z))))))
  (translate
    (sympy   "Pow({z}, {w})")
    (wolfram "Power[{z}, {w}]")
    (maxima  "({z})^({w})")))

sqrt(z: complex) → complex

Principal square root.

Lean (spec/generated/All.lean, )
def AE.sqrt (z : ℂ) : ℂ := if z = 0 then 0 else AE.exp (1 / 2 * AE.log z)
def AE.sqrt.D (z : ℂ) : Prop := True
definition
0if z = 0
exp((1/2)·log(z))otherwise
no condition of its own: wherever its definition is defined
systemtranslation check
SymPysqrt({z})
WolframSqrt[{z}]
Maximasqrt({z})
Source (spec/functions/sqrt.sexp)
(defun sqrt ((z complex)) complex
  (doc "Principal square root.")
  (expand (piecewise ((= z 0) 0) (else (exp (* 1/2 (log z))))))
  (translate
    (sympy   "sqrt({z})")
    (wolfram "Sqrt[{z}]")
    (maxima  "sqrt({z})")))

surd(x: real, n: integer) → real

Real n-th root of a real x, for a nonzero integer n.

Lean (spec/generated/All.lean, )
def AE.surd (x n : ℂ) : ℂ :=
  if AE.ge x 0 then AE.pow x (1 * AE.inv n) else -(AE.pow (-x) (1 * AE.inv n))
def AE.surd.D (x n : ℂ) : Prop :=
  AE.IsReal x ∧
  AE.IsInt n ∧
  (n ≠ 0 → (AE.IsReal x ∧ (¬AE.ge x 0 → AE.odd.D n)) ∧ (AE.ge x 0 ∨ AE.odd n → ¬x ≠ 0 → AE.IsReal n)) ∧
  (n ≠ 0 ∧ (AE.ge x 0 ∨ AE.odd n) ∧ (x ≠ 0 ∨ AE.gt n 0)) ∧
  AE.IsReal x ∧
  (AE.ge x 0 → n ≠ 0 ∧ AE.pow.D x (1 * AE.inv n)) ∧
  (¬AE.ge x 0 → n ≠ 0 ∧ AE.pow.D (-x) (1 * AE.inv n))
definition
x^(1/n)if x ≥ 0
−(−x)^(1/n)otherwise
n ≠ 0 and (x ≥ 0 or n is odd) and (x ≠ 0 or n > 0)
systemtranslation check
SymPyreal_root({x}, {n})
WolframSurd[{x}, {n}]
Source (spec/functions/surd.sexp)
(defun surd ((x real) (n integer)) real
  (doc "Real n-th root of a real x, for a nonzero integer n."
       "The nonnegative root for x >= 0, and -surd(-x, n) for x < 0 and odd n (surd(-8, 3) = -2); a negative n gives the reciprocal.  Undefined for n = 0, for x < 0 with even n, and for x = 0 with n < 0.  SymPy real_root, Wolfram Surd; the rootn operator of SimpliPy.")
  (defined (and (!= n 0) (or (>= x 0) (odd n)) (or (!= x 0) (> n 0))))
  (expand (piecewise ((>= x 0) (pow x (/ 1 n))) (else (- (pow (- x) (/ 1 n))))))
  (translate
    (sympy   "real_root({x}, {n})")
    (wolfram "Surd[{x}, {n}]")))

Trigonometric

cos(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.cos (z : ℂ) : ℂ := (AE.exp (AE.i * z) + AE.exp (-(AE.i * z))) * AE.inv 2
def AE.cos.D (z : ℂ) : Prop := True
definition
(exp(i·z) + exp(−i·z))/2
no condition of its own: wherever its definition is defined
systemtranslation check
SymPycos({z})
WolframCos[{z}]
Maximacos({z})
Source (spec/functions/cos.sexp)
(defun cos ((z complex)) complex
  (expand (/ (+ (exp (* i z)) (exp (- (* i z)))) 2))
  (translate
    (sympy   "cos({z})")
    (wolfram "Cos[{z}]")
    (maxima  "cos({z})")))

sin(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.sin (z : ℂ) : ℂ := (AE.exp (AE.i * z) - AE.exp (-(AE.i * z))) * AE.inv (2 * AE.i)
def AE.sin.D (z : ℂ) : Prop := 2 * AE.i ≠ 0
definition
(exp(i·z) − exp(−i·z))/(2i)
no condition of its own: wherever its definition is defined
systemtranslation check
SymPysin({z})
WolframSin[{z}]
Maximasin({z})
Source (spec/functions/sin.sexp)
(defun sin ((z complex)) complex
  (expand (/ (- (exp (* i z)) (exp (- (* i z)))) (* 2 i)))
  (translate
    (sympy   "sin({z})")
    (wolfram "Sin[{z}]")
    (maxima  "sin({z})")))

tan(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.tan (z : ℂ) : ℂ := AE.sin z * AE.inv (AE.cos z)
def AE.tan.D (z : ℂ) : Prop := AE.cos.D z ∧ AE.cos z ≠ 0 ∧ AE.sin.D z ∧ AE.cos.D z ∧ AE.cos z ≠ 0
definition
sin(z)/cos(z)
cos(z) ≠ 0
systemtranslation check
SymPytan({z})
WolframTan[{z}]
Maximatan({z})
Source (spec/functions/tan.sexp)
(defun tan ((z complex)) complex
  (defined (!= (cos z) 0))
  (expand (/ (sin z) (cos z)))
  (translate
    (sympy   "tan({z})")
    (wolfram "Tan[{z}]")
    (maxima  "tan({z})")))

Inverse trigonometric

acos(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.acos (z : ℂ) : ℂ := AE.pi * AE.inv 2 - AE.asin z
def AE.acos.D (z : ℂ) : Prop := AE.asin.D z
definition
π/2 − asin(z)
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyacos({z})
WolframArcCos[{z}]
Source (spec/functions/acos.sexp)
(defun acos ((z complex)) complex
  (expand (- (/ pi 2) (asin z)))
  (translate
    (sympy   "acos({z})")
    (wolfram "ArcCos[{z}]")))

acot(z: complex) → complex

Inverse cotangent.

Lean (spec/generated/All.lean, )
inductive AE.acot.Variant | dlmf | continuous
def AE.acot : AE.acot.Variant → ℂ → ℂ
  | .dlmf, z => AE.atan (1 * AE.inv z)
  | .continuous, z => AE.pi * AE.inv 2 - AE.atan z
def AE.acot.D : AE.acot.Variant → ℂ → Prop
  | .dlmf, z => z ≠ 0 ∧ AE.atan.D (1 * AE.inv z)
  | .continuous, z => AE.atan.D z
dlmfatan(1/z)
continuousπ/2 − atan(z)
conventions differ; where they disagree, no case depends on the value
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyacot({z})
WolframArcCot[{z}]
Source (spec/functions/acot.sexp)
(defun acot ((z complex)) complex
  (doc "Inverse cotangent."
       "Convention-dependent: DLMF atan(1/z) vs. the real-continuous pi/2 - atan(z).  They differ e.g. on the negative reals, so no case depends on the value there.")
  (variants
    (dlmf       (atan (/ 1 z)))
    (continuous (- (/ pi 2) (atan z))))
  (translate
    (sympy   "acot({z})")
    (wolfram "ArcCot[{z}]")))

asin(z: complex) → complex

Principal arcsine.

Lean (spec/generated/All.lean, )
def AE.asin (z : ℂ) : ℂ := (-AE.i) * AE.log (AE.i * z + AE.sqrt (1 - z * z))
def AE.asin.D (z : ℂ) : Prop := AE.sqrt.D (1 - z * z) ∧ AE.i * z + AE.sqrt (1 - z * z) ≠ 0
definition
−i·log(i·z + √(1 − z·z))
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyasin({z})
WolframArcSin[{z}]
Source (spec/functions/asin.sexp)
(defun asin ((z complex)) complex
  (doc "Principal arcsine."
       "DLMF 4.23.19.")
  (expand (* (- i) (log (+ (* i z) (sqrt (- 1 (* z z)))))))
  (translate
    (sympy   "asin({z})")
    (wolfram "ArcSin[{z}]")))

atan(z: complex) → complex

Principal arctangent.

Lean (spec/generated/All.lean, )
def AE.atan (z : ℂ) : ℂ := AE.i * AE.inv 2 * (AE.log (1 - AE.i * z) - AE.log (1 + AE.i * z))
def AE.atan.D (z : ℂ) : Prop := (z ≠ AE.i ∧ z ≠ -AE.i) ∧ 1 - AE.i * z ≠ 0 ∧ 1 + AE.i * z ≠ 0
definition
(i/2)·(log(1 − i·z) − log(1 + i·z))
z ≠ i and z ≠ −i
systemtranslation check
SymPyatan({z})
WolframArcTan[{z}]
Maximaatan({z})
Source (spec/functions/atan.sexp)
(defun atan ((z complex)) complex
  (doc "Principal arctangent."
       "On the branch cuts (imaginary axis, |im z| > 1) the value is the formula's: continuous from the right half plane on the upper cut (im z > 1) and from the left half plane on the lower cut (im z < -1), e.g. atan(2i) = pi/2 + 0.5493i, atan(-2i) = -pi/2 - 0.5493i.  SymPy 1.14, mpmath 1.3 and Wolfram 14.3 all agree with this.")
  (defined (and (!= z i) (!= z (- i))))
  (expand (* (/ i 2) (- (log (- 1 (* i z))) (log (+ 1 (* i z))))))
  (translate
    (sympy   "atan({z})")
    (wolfram "ArcTan[{z}]")
    (maxima  "atan({z})")))

atan2(y: real, x: real) → real

Angle of the point (x, y), in (-pi, pi].

Lean (spec/generated/All.lean, )
def AE.atan2 (y x : ℂ) : ℂ := AE.im (AE.log (x + AE.i * y))
def AE.atan2.D (y x : ℂ) : Prop := AE.IsReal y ∧ AE.IsReal x ∧ ¬(x = 0 ∧ y = 0) ∧ x + AE.i * y ≠ 0
definition
Im(log(x + i·y))
x ≠ 0 or y ≠ 0
systemtranslation check
SymPyatan2({y}, {x})
WolframArcTan[{x}, {y}]
Maximaatan2({y}, {x})
Source (spec/functions/atan2.sexp)
(defun atan2 ((y real) (x real)) real
  (doc "Angle of the point (x, y), in (-pi, pi]."
       "Argument order: y first, as SymPy's atan2(y, x); Wolfram's is ArcTan[x, y].")
  (defined (not (and (= x 0) (= y 0))))
  (expand (im (log (+ x (* i y)))))
  (translate
    (sympy   "atan2({y}, {x})")
    (wolfram "ArcTan[{x}, {y}]")
    (maxima  "atan2({y}, {x})")))

Hyperbolic & inverse hyperbolic

acosh(z: complex) → complex

Principal inverse hyperbolic cosine.

Lean (spec/generated/All.lean, )
def AE.acosh (z : ℂ) : ℂ := AE.log (z + AE.sqrt (z + 1) * AE.sqrt (z - 1))
def AE.acosh.D (z : ℂ) : Prop :=
  (AE.sqrt.D (z + 1) ∧ AE.sqrt.D (z - 1)) ∧ z + AE.sqrt (z + 1) * AE.sqrt (z - 1) ≠ 0
definition
log(z + √(z + 1)·√(z − 1))
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyacosh({z})
WolframArcCosh[{z}]
Source (spec/functions/acosh.sexp)
(defun acosh ((z complex)) complex
  (doc "Principal inverse hyperbolic cosine."
       "DLMF 4.37.19, log(z + sqrt(z + 1) sqrt(z - 1)); branch cut (-inf, 1].  Agrees with SymPy acosh and Wolfram ArcCosh.")
  (expand (log (+ z (* (sqrt (+ z 1)) (sqrt (- z 1))))))
  (translate
    (sympy   "acosh({z})")
    (wolfram "ArcCosh[{z}]")))

asinh(z: complex) → complex

Principal inverse hyperbolic sine.

Lean (spec/generated/All.lean, )
def AE.asinh (z : ℂ) : ℂ :=
  if AE.ge (AE.re z) 0 then AE.log (z + AE.sqrt (z * z + 1))
  else -(AE.log ((-z) + AE.sqrt (z * z + 1)))
def AE.asinh.D (z : ℂ) : Prop :=
  (AE.ge (AE.re z) 0 → AE.sqrt.D (z * z + 1) ∧ z + AE.sqrt (z * z + 1) ≠ 0) ∧
  (¬AE.ge (AE.re z) 0 → AE.sqrt.D (z * z + 1) ∧ (-z) + AE.sqrt (z * z + 1) ≠ 0)
definition
log(z + √(z·z + 1))if Re(z) ≥ 0
−log(−z + √(z·z + 1))otherwise
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyasinh({z})
WolframArcSinh[{z}]
Source (spec/functions/asinh.sexp)
(defun asinh ((z complex)) complex
  (doc "Principal inverse hyperbolic sine."
       "DLMF 4.37.16, log(z + sqrt(z^2 + 1)); branch cuts on the imaginary axis, |im z| > 1.  That formula is odd in z everywhere, cuts included, so it is written as -asinh(-z) on re z < 0, which is the same function but avoids cancellation in numerics.  Agrees with SymPy asinh and Wolfram ArcSinh.")
  (expand (piecewise
            ((>= (re z) 0) (log (+ z (sqrt (+ (* z z) 1)))))
            (else (- (log (+ (- z) (sqrt (+ (* z z) 1))))))))
  (translate
    (sympy   "asinh({z})")
    (wolfram "ArcSinh[{z}]")))

atanh(z: complex) → complex

Principal inverse hyperbolic tangent.

Lean (spec/generated/All.lean, )
def AE.atanh (z : ℂ) : ℂ := (AE.log (1 + z) - AE.log (1 - z)) * AE.inv 2
def AE.atanh.D (z : ℂ) : Prop := (z ≠ 1 ∧ z ≠ -1) ∧ 1 + z ≠ 0 ∧ 1 - z ≠ 0
definition
(log(1 + z) − log(1 − z))/2
z ≠ 1 and z ≠ −1
systemtranslation check
SymPyatanh({z})
WolframArcTanh[{z}]
Source (spec/functions/atanh.sexp)
(defun atanh ((z complex)) complex
  (doc "Principal inverse hyperbolic tangent."
       "DLMF 4.37.24 with principal logs, (log(1 + z) - log(1 - z))/2; branch cuts (-inf, -1] and [1, inf), on which this form is the SymPy atanh value.  Undefined at z = 1 and z = -1.")
  (defined (and (!= z 1) (!= z -1)))
  (expand (/ (- (log (+ 1 z)) (log (- 1 z))) 2))
  (translate
    (sympy   "atanh({z})")
    (wolfram "ArcTanh[{z}]")))

cosh(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.cosh (z : ℂ) : ℂ := (AE.exp z + AE.exp (-z)) * AE.inv 2
def AE.cosh.D (z : ℂ) : Prop := True
definition
(exp(z) + exp(−z))/2
no condition of its own: wherever its definition is defined
systemtranslation check
SymPycosh({z})
WolframCosh[{z}]
Source (spec/functions/cosh.sexp)
(defun cosh ((z complex)) complex
  (expand (/ (+ (exp z) (exp (- z))) 2))
  (translate
    (sympy   "cosh({z})")
    (wolfram "Cosh[{z}]")))

sinh(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.sinh (z : ℂ) : ℂ := (AE.exp z - AE.exp (-z)) * AE.inv 2
def AE.sinh.D (z : ℂ) : Prop := True
definition
(exp(z) − exp(−z))/2
no condition of its own: wherever its definition is defined
systemtranslation check
SymPysinh({z})
WolframSinh[{z}]
Source (spec/functions/sinh.sexp)
(defun sinh ((z complex)) complex
  (expand (/ (- (exp z) (exp (- z))) 2))
  (translate
    (sympy   "sinh({z})")
    (wolfram "Sinh[{z}]")))

tanh(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.tanh (z : ℂ) : ℂ := AE.sinh z * AE.inv (AE.cosh z)
def AE.tanh.D (z : ℂ) : Prop :=
  AE.cosh.D z ∧ AE.cosh z ≠ 0 ∧ AE.sinh.D z ∧ AE.cosh.D z ∧ AE.cosh z ≠ 0
definition
sinh(z)/cosh(z)
cosh(z) ≠ 0
systemtranslation check
SymPytanh({z})
WolframTanh[{z}]
Source (spec/functions/tanh.sexp)
(defun tanh ((z complex)) complex
  (defined (!= (cosh z) 0))
  (expand (/ (sinh z) (cosh z)))
  (translate
    (sympy   "tanh({z})")
    (wolfram "Tanh[{z}]")))

Rounding, sign & absolute value

abs(z: complex) → real

Lean (spec/generated/All.lean, )
def AE.abs (z : ℂ) : ℂ := AE.sqrt (z * AE.conj z)
def AE.abs.D (z : ℂ) : Prop := AE.sqrt.D (z * AE.conj z)
definition
√(z·conj(z))
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyAbs({z})
WolframAbs[{z}]
Maximaabs({z})
Source (spec/functions/abs.sexp)
(defun abs ((z complex)) real
  (expand (sqrt (* z (conj z))))
  (translate
    (sympy   "Abs({z})")
    (wolfram "Abs[{z}]")
    (maxima  "abs({z})")))

ceiling(x: real) → real

Lean (spec/generated/All.lean, )
def AE.ceiling (x : ℂ) : ℂ := -(AE.floor (-x))
def AE.ceiling.D (x : ℂ) : Prop := AE.IsReal x ∧ AE.IsReal (-x)
definition
−⌊−x⌋
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyceiling({x})
WolframCeiling[{x}]
Source (spec/functions/ceiling.sexp)
(defun ceiling ((x real)) real
  (expand (- (floor (- x))))
  (translate
    (sympy   "ceiling({x})")
    (wolfram "Ceiling[{x}]")))

heaviside(x: real) → real

Unit step.

Lean (spec/generated/All.lean, )
inductive AE.heaviside.Variant | zero | half | one | undefined_at_0
def AE.heaviside : AE.heaviside.Variant → ℂ → ℂ
  | .zero, x => if AE.gt x 0 then 1 else 0
  | .half, x => if AE.gt x 0 then 1 else if x = 0 then 1 / 2 else 0
  | .one, x => if AE.ge x 0 then 1 else 0
  | .undefined_at_0, x => if AE.gt x 0 then 1 else if AE.lt x 0 then 0 else AE.undef
def AE.heaviside.D : AE.heaviside.Variant → ℂ → Prop
  | .zero, x => AE.IsReal x
  | .half, x => AE.IsReal x
  | .one, x => AE.IsReal x
  | .undefined_at_0, x =>
      AE.IsReal x ∧ AE.IsReal x ∧ (¬AE.gt x 0 → AE.IsReal x ∧ (¬AE.lt x 0 → False))
zero
1if x > 0
0otherwise
half
1if x > 0
1/2if x = 0
0otherwise
one
1if x ≥ 0
0otherwise
undefined-at-0
1if x > 0
0if x < 0
conventions differ; where they disagree, no case depends on the value
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyHeaviside({x})
WolframHeavisideTheta[{x}]
Source (spec/functions/heaviside.sexp)
(defun heaviside ((x real)) real
  (doc "Unit step."
       "The value at 0 is convention-dependent (the variants), so no case depends on it.")
  (variants
    (zero         (piecewise ((> x 0) 1) (else 0)))
    (half         (piecewise ((> x 0) 1) ((= x 0) 1/2) (else 0)))
    (one          (piecewise ((>= x 0) 1) (else 0)))
    (undefined-at-0 (piecewise ((> x 0) 1) ((< x 0) 0))))
  (translate
    (sympy   "Heaviside({x})")
    (wolfram "HeavisideTheta[{x}]")))

max(a: real, b: real) → real

Lean (spec/generated/All.lean, )
def AE.max (a b : ℂ) : ℂ := if AE.ge a b then a else b
def AE.max.D (a b : ℂ) : Prop := AE.IsReal a ∧ AE.IsReal b ∧ AE.IsReal a ∧ AE.IsReal b
definition
aif a ≥ b
botherwise
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyMax({a}, {b})
WolframMax[{a}, {b}]
Source (spec/functions/max.sexp)
(defun max ((a real) (b real)) real
  (expand (piecewise ((>= a b) a) (else b)))
  (translate
    (sympy   "Max({a}, {b})")
    (wolfram "Max[{a}, {b}]")))

min(a: real, b: real) → real

Lean (spec/generated/All.lean, )
def AE.min (a b : ℂ) : ℂ := if AE.le a b then a else b
def AE.min.D (a b : ℂ) : Prop := AE.IsReal a ∧ AE.IsReal b ∧ AE.IsReal a ∧ AE.IsReal b
definition
aif a ≤ b
botherwise
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyMin({a}, {b})
WolframMin[{a}, {b}]
Source (spec/functions/min.sexp)
(defun min ((a real) (b real)) real
  (expand (piecewise ((<= a b) a) (else b)))
  (translate
    (sympy   "Min({a}, {b})")
    (wolfram "Min[{a}, {b}]")))

sign(z: complex) → complex

Complex sign: z/|z|, sign(0) = 0.

Lean (spec/generated/All.lean, )
def AE.sign (z : ℂ) : ℂ := if z = 0 then 0 else z * AE.inv (AE.abs z)
def AE.sign.D (z : ℂ) : Prop := ¬z = 0 → AE.abs.D z ∧ AE.abs z ≠ 0
definition
0if z = 0
z/|z|otherwise
no condition of its own: wherever its definition is defined
systemtranslation check
SymPysign({z})
WolframSign[{z}]
Source (spec/functions/sign.sexp)
(defun sign ((z complex)) complex
  (doc "Complex sign: z/|z|, sign(0) = 0.")
  (expand (piecewise ((= z 0) 0) (else (/ z (abs z)))))
  (translate
    (sympy   "sign({z})")
    (wolfram "Sign[{z}]")))

Other

gamma(z: complex) → complex

Lean (spec/generated/All.lean, )
def AE.gamma (z : ℂ) : ℂ := Complex.Gamma z
def AE.gamma.D (z : ℂ) : Prop := AE.integer.D z ∧ ¬(AE.integer z ∧ AE.le (AE.re z) 0)
Lean Complex.Gamma; numerics mpmath gamma
z ∉ ℤ or Re(z) > 0
systemtranslation check
SymPygamma({z})
WolframGamma[{z}]
Source (spec/functions/gamma.sexp)
(primitive gamma ((z complex)) complex
  (defined (not (and (integer z) (<= (re z) 0))))
  (lean "Complex.Gamma")
  (mpmath "gamma")
  (translate
    (sympy   "gamma({z})")
    (wolfram "Gamma[{z}]")))

Predicates

composite(x: complex) → bool

x is an integer > 1 that is not prime.

Lean (spec/generated/All.lean, )
def AE.composite (x : ℂ) : Prop := AE.integer x ∧ AE.gt (AE.re x) 1 ∧ ¬AE.prime x
def AE.composite.D (x : ℂ) : Prop :=
  AE.integer.D x ∧ (AE.integer x → AE.gt (AE.re x) 1 → AE.prime.D x)
definition
x ∈ ℤ and Re(x) > 1 and x is not prime
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.composite({x})
Wolfram(Element[{x}, Integers] && {x} > 1 && !Element[{x}, Primes])
Source (spec/functions/composite.sexp)
(defun composite ((x complex)) bool
  (doc "x is an integer > 1 that is not prime.")
  (expand (and (integer x) (> (re x) 1) (not (prime x))))
  (translate
    (sympy   "Q.composite({x})")
    (wolfram "(Element[{x}, Integers] && {x} > 1 && !Element[{x}, Primes])")))

even(x: complex) → bool

x is an even integer: x = 2k for some integer k.

Lean (spec/generated/All.lean, )
def AE.even (x : ℂ) : Prop := AE.integer (x * AE.inv 2)
def AE.even.D (x : ℂ) : Prop := AE.integer.D (x * AE.inv 2)
definition
x/2 ∈ ℤ
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.even({x})
WolframElement[({x})/2, Integers]
Source (spec/functions/even.sexp)
(defun even ((x complex)) bool
  (doc "x is an even integer: x = 2k for some integer k."
       "Wolfram's EvenQ is syntactic (EvenQ[n] is False for a symbol), so it is NOT the translation.")
  (expand (integer (/ x 2)))
  (translate
    (sympy   "Q.even({x})")
    (wolfram "Element[({x})/2, Integers]")))

imaginary(x: complex) → bool

x = k i for a real k != 0 (0 is not imaginary).

Lean (spec/generated/All.lean, )
def AE.imaginary (x : ℂ) : Prop := AE.re x = 0 ∧ x ≠ 0
def AE.imaginary.D (x : ℂ) : Prop := True
definition
Re(x) = 0 and x ≠ 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.imaginary({x})
Wolfram(Re[{x}] == 0 && {x} != 0)
Source (spec/functions/imaginary.sexp)
(defun imaginary ((x complex)) bool
  (doc "x = k i for a real k != 0 (0 is not imaginary).")
  (expand (and (= (re x) 0) (!= x 0)))
  (translate
    (sympy   "Q.imaginary({x})")
    (wolfram "(Re[{x}] == 0 && {x} != 0)")))

integer(x: complex) → bool

Lean (spec/generated/All.lean, )
def AE.integer (x : ℂ) : Prop := AE.real x ∧ AE.re x = AE.floor (AE.re x)
def AE.integer.D (x : ℂ) : Prop := AE.real.D x
definition
x ∈ ℝ and Re(x) = ⌊Re(x)⌋
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.integer({x})
WolframElement[{x}, Integers]
Source (spec/functions/integer.sexp)
(defun integer ((x complex)) bool
  (expand (and (real x) (= (re x) (floor (re x)))))
  (translate
    (sympy   "Q.integer({x})")
    (wolfram "Element[{x}, Integers]")))

irrational(x: complex) → bool

Lean (spec/generated/All.lean, )
def AE.irrational (x : ℂ) : Prop := AE.real x ∧ ¬AE.rational x
def AE.irrational.D (x : ℂ) : Prop := AE.real.D x ∧ (AE.real x → AE.rational.D x)
definition
x ∈ ℝ and x ∉ ℚ
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.irrational({x})
Wolfram(Element[{x}, Reals] && !Element[{x}, Rationals])
Source (spec/functions/irrational.sexp)
(defun irrational ((x complex)) bool
  (expand (and (real x) (not (rational x))))
  (translate
    (sympy   "Q.irrational({x})")
    (wolfram "(Element[{x}, Reals] && !Element[{x}, Rationals])")))

negative(x: complex) → bool

x is real and < 0.

Lean (spec/generated/All.lean, )
def AE.negative (x : ℂ) : Prop := AE.real x ∧ AE.lt (AE.re x) 0
def AE.negative.D (x : ℂ) : Prop := AE.real.D x
definition
x ∈ ℝ and Re(x) < 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.negative({x})
Wolfram(Element[{x}, Reals] && {x} < 0)
Source (spec/functions/negative.sexp)
(defun negative ((x complex)) bool
  (doc "x is real and < 0.")
  (expand (and (real x) (< (re x) 0)))
  (translate
    (sympy   "Q.negative({x})")
    (wolfram "(Element[{x}, Reals] && {x} < 0)")))

nonnegative(x: complex) → bool

x is real and >= 0.

Lean (spec/generated/All.lean, )
def AE.nonnegative (x : ℂ) : Prop := AE.real x ∧ AE.ge (AE.re x) 0
def AE.nonnegative.D (x : ℂ) : Prop := AE.real.D x
definition
x ∈ ℝ and Re(x) ≥ 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.nonnegative({x})
Wolfram(Element[{x}, Reals] && {x} >= 0)
Source (spec/functions/nonnegative.sexp)
(defun nonnegative ((x complex)) bool
  (doc "x is real and >= 0.")
  (expand (and (real x) (>= (re x) 0)))
  (translate
    (sympy   "Q.nonnegative({x})")
    (wolfram "(Element[{x}, Reals] && {x} >= 0)")))

nonpositive(x: complex) → bool

x is real and <= 0.

Lean (spec/generated/All.lean, )
def AE.nonpositive (x : ℂ) : Prop := AE.real x ∧ AE.le (AE.re x) 0
def AE.nonpositive.D (x : ℂ) : Prop := AE.real.D x
definition
x ∈ ℝ and Re(x) ≤ 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.nonpositive({x})
Wolfram(Element[{x}, Reals] && {x} <= 0)
Source (spec/functions/nonpositive.sexp)
(defun nonpositive ((x complex)) bool
  (doc "x is real and <= 0.")
  (expand (and (real x) (<= (re x) 0)))
  (translate
    (sympy   "Q.nonpositive({x})")
    (wolfram "(Element[{x}, Reals] && {x} <= 0)")))

nonzero(x: complex) → bool

x != 0 (x may be non-real).

Lean (spec/generated/All.lean, )
def AE.nonzero (x : ℂ) : Prop := x ≠ 0
def AE.nonzero.D (x : ℂ) : Prop := True
definition
x ≠ 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPy(~Q.zero({x}))
Wolfram({x} != 0)
Source (spec/functions/nonzero.sexp)
(defun nonzero ((x complex)) bool
  (doc "x != 0 (x may be non-real)."
       "SymPy's Q.nonzero means 'real and nonzero', so it is NOT the translation.")
  (expand (!= x 0))
  (translate
    (sympy   "(~Q.zero({x}))")
    (wolfram "({x} != 0)")))

odd(x: complex) → bool

x is an odd integer: x = 2k + 1 for some integer k.

Lean (spec/generated/All.lean, )
def AE.odd (x : ℂ) : Prop := AE.integer ((x - 1) * AE.inv 2)
def AE.odd.D (x : ℂ) : Prop := AE.integer.D ((x - 1) * AE.inv 2)
definition
(x − 1)/2 ∈ ℤ
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.odd({x})
WolframElement[(({x}) - 1)/2, Integers]
Source (spec/functions/odd.sexp)
(defun odd ((x complex)) bool
  (doc "x is an odd integer: x = 2k + 1 for some integer k."
       "Not OddQ (syntactic).")
  (expand (integer (/ (- x 1) 2)))
  (translate
    (sympy   "Q.odd({x})")
    (wolfram "Element[(({x}) - 1)/2, Integers]")))

positive(x: complex) → bool

x is real and > 0.

Lean (spec/generated/All.lean, )
def AE.positive (x : ℂ) : Prop := AE.real x ∧ AE.gt (AE.re x) 0
def AE.positive.D (x : ℂ) : Prop := AE.real.D x
definition
x ∈ ℝ and Re(x) > 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.positive({x})
Wolfram(Element[{x}, Reals] && {x} > 0)
Source (spec/functions/positive.sexp)
(defun positive ((x complex)) bool
  (doc "x is real and > 0.")
  (expand (and (real x) (> (re x) 0)))
  (translate
    (sympy   "Q.positive({x})")
    (wolfram "(Element[{x}, Reals] && {x} > 0)")))

prime(x: complex) → bool

x is a (positive) prime integer.

Lean (spec/generated/All.lean, )
def AE.prime (x : ℂ) : Prop := (fun x : ℂ => ∃ n : ℕ, Nat.Prime n ∧ x = (n : ℂ)) x
def AE.prime.D (x : ℂ) : Prop := True
Lean (fun x : ℂ => ∃ n : ℕ, Nat.Prime n ∧ x = (n : ℂ)); numerics python is_prime
everywhere on its parameter types
systemtranslation check
SymPyQ.prime({x})
WolframElement[{x}, Primes]
Source (spec/functions/prime.sexp)
(primitive prime ((x complex)) bool
  (doc "x is a (positive) prime integer."
       "Not PrimeQ (syntactic).")
  (lean "(fun x : ℂ => ∃ n : ℕ, Nat.Prime n ∧ x = (n : ℂ))")
  (python "is_prime")
  (translate
    (sympy   "Q.prime({x})")
    (wolfram "Element[{x}, Primes]")))

rational(x: complex) → bool

x is a rational number.

Lean (spec/generated/All.lean, )
def AE.rational (x : ℂ) : Prop := (fun x : ℂ => ∃ q : ℚ, x = (q : ℂ)) x
def AE.rational.D (x : ℂ) : Prop := True
Lean (fun x : ℂ => ∃ q : ℚ, x = (q : ℂ)); numerics python is_rational
everywhere on its parameter types
systemtranslation check
SymPyQ.rational({x})
WolframElement[{x}, Rationals]
Source (spec/functions/rational.sexp)
(primitive rational ((x complex)) bool
  (doc "x is a rational number."
       "Numerically checked heuristically (within 1e-28 of a fraction with denominator <= 10^6).")
  (lean "(fun x : ℂ => ∃ q : ℚ, x = (q : ℂ))")
  (python "is_rational")
  (translate
    (sympy   "Q.rational({x})")
    (wolfram "Element[{x}, Rationals]")))

real(x: complex) → bool

x is a real number (imaginary part zero).

Lean (spec/generated/All.lean, )
def AE.real (x : ℂ) : Prop := AE.im x = 0
def AE.real.D (x : ℂ) : Prop := True
definition
Im(x) = 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.real({x})
WolframElement[{x}, Reals]
Source (spec/functions/real.sexp)
(defun real ((x complex)) bool
  (doc "x is a real number (imaginary part zero).")
  (expand (= (im x) 0))
  (translate
    (sympy   "Q.real({x})")
    (wolfram "Element[{x}, Reals]")))

zero(x: complex) → bool

Lean (spec/generated/All.lean, )
def AE.zero (x : ℂ) : Prop := x = 0
def AE.zero.D (x : ℂ) : Prop := True
definition
x = 0
no condition of its own: wherever its definition is defined
systemtranslation check
SymPyQ.zero({x})
Wolfram({x} == 0)
Source (spec/functions/zero.sexp)
(defun zero ((x complex)) bool
  (expand (= x 0))
  (translate
    (sympy   "Q.zero({x})")
    (wolfram "({x} == 0)")))

Extensions (ext/)

ext/demo/sinc(x: real) → real

Unnormalised sinc: sin(x)/x, sinc(0) = 1.

Lean (spec/generated/All.lean, )
def AE.ext.demo.sinc (x : ℂ) : ℂ := if x = 0 then 1 else AE.sin x * AE.inv x
def AE.ext.demo.sinc.D (x : ℂ) : Prop := AE.IsReal x ∧ (¬x = 0 → AE.sin.D x ∧ x ≠ 0)
definition
1if x = 0
sin(x)/xotherwise
no condition of its own: wherever its definition is defined
systemtranslation check
WolframSinc[{x}]
Source (spec/functions/ext/demo/sinc.sexp)
; Example of a namespaced extension entry.  Extensions are UNOFFICIAL: cases
; using them are graded but off by default in every report.  Deliberately has
; no SymPy translation, so such cases are reported "unsupported" for SymPy.
(defun ext/demo/sinc ((x real)) real
  (doc "Unnormalised sinc: sin(x)/x, sinc(0) = 1.")
  (expand (piecewise ((= x 0) 1) (else (/ (sin x) x))))
  (translate
    (wolfram "Sinc[{x}]")))

Translation checks

A system receives each library function as its own native function. translation-check asks every CAS to evaluate those translations at exact points and compares with the spec.

What is compared

Each function at and , the cases ; at 40 digits and problems . Lean and the numeric checker agree , except for the parts . .

Every point gets one verdict:

Results per function

The latest run per function and CAS (tmp/translation-check/<cas>.json); hover a badge for the breakdown, click it for every point. “not run” is not the same as checked and fine. No result at all for SymPy, Wolfram: the Wolfram check has to run where a Wolfram kernel is (the eval host), and has not been run yet.

functionSymPyWolfram
Powers & roots
pow
sqrt
surd
Trigonometric
cos
sin
tan
Inverse trigonometric
acos
acot
asin
atan
atan2
Hyperbolic & inverse hyperbolic
acosh
asinh
atanh
cosh
sinh
tanh
Rounding, sign & absolute value
abs
ceiling
heaviside
max
min
sign
Other
gamma
Predicates
composite
even
imaginary
integer
irrational
negative
nonnegative
nonpositive
nonzero
odd
positive
prime
rational
real
zero
Extensions (ext/)
ext/demo/sincno translation

End to end over cases

Totals only.

  • SymPy: not run
  • Wolfram: not run