Mathelia is a system for writing mathematics as Books: short, self-contained texts whose theorems are machine-checked.
Like Metamath and Mizar, we build mathematics on first-order logic and set theory by accumulating definitions, theorems and proofs.
Our vision is that AI agents write the Books, and humans read them as works of art: each Book has one goal, every assumption is visible, and proofs are short enough to follow.

Where to start: the example below (Cantor's theorem, one short proof explained step by step); the English tutorial (6 short Books on how a Book is written and reviewed); the Freek100 list (Books on well-known theorems).

An example: Cantor's theorem

There is no bijection between a set \(X\) and its power set \(\wp X\). Take any \(f : X \to \wp X\) and let \(A = \{x \in X \mid x \notin f(x)\}\). If \(A = f(a)\), then \(a \in A \iff a \notin A\); so \(f\) is not surjective. In our Book on Cantor's theorem this is written as follows (Book with all proofs, source):

thm `X {/}=# ℘ X` ◀ W. , ax_s
prf |A_ := `\{ cls x ∈ |X | {/}∃ y (\< pr x ; y \> ∈ |f and x ∈ y) \}` ;
    `|f ∈ |X → ℘ |X ⟹ |f {/}∈ |X →S ℘ |X` /// W. -| ax_s[C_:=`|A_`] , pr:0 v;
    Le <- `f ∈ X → ℘ X ⟹ f {/}∈ X →S ℘ X` -| W. , ax_s h[fix];
    goal / =#.' / →IS. / →I. -| Le p;
    goal -| W. , ax_s h;
  • The statement X {/}=# ℘ X is displayed as \(X \stackrel{{\tt /}}{\stackrel{\#}=} \wp X\): \(X\) and \(\wp X\) do not have the same size.
  • The assumptions after \(\blacktriangleleft\) are all the theorem depends on: W. (the definitions made earlier in the Book: power set, ordered pair, function, surjection, …) and ax_s, separation: ∃ X C_ ⊂_ X ⟹ Exi C_, i.e. a class C_ contained in some set is a set (Exi C_ means ∃ X (X =_ C_)).
  • In the proof, goal is the statement being proved (X {/}=# ℘ X), |X and |f are \(X\) and \(f\) fixed as constants, and |A_ is the diagonal class \(A\); ax_s[C_:=`|A_`] is ax_s with |A_ substituted for its class variable C_, so the prover itself finds that \(A\) is a set (\(A \subset X\)). Each step says "this formula follows from these facts", may first unfold definitions (/// W. unfolds the definitions three times), and names the prover that checks it: p = Prover9, v = Vampire. O means "no facts".
  • The steps marked h are checked by Hyperion, our own component that combines checked steps: h[fix] turns the result about the fixed |X, |f into one about all \(X\), \(f\), and the last step combines everything into the stated theorem.

The same Book also gives a second proof (no injection from \(\wp X\) into \(X\)); a Book may contain several proofs of one theorem, or the proofs may be put in separate Books. Reviewing the whole Book (12 theorems) takes about 2 seconds.

Formulas are written in our notation Formel and translated by fixed, mechanical rules into one-sorted first-order logic, or into a two-sorted logic of sets and classes. The translator never reasons; replacing a formula by an "equivalent" one is a theorem, not a translation.

Mathelia and Metamath

MetamathMathelia
Foundationfirst-order logic and ZFC set theory, classes as eliminable abbreviationsthe same idea: first-order logic and set theory, classes translated away by fixed rules
Logicbuilt from Hilbert-style axioms inside the databasefirst-order logic is taken as known
Proof stepsevery step written out, checked by a tiny verifiershort steps, each checked by an automated prover
Libraryone large database (set.mm)many small Books, each with one goal and explicit assumptions
Writer / readerhumans (and increasingly machines) write; the proofs are complete and explicitAI writes; humans read the Book as a text

We share Metamath's starting point, and we admire its idea that anyone can check every step with a very small program. That is exactly where Mathelia is weaker today, as described below.

What a check relies on

When a theorem is accepted, the result relies on:

  1. the assumptions written in the theorem (axioms and definitions);
  2. the translation rules from Formel to first-order logic (implemented in PHP);
  3. the automated provers Prover9 (2009-11A) and Vampire (5.0.1), and, for higher-order steps, Satallax, used as oracles: their proofs are not yet re-checked;
  4. the rules of Hyperion.

Every review report lists these: the assumptions of each theorem (separating axioms from definitions), and the date, the version of the review code and the prover versions.

So "accepted" means that the current pipeline accepted the theorem; it does not mean that the pipeline itself has been independently proved sound.

Known open points:

  • Hyperion is not yet a small, independently verified kernel. It now records each derivation (which rule, which checked steps and theorems it used), but no small independent checker re-checks these records yet.
  • By default, a definition of a set-valued symbol is read as also asserting that the set exists; the review report names such definitions. An option makes a Book prove existence before the definition; we plan to use it in Books that discuss the axioms of set theory.
  • A step may use a theorem proved in the two-sorted logic inside a one-sorted step. This is not yet proved sound, so it is allowed only when the step is explicitly marked (h[lift]), and the result shows which theorems depend on it.
  • The text of a Book does not fix the meaning of every symbol by itself: the grammar of symbols and some definitions (e.g. ax_s) are stored in a shared database. We are considering exporting an "expanded Book" that includes everything it depends on.
  • During development, independent reviews by other AI systems found several cases where Hyperion accepted something it should not. All were fixed, and each case is kept as a regression test.

Formalizing 100 Theorems: 22 so far

An AI (Claude) is writing Mathelia Books for the theorems in Freek Wiedijk's list. So far the AI does not work on its own: a human (our representative) chooses the goals, reads the Books and asks for changes, and the AI writes and revises them. See the list of Books; no account is needed. The Books do not all rely on the same things: each review report shows what its theorems depend on (for example, steps marked h[lift]).

Status and contact

Mathelia is developed by the ATP Research Group, a small group in Japan. It is still under development. Books and their sources can be read without an account. An English tutorial (6 short Books) is available; the explanatory text in the other Books and most of the interface are still in Japanese.
We would be very glad to hear your opinions, especially on how to make the checks more trustworthy. For example:

  • How could a small independent checker, as in Metamath, be added: one that re-checks Hyperion's derivation records, or the provers' proofs?
  • Should a Book be self-contained down to the grammar and definitions of its symbols, or is a shared base of definitions acceptable?

Contact: Tomohiko Suda [t@mshk1201.com]