The best way to understand MathLingua is to start with an example. We will create a small collection of a theorem, a couple definitions, and a book. First we will describe the theorem:

Theorem:

.for:G := (X, *, e),a,b,c

where:

.'G is \group'

.'a, b, c \in X'

then:

.if:

.'a*b = a*c'

then:

.'b = c'

Metadata:

.concept:"This result shows that the $\textbf{left cancellation law}$ is true in a group."

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"47"

.for:G := (X, *, e),a,b,c

where:

.'G is \group'

.'a, b, c \in X'

then:

.if:

.'a*b = a*c'

then:

.'b = c'

Metadata:

.concept:"This result shows that the $\textbf{left cancellation law}$ is true in a group."

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"47"

This example describes a proven mathematical result that states that the left cancellation property holds in groups.

Read out loud, the result says for any *G* that is a tuple of *(X, *, e)* and any
*a*, *b*, and *c* where *G* is a group and *a*, *b*, and
*c* are elements of *X*, then if *a*b = a*c* then *b = c*.

Notice that reading the result out loud essentially amounts to reading the result top to bottom and left to right ignoring indentation. The MathLingua code above, and the previous paragraph describing it, might have been both equally easy for you to read and understand.

But for a computer, the indentation and layout in MathLingua code conveys meaning that is easy to understand, while the same meaning in the paragraph above is much more difficult to understand.

This illustrates an explicit goal of MathLingua. It is designed to be just as easy to understand as traditional mathematical literature for a person, but can also be understood by a computer (in particular the MathLingua command line tool mlg or Visual Studio Code extension).

To the MathLingua tooling, MathLingua isn't just text (like it is in LaTeX), but has meaning. And if it can understand MathLingua, it can automate updating your collection of knowledge as you grow it.

Next, notice that our result precisely describes that cancellation can occur in groups but
also has a *concept* section that makes this clear. Thus, if the precise statement is
not immediately clear, the *concept* section allows you to give an easier to understand
summary of the result, describe why the result is important, or describe how it is related to
other results.

Further, the result has a reference to something called *AbstractAlgebraTheoryAndApplications*
page *47*. However, what is this reference$?$

This reference is just another item recorded using MathLingua as:

[AbstractAlgebraTheoryAndApplications]

Resource:

.type:"Book"

.name:"Abstract Algebra Theory and Applications"

.author:"Thomas W. Judson"

.date:"August 15, 2014"

.url:"http://abstract.ups.edu/download/aata-20140815.pdf"

.offset:"10"

Metadata:

.tag:"Abstract Algebra"

Resource:

.type:"Book"

.name:"Abstract Algebra Theory and Applications"

.author:"Thomas W. Judson"

.date:"August 15, 2014"

.url:"http://abstract.ups.edu/download/aata-20140815.pdf"

.offset:"10"

Metadata:

.tag:"Abstract Algebra"

We won't go into details about this item. The point at this time is that using MathLingua, you can describe not just mathematical results, but also describe books and other resources that can be read for further information about results.

Now notice that the left cancellation result references the definition of a *Group*,
but what is a *Group*$?$ The following shows how to encode this definition in MathLingua:

[\group]

Defines:G := (X, *, e)

assuming:

.'X is \set'

.'* is \binary.operation:on{X}'

.'e \in X'

means:

.for:a,b,c

where:

.'a, b, c \in X'

then:

.'(a * b) * c = a * (b * c)'

.for:a

where:

.'a \in X'

then:

.'a * e = e * a = a'

.for:a

where:

.'a \in X'

then:

.exists:b

suchThat:

.'b \in X'

.'a * b = b * a = e'

Metadata:

.written:"\textrm{group}"

.concept:"The integers have a nice property that zero is an integer and any integer $x$ has a negative $-x$ such that $x + -x = 0$, along with the fact that addition is $\textbf{associative}$. A $\textbf{group}$ abstracts this notion of a set and an operation with these nice properties."

.note:"$*$ is said to be $\textbf{associative}$ because $a*(b*c) = (a*b)*c$ for any $a,b,c \in X$."

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"43"

Defines:G := (X, *, e)

assuming:

.'X is \set'

.'* is \binary.operation:on{X}'

.'e \in X'

