Compendium

Mathematical / Proof Notation Languages Family Index

16 min read

Mathematical / Proof Notation Languages Family Index

type: language-family-index family: math-notation languages_catalogued: 26 tags: [language-reference, family-index, math-notation, latex, mathml, asciimath, wolfram, openmath, typst, tikz, apl, iverson]

Mathematical / Proof Notation — Family Index

Family overview

This family is the set of encodings people use to put mathematics into a computer. Not the proof-tactic DSLs of Coq/Lean/Isabelle (those live in notation-spec) and not the general document-typesetting engines (those live in document-typesetting) — this index narrows on the math layer specifically: how you write a fraction, an integral, a commutative diagram, or a mathematical object so that a renderer or computer-algebra system can act on it. The two parents of the field are Donald Knuth’s TeX math mode (1978, born from his frustration with the Volume 2 galleys of The Art of Computer Programming) and the AMS-LaTeX macro layer (American Mathematical Society, 1990 — amsmath, amssymb, amsthm) which made journal-grade mathematics writable as logical markup. Every modern math-rendering pipeline — MathJax, KaTeX, Pandoc, Quarto, Jupyter, arXiv, Wikipedia — still treats LaTeX-flavored math as the lingua franca, including pipelines whose published output is HTML+MathML.

The parallel MathML lineage (W3C Math Working Group, 1998 first Recommendation; MathML 3.0 in 2010; MathML 4.0 still on the Recommendation track in 2026 with MathML Core advancing to CR — see W3C charter and mathml-core editor’s draft) was designed to give the web semantic mathematics with the same first-class structural representation HTML gives prose. In practice MathML 1–3 lost the rendering war to MathJax (Davide Cervone, Volker Sorge — v4.1.2 as of May 2026) and KaTeX (Khan Academy, 2014; v0.16.x stable in 2026), both of which accept LaTeX-ish source and emit (variously) HTML+CSS, SVG, or MathML output. The 2023 enabling of MathML Core in Chromium (joining Firefox and WebKit) finally made native browser MathML practical without polyfills, but the authoring layer in 2026 is still overwhelmingly LaTeX-flavored, with MathML acting as a transport and accessibility format more than an authoring one.

A deep design split runs through the family: presentation (how should the math look?) versus content / semantic (what does the math mean?). Presentation MathML, AsciiMath, TeX/LaTeX math, and Typst math are all presentation-layer. Content MathML, OpenMath (with its Content Dictionaries), and OMDoc (Kohlhase, KWARC, 1998+) are content-layer — they encode “this is the function sin applied to the variable x” rather than “place a sin glyph followed by an italic x.” Content forms are what you want for cross-system interchange (e.g. exporting from Mathematica into Maple, or from a theorem prover library into a Wikipedia article) but are too verbose for ordinary writing. The MMT format (Kohlhase et al.) extended OMDoc with formal foundations and is the reference implementation for active mathematical-knowledge management research.

A third tradition treats math notation as the programming language itself: APL (Iverson, 1962, full glyph alphabet from ⍳⍴⍒⌽⌹⍤), J (Iverson, 1990, ASCII-only successor), K/Q/kdb+ (Whitney, 1993+), and the Wolfram Language with its three-form authoring system (InputForm, StandardForm, FullForm — InputForm parses ASCII keyboard text, StandardForm renders 2D math typography in the front-end, FullForm exposes the underlying f[x, y] term tree). Iverson’s 1979 Turing-lecture paper “Notation as a Tool of Thought” (Comm. ACM, August 1980) is the manifesto. The lineage has produced more vocabulary than mainstream code (J, K, Q are now financial-quant standards; APL itself survives at Dyalog) but it remains the only family in the index where the mathematical notation is the executable program. Finally, the diagram-notation subfamily — TikZ + tikz-cd (Stefan Kottwitz, Felix Kuran et al.; tikz-cd by Florêncio Neves, currently maintained by the LaTeX community), xy-pic (Kristoffer Rose, 1991), and CD-LaTeX — encodes commutative diagrams and category-theory arrows that simple linear math notation cannot express. And Typst (Martin Haug & Laurenz Mädje, TU Berlin, 2023; v0.13 series in 2026) is the current credible challenger to TeX’s 48-year monopoly: cleaner math syntax (x_i reads as a subscript without entering math mode, mat(1, 2; 3, 4) defines a matrix, function calls replace macros, and incremental compilation makes errors tractable).

