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.

A complete example: there are infinitely many primes

This is the main theorem of our Book on the infinitude of primes, with its whole proof (source of the whole Book):

let/thm Linf <- `n ∈ 𝕄 ⟹ [ ∃ p ∈ ℙ . n < p ]` ◀ W. ,, 𝕄0s ,, IND𝕄 ,, suc𝕄 ,, +𝕄 ,, *𝕄
prf L2 <- `N ∈ 𝕄 and N {/}= 0 ⟹ 2 ≤ N + 1` -| L2≤ ,, +𝕄 ,, 1. ,, suc𝕄 ,, 𝕄0s ,, +∈𝕄 v;
    L3 <- `[ n ; N ; p col ∈ 𝕄 ] and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n ⟹ d ∣ N) ]
           and p ∈ ℙ and p ∣ N + 1 ⟹ n < p` -| Ltot ,, Lcop ,, ℙ.' ,, L≠0 p;
    Linf -| LN ,, L2 ,, Lpf ,, L3 ,, ℙ.' ,, +∈𝕄 ,, 𝕄0s ,, 1. v;
    Linf -| W. ,, 𝕄0s ,, IND𝕄 ,, suc𝕄 ,, +𝕄 ,, *𝕄 h;
  • The statement is displayed as \(n \in \mathbb{M} \Longrightarrow \exists p \in \mathbb{P}\ (n < p)\).
  • The assumptions after \(\blacktriangleleft\) are all the theorem depends on: \(\mathrm{W.}\) (the definitions introduced so far in the Book) and the axioms of the natural numbers: 𝕄0s (\(0 \in \mathbb{M}\), closed under successor), IND𝕄 (induction), suc𝕄 (successor is injective and never \(0\)), +𝕄, *𝕄 (recursive equations). Changing the assumptions gives a different Book with a different construction.
  • Each proof step says "this formula follows from these facts" and names the backend that checks it: p = Prover9, v = Vampire. LN (some \(N \neq 0\) is divisible by every \(d\) with \(0 < d \le n\)) and Lpf (every \(m \ge 2\) has a prime factor) are lemmas proved earlier in the same Book.
  • The last step (h) is checked by Hyperion, our own component that combines the checked steps into the stated theorem (composition, deduction, generalization, existential elimination, instances of axioms with class variables, unfolding definitions).

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.
Reviewing the whole primes Book (4 theorems on top of a small Book of arithmetic) takes about 4 seconds.

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), used as oracles: their proofs are not yet re-checked;
  4. the rules of Hyperion.

Known open points:

  • Hyperion is not yet a small, independently verified kernel. We are making it output each derivation in basic rules, so that a small checker can re-check it.
  • By default, a definition of a set-valued symbol is read as also asserting that the set exists. 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 the mark.
  • 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: 16 so far

From Freek Wiedijk's list, written by an AI (Claude) as Mathelia Books. Each link opens the Book; no account is needed.

  • #1 Irrationality of \(\sqrt{2}\) [1]
  • #3 Denumerability of the rationals [3] [3b]
  • #11 Infinitude of primes [11]
  • #23 Pythagorean triples [23]
  • #25 Schröder–Bernstein theorem [25]
  • #44 Binomial theorem [44]
  • #52 Number of subsets of a set [52a] [52b]
  • #58 Number of combinations [58]
  • #60 Bézout's theorem [60] [60b]
  • #63 Cantor's theorem [63]
  • #66 Sum of a geometric series [66]
  • #68 Sum of an arithmetic series [68a] [68b]
  • #69 Greatest common divisor algorithm [69]
  • #74 Principle of mathematical induction [74]
  • #80 Fundamental theorem of arithmetic [80]
  • #85 Divisibility by 3 rule [85]

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, but the explanatory text in the Books, the interface and the tutorials are currently in Japanese; English Books are in preparation.
We would be very glad to hear your opinions, especially on how to make the checks more trustworthy.
Contact: Tomohiko Suda [t@mshk1201.com]