means:

.for:a,b,c

where:

.'a, b, c \in X'

then:

.'(a * b) * c = a * (b * c)'

.for:a

where:

.'a \in X'

then:

.'a * e = e * a = a'

.for:a

where:

.'a \in X'

then:

.exists:b

suchThat:

.'b \in X'

.'a * b = b * a = e'

Metadata:

.written:"\textrm{group}"

.concept:"The integers have a nice property that zero is an integer and any integer $x$ has a negative $-x$ such that $x + -x = 0$, along with the fact that addition is $\textbf{associative}$. A $\textbf{group}$ abstracts this notion of a set and an operation with these nice properties."

.note:"$*$ is said to be $\textbf{associative}$ because $a*(b*c) = (a*b)*c$ for any $a,b,c \in X$."

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"43"

The definition details the specifics of what a group is as well as a concept and note that provide
additional information. Further, the definition uses an indentation style similar to the *Theorem:*
above to convey meaning. Also, note that the command *\group* is used to specify a group, and a
group is a tuple of the form *G := (X, *, e)*.

Next notice that the definition of a group refers to a *\binary.operation:on{X}* and
a *\set*. In MathLingua, you don't need to define everything that you use, but it is
good to do so. The following are those definitions:

[\binary.operation:on{A}]

Defines:*

assuming:

.'A is \set'

means:

."$*?$ is a function that assigns to each pair $(a?, b?) \in A? \times A?$ a unique element $a? *? b? \in A."

Metadata:

.written:"A?? \times A?? \mapsto A??"

.name:

."binary operation"

."law of composition"

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"42"

[\set]

Defines:X

means:

."A well defined collection of distinct objects."

Metadata:

.written:"\textrm{set}"

Defines:*

assuming:

.'A is \set'

means:

."$*?$ is a function that assigns to each pair $(a?, b?) \in A? \times A?$ a unique element $a? *? b? \in A."

Metadata:

.written:"A?? \times A?? \mapsto A??"

.name:

."binary operation"

."law of composition"

.reference:

.source:"@AbstractAlgebraTheoryAndApplications"

page:"42"

[\set]

Defines:X

means:

."A well defined collection of distinct objects."

Metadata:

.written:"\textrm{set}"

Notice that the above definitions use double quotes instead of single quotes. In MathLingua, text in single quotes are statements that refer to definitions. Text in double quotes are instead interpreted as LaTeX.

This allows us to provide a textual definition in LaTeX if a structural description is not needed. In particular, the knowledge in our collection can be as precise as we need it with the ability to add precision later.

Further notice that the definitions have a *written:* section. For the
*\binary.operation:on{A}* the written form is *A?? \times A?? \mapsto A??*.
This is used by the MathLingua tooling render MathLingua code similar to how LaTeX code is
rendered into math symbols.

In particular, what the written form says is that a *\binary.operation:on{A}*
command should be displayed to look the same as how *A?? \times A?? \mapsto A??*
is rendered in LaTeX. The *??* states that *A* is a parameter to the
*\binary.operation:on{A}* and that parameter should have parentheses written around
it if it is a complex expression.

For example the expression *\binary.operation:on{X + Y}* would be rendered as
*(X + Y) \times (X + Y) \mapsto (X + Y)*

At this point, we have a theorem with related definitions, but they are hard to visualize
as plain text. The MathLingua tooling has the ability to render MathLingua code. The result
for the code above is as follows. Notice the way *\binary.operation:on{X}* is rendered.

Theorem:

.for:\[G := (X, *, e)\],\[a\],\[b\],\[c\]

where:

.\[G\]is\[\textrm{group}\]

.\[a, b, c \in X\]

then:

.if:

.\[a * b = a * c\]

then:

.\[b = c\]

Metadata:

.concept:This result shows that the $\textbf{left cancellation law}$ is true in a group.

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:47

[AbstractAlgebraTheoryAndApplications]

Resource:

.type:Book

.name:Abstract Algebra Theory and Applications

.author:Thomas W. Judson

.date:August 15, 2014

.url:http://abstract.ups.edu/download/aata-20140815.pdf

.offset:10

Metadata:

.tag:Abstract Algebra

[\group]

Defines:\[G := (X, *, e)\]

