最初の投稿

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

The second 100 (11/10)

Subject: Seeking feedback on a proposed sequel to Freek100

Hello everyone,

I would like to invite you to comment on a project I have been working on: The Second 100 — an independent, unofficial sequel to Freek100.

The current list of 100 theorems is available here: https://atp-research.com/mathelia/sequel_freek100/

This is a working draft, and the selection is still open to discussion. I would particularly appreciate:

  • Suggestions for additions and replacements;
  • Suggestions of theorems with especially ingenious or beautiful proofs;
  • Information about which of these theorems are already formalized in set.mm (ideally with references), and opinions on which of the remaining ones would be particularly interesting or challenging to formalize.

The aim is to create an enjoyable collection, in the spirit of Freek100, that also showcases some of the surprising ideas in mathematics.

Of the 41 theorems suggested to Freek Wiedijk as missing from the list on his page, 14 are included in our current selection.

Several AI systems have helped us develop and review the list, but I would especially value feedback from human mathematicians and members of the formalization community.

All comments, suggestions, and criticisms are welcome!

Thank you.

10/30への返信案(claude)

Hi Alex,

Thank you for the pointers — "Metamathelia" made me smile.

I agree that checking a system with a different system, in a different metalanguage, is worth more than checking it from inside. Hyperion and our translation layers are written in PHP, so a checker for recorded derivations would be most convincing if it were written separately, in a different language, from a written specification of the rules. We have not started this yet: Hyperion does not yet produce a complete record of the theorems, rules and side conditions it used, and that record has to come first. I mention the checker as the direction we are heading, not as something we have.

Your literate programming suggestion is interesting. Mathelia's Books already keep prose, definitions, theorems and proofs in one document, but we have not applied the same approach to the implementation or to the rule specification. Keeping the rule set, its rationale and the checker's code together in one document is something we are considering; we have not decided on it.

A question, if you have experience with this: for a small checker of this kind, would you write the specification first (as in the Lean4lean / MetaRocq style) or the implementation first and extract the specification from it?

Thanks again for the suggestions.

Best regards,
Hayato Kondo
ATP Research Group

上の返信案をchatgptで添削

Hi Alex,

Thank you for the pointers — "Metamathelia" made me smile.

I agree that checking a system with a different system, in a different metalanguage, is worth more than checking it from inside. Hyperion and our translation layers are written in PHP, so a checker for recorded derivations would be most convincing if it were written separately, in a different language, from a written specification of the rules.

We have not started this yet: Hyperion does not yet produce a complete record of the theorems, rules and side conditions it used, and that record has to come first. I mention the checker as the direction we are heading, not as something we have.

Your literate programming suggestion is interesting. Mathelia's Books already keep prose, definitions, theorems and proofs in one document, but we have not applied the same approach to the implementation or to the rule specification. Keeping the rule set, its rationale and the checker's code together in one document is something we are considering; we have not decided on it.

A question, if you have experience with this: would you recommend starting with a written specification and then implementing the checker against it, or starting with a simple implementation and gradually formalizing its specification? I would also be interested in how you see approaches such as Lean4lean and MetaCoq in this context.

Thanks again for the suggestions.

Best regards,

Hayato Kondo ATP Research Group

claude 返信案(11/14)

Subject: Re: Seeking feedback on a proposed sequel to Freek100

Hi Xander,

Thank you for the pointer to 1000+. I had not seen it before, and it is a useful comparison for what we are doing.

As I understand it, 1000+ takes the opposite approach to ours. It is broad: it takes everything on Wikipedia's List of Theorems, and its main purpose is to track formalization status. Our "Second 100" is deliberately small and curated. We want a list that, like Freek100, can serve as a shared benchmark and is something people can actually read and discuss. The selection criteria are:

  • foundational and/or surprising theorems
  • statements that can be turned into a readable book (a clear claim, statable assumptions, a followable proof)
  • a spread over sixteen areas
  • a rough ★–★★★ difficulty rating

So the two projects are complementary rather than competing. 1000+ could serve as a good cross-reference for our list. For each of our 100, it would be helpful to link to the corresponding 1000+ entry, if there is one, and to see which systems have formalized it.

I have two questions, if you know the answers.

  1. Does 1000+ record per-system formalization status (set.mm, Mathlib, Isabelle/AFP, HOL Light, Lean, etc.) with references? If so, we would like to use it to fill in the set.mm column.
  2. Is there a good way to propose corrections or additions? I could not find a contribution process on the about page and assume it is via the GitHub repository.

For the original request, we would still be glad to hear from anyone on three things:

  • theorems you would add or replace
  • theorems whose proofs are especially clever or beautiful
  • which of the remaining ones are already in set.mm (with references), and which you think would be interesting or hard to formalize there

The current draft is at https://atp-research.com/mathelia/sequel_freek100/

Best regards,
Hayato Kondo
ATP Research

Greetings from the ATP Research Group — An Introduction to Mathelia 返信案(11/14)

Hi Jim,

Thank you for the answers, and for the pointer to the definition rules in conventions.html.

Your advice to focus on definition checkers rather than verifiers is helpful. Everything in a Mathelia Book builds on its definitions, so we will read that section and compare it with how Mathelia handles definitions.

A test suite of definitions that must be rejected also seems like a good first step, since it can be built before any independent checker exists. If the Metamath community has a collection of such cases, we would be glad to learn from it.

Thanks again,

[name]