Chapter 1　Mathelia

Mathelia is software for creating robust mathematics.
It brings together a notation for writing mathematics, a way of presenting it as a book, and a mechanism for checking proofs.
When writing mathematics, the basic workflow will be a repetition of write mathematics → check the display → have the machine review it.

★This tutorial (0_tutorial_en) is a simplified version for humans that explains only the essential parts of Mathelia. The AI tutorial (0_tutorial_AI) contains more and finer explanations.
★The explanations of the specification may sometimes lack precision or definitions; in such cases we try to give good examples instead. Also, it is not a bad idea to read actual books first, before the tutorial.
★Much of Mathelia's specification is not yet fixed. We welcome constructive feedback such as "I would like this kind of feature" from users.

1.1 Mathelia and Books

Mathematics is written in something called a Book. It is stored in a .book file and viewed with the display software.
To write your own Book, click "ファイル操作" (File operations) on the "フォルダ一覧" (Folder list) page and create a new .book (login required).
A Book usually contains data such as introductions and definitions of mathematical symbols, theorems and their proofs.
Some data, such as proofs (prf), do not appear in the display. This keeps the Book clean.

A Book must be written according to the .book file specification.
It consists of a header and a body, separated by a line ---. Each line of the header and the body begins, as a rule, with a command word.
This line (line 22 of the source) begins with the command word txt. A list of command words is in the AI tutorial.
As examples of Book features, section numbers can be assigned automatically, and other Books can be imported to inherit their data.
When a Book is compiled (when you click "表示" (Display)), it is checked whether, e.g., "there are no syntax errors and it can be displayed" and "other files can be read properly".

1.2 Reviewing a Book

When a Book is displayed, a 査読（この頁） (Review this page) button appears at the bottom of each page (it does not appear for this Book, since there is nothing to review).
Pressing it runs the introduction review (whether symbols etc. are introduced before they are used) followed by the Thm review (whether the proofs are correct).
If both give OK, the page passes. Otherwise FAIL is shown.
A FAIL in the Thm review means "the correctness of the proof could not be confirmed"; it is not a verdict that the claim is false.

Review is the most important feature of Mathelia, and it checks things literally "mechanically".
It proceeds from top to bottom, using only what is written in "the things introduced up to that point" in the Book (and in the imported Books).
Note that txt lines are explanations for humans and are ignored by the review.
Also, what is reviewed is the saved .book. Results are stored per page, and the reviews of earlier pages and of imported books are not redone; their results are reused.

1.3 Components of Mathelia

Mathelia internally has many highly independent components.
〇The DB (database) stores various data.
〇For describing mathematics, Formel, which handles Forms, and Thmel, which handles Thms, are used (see 2.book and 3.book for details).
〇The backends that review Thms (prover+, vampire+, satallax+, hyperion) can be called the heart of Mathelia.
Moreover, prover+ contains the automated theorem prover Prover9, vampire+ contains Vampire, and satallax+ contains Satallax.
〇The Mathelia core performs file operations, Book operations and so on, and also bridges the components.
To guarantee the robustness of Books, it is important to make each component robust and to keep the flow of information between components clear.