In our deep library

None of these notations have standalone deep-library notes — they are markup or interchange formats more than general-purpose programming languages. Cross-reference:

  • document-typesetting — overlaps on TeX, LaTeX, ConTeXt, Typst, Pollen as typesetting engines. This index treats them as math input languages (i.e., the math-mode subset, AMS extensions, equation environments). Read both notes when researching either.
  • notation-spec — overlaps on Z notation, B-method, VDM-SL, BNF/EBNF as specification / verification languages. This index covers them as mathematical notation systems (set-theoretic schema language, abstract machine notation, Backus-style grammar notation). The notation-spec note treats them as systems for proving and verifying; this note treats them as encodings of mathematical text.
  • scientific — Mathematica, Maple, MATLAB, SymPy, Maxima, GAP, SageMath are catalogued there as computer-algebra systems. Here they appear only as far as their notation surface (Wolfram Language’s three forms, Maple’s 2D math input, MATLAB Symbolic Math Toolbox’s latex() and pretty(), SymPy’s pprint()).
  • notation-spec also catalogues the proof assistants (Coq/Rocq, Lean, Agda, Idris, Isabelle/HOL) — those are theorem-prover DSLs, not raw mathematical notation, and intentionally not duplicated here.
  • esoteric — APL is sometimes listed there for its glyph alphabet; here it appears as the canonical “math notation as a programming language” entry.

Tier 3 family table

