Paste Lean 4 / Mathlib-flavored code — a theorem, lemma,
def, or just a bare expression. leanmath reads its shape the way a
math-literate human skims Lean, and renders it back as ordinary notation: quantifiers,
hypotheses laid out plainly, and a copyable LaTeX formula underneath.
This is a best-effort translator, not a Lean parser — it pattern-matches common syntax
(binders, quantifiers, logical connectives, arithmetic, sqrt/abs,
Nat/Real/…) and juxtaposition-as-application (f x y
→ f(x, y)). A multi-step by proof also gets split into a "proof
sketch" list, one tactic call per line. Custom notation and anything
elaboration-dependent still won't be understood — it just renders the text it can see.
Always sanity-check the output against the source.