最初の投稿案
Subject: Mathelia: a library of mathematical "books" checked by Prover9/Vampire — feedback welcome
Hello everyone,
I am Tomohiko Suda from the ATP Research Group, a small group in Japan.
I am not good at English, so please forgive any awkward phrasing.
For the past few years we have been developing Mathelia, a system for
writing mathematics as "books" whose theorems are machine-checked.
Like Metamath and Mizar, we build mathematics by accumulating
definitions, theorems and proofs, and we have learned a lot from both
projects. I would like to introduce Mathelia here and ask for your
opinions.
Main ideas:
- Formulas are written in our own notation (Formel), and translated by
fixed rules into first-order logic or a two-sorted (set/class)
first-order logic. - Each proof step is sent to an automated prover (Prover9, or Vampire
for the two-sorted case). Steps are combined by our own small
meta-reasoning component (Hyperion: composition, deduction,
generalization, existential elimination, etc.). - Our long-term vision is that AI agents write most of the proofs, and
humans read the books as works of art: short, self-contained, and
easy to follow.
So far we have formalized 16 theorems from Freek Wiedijk's
"Formalizing 100 Theorems" list (e.g. the infinitude of primes,
the Schroeder-Bernstein theorem, the binomial theorem).
We know that trust is the central question. At present a theorem is
accepted if Prover9/Vampire proves every step and Hyperion accepts the
combination. Hyperion is not yet a small verified kernel. We are
working on having it output a derivation in basic rules that can be
re-checked independently. We also keep a list of known open issues.
An English introduction page is here: [URL]
I would be grateful for any comments, especially on:
- How would you evaluate a system that relies on external provers
like Prover9 for individual steps? - What would you want to see first in order to trust or try such a
system?
Thank you for reading.
Tomohiko Suda
ATP Research Group