NotationFirst appearedOriginTypeStatus (2026)URL
TeX math mode1978Donald Knuth (Stanford)Macro-expanded presentation markup; $...$ and $$...$$ delimiters; box-and-glue layoutFoundational; frozen-by-design but ubiquitous via pdfTeX, XeTeX, LuaTeX engineshttps://www.tug.org/texlive/
AMS-LaTeX (amsmath, amssymb, amsthm)1990American Mathematical Society + LaTeX team (Frank Mittelbach, Rainer Schöpf, Michael Downes)LaTeX package set: aligned equations, theorem environments, blackboard-bold, fraktur, AMS symbols; maintenance moved to LaTeX Project, in TeX LiveActive; the de-facto standard for journal-quality mathematicshttps://www.ams.org/publications/authors/tex/amslatex
Presentation MathML1998 (MathML 1.0)W3C Math Working Group (Patrick Ion, Robert Miner, et al.)XML markup for the visual structure of math (<mfrac>, <msup>, <mrow>); MathML 3.0 (2010); MathML 4.0 Working Draft on Recommendation track in 2026Native browser support landed across Chromium/Firefox/WebKit (Chromium 2023); MathML Core advancing to CR; MathJax/KaTeX still dominate authoringhttps://www.w3.org/TR/mathml4/
Content MathML1998W3C Math Working GroupXML markup for the meaning of math (<apply>, <plus>, <sin>, <ci>); pairs with Presentation MathML for semantic+visual round-tripsNiche; used in computer-algebra interchange and accessibility, but rarely hand-writtenhttps://www.w3.org/TR/mathml4/chapter4.html
AsciiMath2004Peter Jipsen (Chapman University)ASCII-friendly math syntax: sum_(i=1)^n i^2 = (n(n+1)(2n+1))/6; JavaScript converts to Presentation MathML on page load; supported as a MathJax input formatActive; popular in wikis, chat, and lightweight CMS systems where LaTeX is too verbosehttps://asciimath.org/
MathJax (rendering engine)2009 (v1.0); v2 2012; v3 2019; v4.0 2025; v4.1.2 in May 2026Davide Cervone, Volker Sorge; American Mathematical Society + Design Science originJavaScript engine that consumes LaTeX, MathML, or AsciiMath input and emits HTML+CSS, SVG, or MathML output; v4 adds dark-mode support, in-line breaking, HTML-in-MathMLVery active; v4.1.2 latest as of May 2026; the dominant browser math rendererhttps://www.mathjax.org/
KaTeX (rendering engine)2014Khan Academy (Emily Eisenberg, Sophie Alpert)LaTeX-only renderer; aggressively fast (no async layout), narrower coverage than MathJax; emits HTML+CSS or MathMLActive; v0.16.x in 2026 (v0.16.25 in late 2025, v0.16.45 in npm by mid-2026); the speed-critical alternative to MathJaxhttps://katex.org/
OpenMath1996 (Bremen workshop); Standard 1.0 in 1998; Standard 2.0 in 2004 (Revision 2 in 2019)OpenMath Society (Bremen, Eindhoven, RISC Linz, Inria et al.)Structural / semantic representation of math objects via Content Dictionaries (CDs) defining symbols; XML or binary encoding; complementary to (and partly inspired) Content MathMLMaintained but niche; backbone of CAS interchange and theorem-prover content librarieshttps://openmath.org/standard/
OMDoc1998+Michael Kohlhase (KWARC, Bremen / Erlangen-Nürnberg)XML format for mathematical documents — theories, proofs, and exposition; superset of OpenMath; v1.2 (2006) is the mature release; refined into the MMT formatMaintained; active in mathematical-knowledge-management research; production use in MathHub, the LaTeXML pipeline, and ALeA learning assistanthttps://omdoc.org/
TeXmacs1999Joris van der Hoeven (Inria)WYSIWYG scientific editor with its own internal math notation tree (not TeX-based despite the name); native CAS bridges (Maxima, Sage, Pari, Macaulay2, Mathematica); v2.1.5 released March 2026 with Qt6 defaultActive; small but loyal community; preferred when interactive CAS sessions need typeset I/Ohttps://www.texmacs.org/
Typst math2023 (v0.1, TU Berlin); v0.13 series in 2026Martin Haug, Laurenz Mädje (TU Berlin)Math mode entered with single $...$; multi-letter words become commands, single letters become variables; mat(1,2;3,4), frac(a,b), function-call syntax replaces TeX macros; v0.13 added math.equation.alt for accessibility and improved class binding for shorthandsVery active; rapid academic adoption; the leading credible TeX successorhttps://typst.app/docs/reference/math/
Pollen math2014Matthew ButterickMath expressed inside Racket X-expression syntax (@$ ... $); rendered via MathJax/KaTeX or LaTeX; not a math notation per se but a host syntax that can carry itActive but niche; used in Butterick’s own books (Practical Typography, Beautiful Racket)https://docs.racket-lang.org/pollen/
Wolfram Language (InputForm / StandardForm / FullForm)1988 (Mathematica 1.0)Stephen Wolfram, Wolfram Research; Wolfram Language v14.3 in August 2025; v14 series ongoing in 2026Three notation surfaces over one term tree: InputForm (ASCII keyboard, e.g. Sin[x]^2 + Cos[x]^2), StandardForm (front-end 2D math typography), FullForm (Plus[Power[Sin[x], 2], Power[Cos[x], 2]] — the canonical S-expression-like form)Very active; v14.3 added LLMGraph, dark mode, noncommutative algebrahttps://reference.wolfram.com/language/
Maple 2D math inputearly 1990s onwardMaplesoft (originally University of Waterloo)Two notation modes: 1D Maple syntax (int(sin(x), x)) and 2D math input (palettes + keyboard shortcuts that build typeset expressions in-place)Active; Maple 2024/2025 releases ongoing; common in engineering and educationhttps://www.maplesoft.com/products/Maple/
MATLAB Symbolic Math Toolbox notation2008 (toolbox folded into MATLAB after MuPAD acquisition)MathWorks (kernel from MuPAD, originally University of Paderborn)syms x y, then ordinary MATLAB infix; render as LaTeX via latex(expr), ASCII art via pretty(expr)Active; bundled in MATLAB; widely used in engineering courseworkhttps://www.mathworks.com/products/symbolic.html
SymPy pretty-print2007 (SymPy 0.4)SymPy contributors (originally Ondřej Čertík)Three output forms: srepr (full term tree), pprint/pretty (Unicode 2D ASCII art), latex (LaTeX); Jupyter integration auto-renders LaTeX via MathJaxVery active; the canonical Python CAS notation surfacehttps://docs.sympy.org/latest/tutorials/intro-tutorial/printing.html
APL (glyph alphabet as notation)1962 (Iverson notation); 1966 (APL\360 implementation)Kenneth E. Iverson (Harvard, then IBM Research); 1979 ACM Turing AwardSingle-glyph operators (⍳⍴⍒⌽⌹⍤⍳⍒↑↓∊⍷⊃⊂⌷) form a self-contained mathematical notation that is also executable; argument is “notation IS the language” (Iverson, “Notation as a Tool of Thought”, CACM 1980)Niche but alive; Dyalog APL is the reference commercial implementation; quant finance and APL puzzle communities sustain ithttps://www.dyalog.com/
Iverson notation (pre-APL, on paper)1962 (Iverson, A Programming Language)Kenneth E. IversonThe pen-and-paper precursor to APL: 2D layout, special characters, Iverson bracket [P] (returning 1 if P is true, 0 otherwise — later popularized by Knuth in Concrete Mathematics)Historical as a notation system; Iverson bracket survives in mainstream math writinghttps://dl.acm.org/doi/10.1145/358896.358899
BNF (Backus-Naur Form)1959–1963 (ALGOL 60 report, Naur ed.)John Backus (IBM); Peter Naur (codifier in the ALGOL 60 report)Meta-notation for context-free grammars: ` ::= ”+” `; arguably the first widely-adopted mathematical notation invented for softwareFoundational and ubiquitous; every language reference, RFC, and textbook uses some flavor
EBNF (Extended BNF)1977 (Wirth); ISO/IEC 14977:1996Niklaus Wirth (ETH Zürich) and othersBNF + repetition ({...}), optional ([...]), grouping ((...)), and quoted terminals; ISO 14977 standardized one variant; W3C XML EBNF is anotherActive; the de-facto formal-grammar notation alongside ANTLR / PEG / yacc-stylehttps://www.iso.org/standard/26153.html
Z notation1977 (Abrial)Jean-Raymond Abrial, Steve Schuman, Bertrand Meyer; matured at Oxford PRG; ISO/IEC 13568:2002 (corrigendum 2007)Set-theoretic specification language with schema boxes (Carroll Morgan) for state and operations; LaTeX zed-csp.sty markup is the standard typesetting; rendered by fuzz, czt, and oz toolchainsLegacy but standardized; still taught in formal-methods courses; used in some safety-critical settingshttps://www.iso.org/standard/21573.html
VDM-SL notation1973 (VDM); ISO/IEC 13817-1:1996 (VDM-SL)IBM Vienna Lab (Dines Bjørner, Cliff Jones); ISO standardization 1996Vienna Development Method Specification Language; Latin-letter ASCII syntax with mathematical operator alternatives; rendered with vdmtools / OvertureNiche; aerospace and Japanese industry pockets; Overture Tool maintainedhttps://www.iso.org/standard/22988.html
B-method mathematical notation1996 (Abrial, The B-Book)Jean-Raymond Abrial; Atelier B / B-ToolkitAbstract Machine Notation (AMN); set-theoretic, refinement-oriented; deployed on Paris Métro Line 14 (driverless), RATP, Alstom rail signalingActive in rail industry; Event-B successor (2005) more academichttps://www.atelierb.eu/en/
OCL (Object Constraint Language) math fragment1997 (IBM); OMG standard 2001; OCL 2.4 in 2014Jos Warmer, Anneke Kleppe (IBM); Object Management Group standardizationUML companion language for invariants, pre/postconditions; uses set-theoretic operators (->forAll, ->exists, ->select); the math sub-notation has its own type system over UML model elementsActive in MDA / model-driven engineering; OCL 2.4 still currenthttps://www.omg.org/spec/OCL/
TikZ / tikz-cd (commutative diagrams)TikZ 2005 (Tantau); tikz-cd ~2013 (Florêncio Neves)Till Tantau (Lübeck) — TikZ; Florêncio Neves — tikz-cdTikZ is a general TeX drawing language; tikz-cd specializes in commutative diagrams: \begin{tikzcd} A \arrow[r] & B \arrow[d] \\ & C \end{tikzcd}; v1.0 documented May 2021; standard category-theory toolActive; the modern default for diagram notation in math papers, replacing xy-pichttps://ctan.org/pkg/tikz-cd
xy-pic1991Kristoffer H. Rose (Aarhus)Earlier diagram package for TeX/LaTeX (and plain TeX); arrow-drawing matrix-style notation: \xymatrix{ A \ar[r] & B }Legacy; largely superseded by tikz-cd, but still seen in older papers and some textbook traditionshttps://ctan.org/pkg/xypic
CD-LaTeX (\begin{CD}...\end{CD})1990 (AMS-LaTeX)American Mathematical SocietyLightweight commutative-diagram environment in amscd package; restricted to rectangular grids with horizontal/vertical/diagonal arrows; simpler than tikz-cd but less expressiveMaintained as part of AMS-LaTeX; used when only basic squares/rectangles are neededhttps://ctan.org/pkg/amscd

