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.

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.

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.
  • 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. See the list of Books; no account is needed.

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.
Contact: Tomohiko Suda [t@mshk1201.com]