assuming:

.\[X\]is\[\textrm{set}\]

.\[*\]is\[X \times X \mapsto X\]

.\[e \in X\]

means:

.for:\[a\],\[b\],\[c\]

where:

.\[a, b, c \in X\]

then:

.\[(a * b) * c = a * (b * c)\]

.for:\[a\]

where:

.\[a \in X\]

then:

.\[a * e = e * a = a\]

.for:\[a\]

where:

.\[a \in X\]

then:

.exists:\[b\]

suchThat:

.\[b \in X\]

.\[a * b = b * a = e\]

Metadata:

.written:\textrm{group}

.concept:The integers have a nice property that zero is an integer and any integer $x$ has a negative $-x$ such that $x + -x = 0$, along with the fact that addition is $\textbf{associative}$. A $\textbf{group}$ abstracts this notion of a set and an operation with these nice properties.

.note:$*$ is said to be $\textbf{associative}$ because $a*(b*c) = (a*b)*c$ for any $a,b,c \in X$.

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:43

[\binary.operation:on{A}]

Defines:\[*\]

assuming:

.\[A\]is\[\textrm{set}\]

means:

.$*$ is a function that assigns to each pair $(a, b) \in A \times A$ a unique element $a * b \in A.

Metadata:

.written:A \times A \mapsto A

.name:

.binary operation

.law of composition

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:42

[\set]

Defines:\[X\]

means:

.A well defined collection of distinct objects.

Metadata:

.written:\textrm{set}

.for:\[G := (X, *, e)\],\[a\],\[b\],\[c\]

where:

.\[G\]is\[\textrm{group}\]

.\[a, b, c \in X\]

then:

.if:

.\[a * b = a * c\]

then:

.\[b = c\]

Metadata:

.concept:This result shows that the $\textbf{left cancellation law}$ is true in a group.

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:47

[AbstractAlgebraTheoryAndApplications]

Resource:

.type:Book

.name:Abstract Algebra Theory and Applications

.author:Thomas W. Judson

.date:August 15, 2014

.url:http://abstract.ups.edu/download/aata-20140815.pdf

.offset:10

Metadata:

.tag:Abstract Algebra

[\group]

Defines:\[G := (X, *, e)\]

assuming:

.\[X\]is\[\textrm{set}\]

.\[*\]is\[X \times X \mapsto X\]

.\[e \in X\]

means:

.for:\[a\],\[b\],\[c\]

where:

.\[a, b, c \in X\]

then:

.\[(a * b) * c = a * (b * c)\]

.for:\[a\]

where:

.\[a \in X\]

then:

.\[a * e = e * a = a\]

.for:\[a\]

where:

.\[a \in X\]

then:

.exists:\[b\]

suchThat:

.\[b \in X\]

.\[a * b = b * a = e\]

Metadata:

.written:\textrm{group}

.concept:The integers have a nice property that zero is an integer and any integer $x$ has a negative $-x$ such that $x + -x = 0$, along with the fact that addition is $\textbf{associative}$. A $\textbf{group}$ abstracts this notion of a set and an operation with these nice properties.

.note:$*$ is said to be $\textbf{associative}$ because $a*(b*c) = (a*b)*c$ for any $a,b,c \in X$.

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:43

[\binary.operation:on{A}]

Defines:\[*\]

assuming:

.\[A\]is\[\textrm{set}\]

means:

.$*$ is a function that assigns to each pair $(a, b) \in A \times A$ a unique element $a * b \in A.

Metadata:

.written:A \times A \mapsto A

.name:

.binary operation

.law of composition

.reference:

.source:@AbstractAlgebraTheoryAndApplications

page:42

[\set]

Defines:\[X\]

means:

.A well defined collection of distinct objects.

Metadata:

.written:\textrm{set}

At this point, we have created a small collection of mathematical knowledge that we can continue to grow. In particular, now that the definition of a group has been recorded, we can record other theorems about groups.

Note that definitions and theorems do not need to be in any particular order and do not need to even be in the same file. You can organize your mathematical knowledge however you would like. You can have separate files for definitions and theorems, separate files by topic, or any other layout. As long as a definition occurs in a file, the MathLingua tooling will be able to find it an use it to render your collection.