最初の投稿

Subject: Greetings from the ATP Research Group — An Introduction to Mathelia

Hello everyone,

My name is Hayato Kondo, and I am writing on behalf of the ATP Research Group, a small research group in Japan working on automated theorem proving and the formalization of mathematics. I’d like to introduce a project we are developing called Mathelia.

Mathelia is a system for writing mathematics in structured documents called Books, which contain definitions, theorems, assumptions, and proofs. We are exploring how automated theorem provers and AI can help create formal mathematics.

For those who are interested, here are a few links:

Mathelia and Metamath take different approaches to formalizing and verifying mathematics. In Mathelia, proof steps are checked using external automated theorem provers together with our own component, Hyperion. Mathelia is still under development, and independent verification of proofs remains an important open issue.

We would be very interested in learning more about the work of the Metamath community and exchanging ideas about formal mathematics, proof verification, and the role of AI in mathematical research.

In particular, we would welcome your thoughts on what lessons we might draw from Metamath’s approach to proof verification as we work toward making Mathelia’s checking process more trustworthy.

We hope this can be the beginning of an ongoing exchange. Thank you for reading, and we look forward to hearing from you.

Best regards,

Hayato Kondo
ATP Research Group

10/20への返信

Hello Steven,

Thank you very much for your thoughtful reply. Your three-part view (soundness of the logic, correctness of the translation, correctness of the checker) is a very useful way for us to organize the problem.

On your last point, we agree. The AI reviews and the regression tests built from them reduce errors, but they are not a guarantee. They tell us where Hyperion went wrong, not that it is now right.

As a concrete first step toward a checkable checker: Hyperion already records each derivation (which rule, which checked steps and which theorems it used). What is missing is a small independent program that re-checks these records against a fixed set of rules. We think this would let us trust a small checker instead of Hyperion as a whole. The translation from our notation to the provers' input would remain a separate question.

May we ask two things?

  • In Metamath, several independent verifiers exist. What has been the most practical way to keep them independent: different authors, different languages, or something else?
  • For a small checker like the one above, would you start by fixing the rule set in a written specification, or by writing the checker first and deriving the specification from it?

Thank you again. We look forward to continuing the discussion.

Best regards,
Hayato Kondo
ATP Research Group