(Catalogue total: 26 entries.)

Notable threads

  • TeX won the authoring war; MathML won (eventually) the rendering and accessibility war — but only via translation from TeX. When the W3C Math WG published MathML 1.0 in 1998 it was framed as the path to semantic web math; in practice almost nobody hand-writes MathML. What people do hand-write is LaTeX (or a shorthand like AsciiMath or Typst), and engines like MathJax (v4.1.2 in May 2026) and KaTeX (v0.16.x) parse that and emit MathML or styled HTML. The 2023 enabling of MathML Core in Chromium finally gave all major browsers native support, which closed the rendering gap — but did not change the authoring layer. MathML’s win is invisible: it is the output format that makes math accessible to screen readers and copy-pasteable into Word.

  • Presentation vs. Content is the deepest design split in math notation. Presentation MathML, AsciiMath, TeX/LaTeX math, Typst math — all describe how the formula looks. Content MathML, OpenMath, OMDoc — describe what it means. Reusable formal mathematics (theorem-prover libraries, CAS interchange, semantic search over published math) wants Content. People actually writing math want Presentation, because presentation is shorter and the meaning is usually obvious from context. The result is a chronic disconnect: the world’s body of mathematics is encoded almost entirely in presentation form, and projects like OpenMath, OMDoc, and MMT (Kohlhase’s Mathematical Modelling and Theory format) have spent 25 years trying to bridge it via parsing, semantification, and content-dictionary mapping.

  • Iverson’s claim that mathematical notation should be the programming language is concretely instantiated, repeatedly, and remains niche. Iverson’s 1979 Turing-lecture paper “Notation as a Tool of Thought” (CACM August 1980) argued that an executable notation that respected mathematical conventions would deepen mathematical thought itself. APL was the prototype, J the ASCII redesign, K the minimalist refinement, Q (kdb+) the database query language, and BQN (2020+) the modern revival. The argument is correct — concise notation does help thought — but the cost is a glyph alphabet (or a thicket of @ =: ;: &.: operators) that violates every “code should be readable” intuition mainstream programming has settled on. Quant finance, niche scientific computing, and hobbyists keep the lineage alive. APL itself runs commercially via Dyalog.

  • Wolfram’s three-form architecture is the cleanest separation of parsing, display, and term-tree in any mathematical notation system. InputForm (ASCII, keyboard-typeable, the canonical input form), StandardForm (the 2D rendered display form the front-end shows you), and FullForm (Plus[Power[Sin[x], 2], Power[Cos[x], 2]] — what the evaluator actually sees, an S-expression-like term tree). The system makes explicit something every other notation conflates: that you write math in one language, display it in another, and manipulate it in a third. Mathematica’s front-end can copy any of the three forms to clipboard, parse any of them as input, and round-trip a notebook through them. Few other systems are this honest about the layering.

  • Typst is the first credible TeX successor in 48 years. Released by Martin Haug and Laurenz Mädje at TU Berlin in 2023, Typst (v0.13 series in 2026) keeps math-mode delimiters ($...$) but cleans up almost everything else: x_i is a subscript without entering a special mode; mat(1, 2; 3, 4) defines a matrix via function-call syntax; multi-letter words like pi, dot, RR automatically resolve to symbols; and you write floor(x) instead of \lfloor x \rfloor. Errors are real error messages with line numbers, not the “Missing $ inserted” mystery messages of TeX. Compilation is incremental and roughly an order of magnitude faster than LaTeX. Adoption is rapid in academic preprints, with import packages like mitex allowing LaTeX math fragments to be embedded during transition.

  • Diagram notation is a separate problem from formula notation, and the family that solved it took 30 years to converge. Linear math notation (TeX, MathML, AsciiMath, Typst) cannot encode commutative diagrams or category-theory arrow shapes — those need 2D placement and arbitrary morphism arrows. Three eras: AMS-LaTeX’s amscd (1990, rectangular grids only), Kristoffer Rose’s xy-pic (1991, more expressive but cryptic syntax), and Florêncio Neves’s tikz-cd (~2013, on top of Till Tantau’s TikZ). Tikz-cd is now the standard in published category theory and homological algebra; xy-pic survives in older textbook traditions; amscd is still used for simple square diagrams.

  • The MathSciNet / MR-citation format is its own micro-notation family. Mathematical Reviews (American Mathematical Society, 1940+) assigns each published math item an MR number (e.g. MR2015234) and a structured citation form. AMS-LaTeX bibliography styles (amsplain.bst, amsalpha.bst) encode the convention; arXiv, journals, and MathSciNet itself round-trip the format. It is not a math notation in the formal sense, but it is the reference-graph notation that the math-publishing world runs on, alongside DOI and arXiv-id. Cross-listed in document-typesetting in passing.

  • The specification-notation family (Z, B, VDM-SL, OCL) sits at the boundary of “math notation” and “formal-methods language.” Z’s schema boxes (Carroll Morgan, Oxford PRG) are first and foremost a notation — a 2D layout with declarations above a horizontal rule and predicates below — that happened to be standardized as ISO/IEC 13568:2002. Same with B’s Abstract Machine Notation, VDM-SL’s set-builder vocabulary, and OCL’s ->forAll / ->select / ->collect chain. They are catalogued more deeply as systems in notation-spec; they appear here because the notation itself is mathematical, often rendered with TeX (zed-csp.sty, vdmlatex) and predates by decades the typing infrastructure that mechanically checks specifications written in them.

  • The Backus-Naur lineage is mathematical notation invented for software. When John Backus and Peter Naur produced the ALGOL 60 report (1963), the metasyntax they used was a deliberate exercise in mathematical formalism for grammars — production rules, alternation, recursion — at a time when programming-language definitions were typically natural prose. Wirth’s EBNF (1977, ISO/IEC 14977:1996) and the W3C-XML EBNF dialect refined the meta-notation. Every modern parser-generator (yacc, ANTLR, PEG, tree-sitter, the instaparse family) traces back to that BNF abstraction. It belongs in this index because it is the most successful mathematical notation invented in the computing era — and because the same BNF metasyntax has been used to formalize, in turn, BNF itself.

Citations

Graph View