Chapter 2　The Position of Mathelia

2.1 Mathematics, AI and Proof Assistants

Since the start of 2026, there has been a stream of news such as "AI solved an open problem in mathematics" and "AI formalized the proof of a major theorem".
Most of these take the form AI finds a proof, and a proof assistant such as Lean checks its correctness. Having machines guarantee correctness is itself already possible at a large scale.
On the other hand, the proofs produced this way are becoming enormous and are no longer something people read and understand. Mathematicians have raised voices saying "what matters in mathematics is the understanding of concepts and insight".
Mathelia is also software in which machines check correctness, but its aim is a little different. It is strongly conscious of humans looking at mathematics made by AI.
And it can be said to be closer to Mizar and Metamath than to Lean.
A. Trybulec of Mizar wrote proofs in a language close to ordinary mathematical prose, and built a library that collects theorems as "articles".
N. Megill of Metamath valued a small, simple mechanism by which anyone can check every step of a proof.
I feel that our philosophy is similar to theirs. Had they been born in the present age of advanced AI, they might have developed something like this software.

2.2 Mathelia and AI

Mathelia is built on the assumption that AI, not only humans, will use it. An AI tutorial (0_tutorial_AI) is also provided, and AI reads it to write Books.
When humans use it, too, the basic approach is to ask AI about what you do not understand. AI will explain the meaning of symbols, how to read theorems, why a proof does not go through, and so on, in line with the Book and the workings of Mathelia.
Even elementary things, such as renaming a Book file, are safer left to AI. The Book might be imported by other Books.

And in the future, it is likely that AI will create Books, and humans will appreciate what has been made.
AI chooses definitions, arranges theorems, searches for proofs, and revises the Book until the review is ALL OK.
Humans savor the choice of construction and notation and the flow of the proofs as a single work.

What is beautiful mathematics? It is self-contained, and one can see what is shown from what. There are no hidden assumptions, and the correctness of the proofs of the theorems is checked by the machine under the written specification.
Not only must the flow be completely visible, it must also be visible cleanly.
Mathelia has many features for this. It enables concise and diverse mathematical expressions, and automated theorem provers (Prover9, Vampire, Satallax) fill in the fine inferences of proofs.
Making full use of the many features, especially getting proofs through, is something AI does far better than humans.
By swapping the assumptions one can make any number of books with different constructions; let us leave the enormous trial and error to AI as well.
I hope that, with the help of AI, more works of mathematics that people can appreciate will come about.

★Many examples are already prepared.
As of October 2026, several of the 100 mathematical theorems have been made into books. Each book aims at one theorem and is kept to a size whose review finishes in a few seconds.