Greetings from the ATP Research Group — An Introduction to Mathelia

[Hayato Kondo]

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:

• About Mathelia: https://atp-research.com/mathelia/about/
• Tutorials for human readers: https://atp-research.com/book_collection/?folder=0_tutorial_en
• AI-oriented tutorials: https://atp-research.com/book_collection/?folder=0_tutorial_AI

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

[Steven Nguyen]

Hello, Hayato, thanks for sharing Mathelia!

I really like the links. I found https://atp-research.com/book_preview/?view=0_tutorial_en%2F1&mathelia_page=2 especially interesting.

On the question of designing a trustworthy checking process (also quite interesting), here are some informal thoughts.

I think proof systems generally have three parts:

1. Someone writes a proof in a (humanly readable) programming language.
2. A tool translates that into (computer) data structures.
3. A tool takes the data, and checks the proof.

Therefore, to show that everything is correct, we need:

1. The source language/mathematical system is sound.
2. The translation is correct.
3. The proof checker is correct.

Looking at "proofs of false" (https://gist.github.com/icecream17/9842449900f4e54636d0fcb70c641bff), Metamath issues come from (1), as all definitions and syntax are axioms.
However, we have a definition checker, so the responsibility shifts from human error in (1) to tool verification in (3).

Lean's proof checker is even more powerful, so (3) is even more difficult to show.

So (3) seems like the thing to focus on. What's very nice is that we have an opportunity to approach (3) in a new way, because we are at the start of the project.
(A similar opportunity to what Rust (programming language) did with memory safety errors).

One idea is to prove (3) incrementally.
That way, even as the proof checker grows in complexity, each individual part of the proof check has a verification.
Perhaps, Mathelia could somehow prove that Mathelia itself works. Humans could read the Book(s) showing that Mathelia works. Not sure how to design that, though.

(This is technically a circular argument, so what's even more better is two systems with proofs of themselves and each other. At this point, I'm going a bit overboard with theorizing about the future.
I think another lesson is the value of independent verifications. It's nice that Metamath has multiple independent verifiers, because it's unlikely that all of them have the same bug)

(I thought about just having AI thoroughly explain that Mathelia works, but https://atp-research.com/mathelia/about/ states

• During development, independent reviews by other AI systems found several cases where Hyperion accepted something it should not. All were fixed, and each case is kept as a regression test.

so... perhaps the only way to really guarantee this kind of thing is a proof)

Anyway, these are just some initial thoughts. I'm interested to hear others thoughts too!

(DALIA scale: D2.5 (lol))