attomath

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.

Main data structures

There are three main data structures in attomath: Statements, DVRs and Theorems.

Statements

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.

DVRs

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.

Theorems

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.