attomath is a system for formalizing and proving mathematical theorems heavily inspired by
Metamath. attomath aims to be as small as possible while
still being able to describe any axiomatic system.
There are three main data structures in attomath: Statements, DVRs and Theorems.
A Statement in attomath could represent something like a -> a is provable or a = b is
syntactically correct. It consists of a judgement (is provable, is syntactically correct)
and a expression (a -> a, a = b). What differentiates attomath most from Metamath is that
expressions are not stored as a string, but as a (binary) syntax tree encoded as a sequence in
prefix order. This makes comparisons and substitutions faster and more consistent.
A DVR is a way of preventing two variables to be equal.
In general it is assumed, that a Statement does not change its meaning if a variable is
replaced with another variable, but this is not true in all cases. For this one can specify that
two variables should not be replaced with the same variable or expressions containing a common
variable.
A Theorem consists of zero or more assumptions (Statements) and DVRs and one conclusion
(also a Statement). This makes it possible to formulate something like if a is provable and
a -> b is provable then b is provable. In this case a is provable and a -> b is provable
are assumptions and b is provable is a
conclusion.
The structs interface guarantees that only valid theorems can be produced if only axioms are
constructed using Theorem::new, while still being able to crate any theorem that can be proven
from the given axioms (these claims are not yet proven).
In attomath, unlike Metamath, all assumptions (called Hypothesis in Metamath) for a theorem
are stored together with their corresponding theorem. This way variables carry no meaning
outside a theorem, and the context for a statement is always the theorem of that statement.
This means that attomaths format is less compact, since "variable types" like formula or
set variable have to be declared for every theorem. But it also leads to a more consistent
format where a theorem is self-contained.