Structured Typesetting for Metamath
Metamath's set.mm database constructs mathematics from scratch, starting from ZFC set theory axioms, up to algebra, topology, analysis, graph theory and more. It includes over 32,000 formalized proofs, all of them automatically verified.
Metamath itself does not prescribe any syntax, other than the fact that formulas shall be unambiguously parseable: they are basically a string of tokens. The set.mm database defines mathematical symbols as such tokens, so that their ASCII version resembles as closely as possible to their counterpart in mathematical notation. The "GIF" and "unicode" typesettings then renders these tokens one by one. For advanced formulas, this notation is increasingly diverging from the classical mathematical notations. This may be a barrier for people discovering Metamath.
This project, structured typesetting, provides a display of set.mm's formulas as close as possible to the usual mathematical notations, and hopes to enable access to Metamath's set.mm to more people. Here are a few interersting entry points from which to browse on:
 The area of a circle areacirc
 The quadratic equation quad
 The binomial theorem binom
 The sum of arithmetic series arisum
 The sum of geometric series geoser
 The Basel problem basel
 The mean value theorem mvth
 Stirling's formula stirling
 The birthday problem birthday
 The inclusionexclusion theorem incexc2
Below is an example of how the same formula, the statement of the trirn theorem, is displayed in the different typesettings:
Original Metamath source 
 ( ph > ( sqr ` sum_ k e. A ( ( B + C ) ^ 2 ) )


GIF typesetting  
Unicode typesetting  
Structured typesetting 
In the cases where it simplifies the display, structured typesetting may however hide the formula's structure.
In the example above, for example, the square roots are formalized as the value of the function sqr
.
This is not directly visible in the structured typesetting.
How does it work?
The MathML markup language is an ISO standard and the W3C recommendation for embedding maths in documents on the Web, therefore it seems a reasonable choice for displaying Metamath's formulas.
Both MathML and Metamath can be seen as using a treelike representation for formulas. The formula of the example above, for example, can be seen as: (click on the bullets to collapse nodes)

Implication: wi
( ph > ps )
In presentation MathML, the same formula can also be seen as a tree:

Math row:
<mrow>
…</mrow>
 Phi symbol identifier
<mi>φ</mi>
$\phi $  Implies operator
<mi>→</mi>
→  Math row:
<mrow>
…</mrow>
 Square root radical notation
<msqrt>
…</msqrt>
$\surd $ Math row:
<mrow>
…</mrow>
 Underscript:
<munder>
…</munder>
 Summation operator
<mo>∑</mo>
$\sum $  Math row:
<mrow>
…</mrow>
 k symbol identifier
<mi>k</mi>
$k$  Elementhood operator
<mo>∈</mo>
$\in $  A symbol identifier
<mi>A</mi>
$A$
 k symbol identifier
 Summation operator
 Superscript:
<msup>
…</msup>
 Fenced row
<mfenced>
…<mfenced>
 B symbol identifier
<mi>A</mi>
$B$  Addition operator
<mo>+</mo>
$+$  C symbol identifier
<mi>A</mi>
$C$
 B symbol identifier
 Numeric value 2
<mn>2</mn>
 Fenced row
 Underscript:
 Math row:
 Lessorequal operator
<mo>≤<mo>
≤  Math row:
<mrow>
…</mrow>
 Square root radical notation
<msqrt>
…</msqrt>
$\surd $ Math row:
<mrow>
…</mrow>
 Underscript:
<munder>
…</munder>
 Summation operator
<mo>∑</mo>
$\sum $  Math row:
<mrow>
…</mrow>
 k symbol identifier
<mi>k</mi>
$k$  Elementhood operator
<mo>∈</mo>
$\in $  A symbol identifier
<mi>A</mi>
$A$
 k symbol identifier
 Summation operator
 Superscript:
<msup>
…</msup>
 B symbol identifier
<mi>B</mi>
$B$  Numeric value 2
<mn>2</mn>
 B symbol identifier
 Underscript:
 Math row:
 Addition operator
<mo>+</mo>
$+$  Square root radical notation
<msqrt>
…</msqrt>
$\surd $ Math row:
<mrow>
…</mrow>
 Underscript:
<munder>
…</munder>
 Summation operator
<mo>∑</mo>
$\sum $  Math row:
<mrow>
…</mrow>
 k symbol identifier
<mi>k</mi>
$k$  Elementhood operator
<mo>∈</mo>
$\in $  A symbol identifier
<mi>A</mi>
$A$
 k symbol identifier
 Summation operator
 Superscript:
<msup>
…</msup>
 C symbol identifier
<mi>C</mi>
$C$  Numeric value 2
<mn>2</mn>
 C symbol identifier
 Underscript:
 Math row:
 Square root radical notation
 Square root radical notation
 Phi symbol identifier
The idea of structured typesetting is to transform one structure into the other. One possibility would have been to give the representation for each of set.mm's syntactic axiom, like for csu and wi. However, in order to be even more flexible, it is actually based on rules. The formula to be displayed is matched against that set of rules, and if a match is found, then the same is applied to each of its element, recursively.
Adapted representations:
Metamath's conventions page provides very useful explanations about the notations used in set.mm.
Formulas displayed with structured typesetting will not differ much from formulas displayed in the Unicode typesetting, until more complex constructs are introduced. Most of the propositional calculus, predicate calculus and work ZFC abstract class building will look very similar in both typesettings. However, staring with functions, structured typsetting for set.mm will displays formulas differently, to get as near as possible to the classical math representation.
Function values, to start with, may surprise new users by the way they are represented in set.mm.
In set.mm, the value of the function F
applied at X
is written ( F ` X )
.
Structured typesetting allows to write is as the more conventional ${F}\left({X}\right)$
The table below provides a comparison of several mathematical constructs, with their representation in set.mm and in structured typesetting.
Construct name  ASCII Representation in set.mm  Structured typesetting  Example theorems 

Function value  ( F ` X ) 
${F}\left({X}\right)$  f1ofveu 
Image of a set  ( F " A ) 
${F}\left[{X}\right]$  unipreima 
Inverse functions  `' F 
${{F}}^{1}$  unpreima 
Sums, products, unions, intersections iterating over sets  sum_ x e. A ( F ` x ) prod_ x e. A ( F ` x ) U_ x e. A ( F ` x ) ^_ x e. A ( F ` x ) 
$\sum _{{x}\in {A}}{F}\left({x}\right)$ $\prod _{{x}\in {A}}{F}\left({x}\right)$  0.999... risefacval 
Sums, products, unions, intersections iterating over integer intervals  sum_ x e. ( 1 ... N ) ( F ` x ) prod_ x e. ( 1 ... N ) ( F ` x ) U_ x e. ( 1 ... N ) ( F ` x ) ^_ x e. ( 1 ... N ) ( F ` x ) 
$\sum _{{x}=1}^{{N}}{F}\left({x}\right)$  pcfac 
Fractions  ( 1 / 2 ) 
$\frac{1}{2}$  geoihalfsum 
Intervals  ( 0 [,) 1 ) 
$\left[0,1\right)$  icoun 
Absolute values Set cardinal 
( abs ` A ) ( # ` A ) 
$\left{A}\right$  hashun 
Square roots  ( sqr ` x ) 
$\sqrt{{x}}$  sqrdiv 
Complex conjugate  ( * ` z ) 
$\stackrel{\u203e}{{z}}$  addcj root1cj 
Decimal numerals  ; ; 3 6 5 
$365$  birthday 1kp2ke3k 
Binomial coefficient  ( M _C N ) 
$\left(\genfrac{}{}{0ex}{}{{M}}{{N}}\right)$  bcp1n 
Exponential notation  ( A ^ B ) ( A ^c B ) ( exp ` X ) 
${{A}}^{{B}}$${e}^{{X}}$  efadd 
Factorials  ( ! ` N ) 
${N}!$  facp1 
Integrals  S_ [ A > B ] ( F ` x ) _d x S. E ( F ` x ) _d x 
${\int}_{{A}}^{{B}}{F}\left({X}\right)d{x}$ ${\int}_{{E}}{F}\left({X}\right)d{x}$  ditgsplit 
Derivatives 
( RR _D F ) ( RR _D ( x e. A > B ) ) 
${{F}}_{\mathbb{R}}^{\prime}$ $\frac{d\left({x}\in {A}\u27fc{B}\right)}{{d}_{\mathbb{R}}{x}}$  mvth divlip dvexp3 
Brackets/parenthesis
TBC
Invisible times
TBC
What is kept the same:
In set.mm, there is a major difference between set variables, written in red lowercase, and class variables, written in pink uppercase. For example, quadratic equations, which are usually written with all variables in lower case $a{x}^{2}+bx+c$, are written in uppercase in Metamath if class variables are used. We keep the set.mm notation for class variables, so the same equation may be rendered ${A}{{X}}^{2}+{B}{X}+{C}$.