# 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 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 inclusion-exclusion 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 ) )       <_ ( ( sqr  sum_ k e. A ( B ^ 2 ) ) + ( sqr  sum_ k e. A ( C ^ 2 ) ) ) )

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 tree-like 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 )
• Phi WFF variable wph ph
• Binary relationwbr A R B
• Function value cfv ( F  X )
• Square root function csqr sqr
• Finite sum construct csu sum_ k e. A B
• The k set variablevk k
• The A class variablecA A
• Operation value co (A F B)
• Operation value co (A F B)
• The B class variablecB B
• Complex addition operation caddc +
• The C class variablecC C
• The exponentiation functioncexp ^
• The integer 2c2 2
• Less-than relation cle <_
• Operation value co (A F B)
• Function value cfv ( F  X )
• Square root function csqr sqr
• Finite sum construct csu sum_ k e. A B
• The k set variablevk k
• The A class variablecA A
• Operation value co (A F B)
• The B class variablecB B
• The exponentiation functioncexp ^
• The integer 2c2 2
• Complex addition operation caddc +
• Function value cfv ( F  X )
• Square root function csqr sqr
• Finite sum construct csu sum_ k e. A B
• The k set variablevk k
• The A class variablecA A
• Operation value co (A F B)
• The C class variablecC C
• The exponentiation functioncexp ^
• The integer 2c2 2

In presentation MathML, the same formula can also be seen as a tree:

• Math row: <mrow></mrow>
• Phi symbol identifier<mi>&phi;</mi> $\phi$
• Implies operator <mi>&rarr;</mi>
• Math row: <mrow></mrow>
• Square root radical notation <msqrt></msqrt> $\surd$
• Math row: <mrow></mrow>
• Underscript: <munder></munder>
• Summation operator <mo>&sum;</mo> $\sum$
• Math row: <mrow></mrow>
• k symbol identifier<mi>k</mi> $k$
• Elementhood operator <mo>&isin;</mo> $\in$
• A symbol identifier<mi>A</mi> $A$
• 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$
• Numeric value 2 <mn>2</mn>
• Less-or-equal operator <mo>&le;<mo>
• Math row: <mrow></mrow>
• Square root radical notation <msqrt></msqrt> $\surd$
• Math row: <mrow></mrow>
• Underscript: <munder></munder>
• Summation operator <mo>&sum;</mo> $\sum$
• Math row: <mrow></mrow>
• k symbol identifier<mi>k</mi> $k$
• Elementhood operator <mo>&isin;</mo> $\in$
• A symbol identifier<mi>A</mi> $A$
• Superscript: <msup></msup>
• B symbol identifier<mi>B</mi> $B$
• Numeric value 2 <mn>2</mn>
• Addition operator <mo>+</mo> $+$
• Square root radical notation <msqrt></msqrt> $\surd$
• Math row: <mrow></mrow>
• Underscript: <munder></munder>
• Summation operator <mo>&sum;</mo> $\sum$
• Math row: <mrow></mrow>
• k symbol identifier<mi>k</mi> $k$
• Elementhood operator <mo>&isin;</mo> $\in$
• A symbol identifier<mi>A</mi> $A$
• Superscript: <msup></msup>
• C symbol identifier<mi>C</mi> $C$
• Numeric value 2 <mn>2</mn>

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.

Metamath's conventions page provides very useful explanations about the notations used in set.mm. Where possible, the notation attempts to conform to modern conventions, with variations due to our choice of the axiom system or to make proofs shorter. However, our notation is strictly sequential (left-to-right). For example, summation is written in the form Σ𝑘 ∈ 𝐴𝐵 (df-sum) which denotes that index variable 𝑘 ranges over 𝐴 when evaluating 𝐵. Thus, Σ𝑘 ∈ ℕ (1 / (2↑𝑘)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum). Structured typesetting and MathML on the other hand, allow to display formulas using underscripts, overscripts, subscripts ans superscripts. See df-sum and geoihalfsum for the representation of the same formula wiht structured typesetting.

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{‾}{{z}}$ addcj
root1cj
Decimal numerals ; ; 3 6 5 $365$ birthday
1kp2ke3k
Binomial coefficient ( M _C N ) $\left(\genfrac{}{}{0}{}{{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}}_{ℝ}^{\prime }$ $\frac{d\left({x}\in {A}⟼{B}\right)}{{d}_{ℝ}{x}}$ mvth
divlip
dvexp3

TBC

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}$.