Welcome to the ATP Research Group!
We research and develop mathematics for a new era.
By mathematics we mean the abstract mathematics studied in university mathematics departments.
Our group was officially founded in May 2024. At first, our aim was to build an "ATP (Automated Theorem Prover) for mathematics".
Today a few members work together, mainly online.
We publish our results step by step; some of them are still under development or incomplete.
Since April 2026 we have been using AI in our work.
Mathelia and AI
We are developing Mathelia, "software for creating mathematics".
Our goal is easy-to-use software that covers everything from "rich and varied mathematical expression" to "complete proofs of theorems".
The best tool for building "beautiful and robust mathematics".
In Mathelia, mathematics is written in a Book (the tutorials are Books, too).
The basic workflow is: write mathematics → check how it is displayed → have the machine review it.
Humans will enjoy the finished mathematics, but it will be AI that creates mathematics with this software.
Mathelia has been designed from the start to be used by AI as well.
After reading the tutorials and a few examples, an AI should quickly understand the specification and be able to use Mathelia.
Join us
We are looking for members who would like to work with us on research and development.
The work of university mathematics departments is bound to change greatly (even if we don't do it ... in the 2030s, refereeing papers will probably be the first task taken over by machines). Why not make it happen together?
To researchers in formal mathematics who feel constrained by type theory: here you can build real mathematics freely!?
Anyone who wants an early taste of the mathematics of a new era is very welcome, too.
Mathelia is free — just register an account and start using it! Please use it as much as you like (and, if you can, send us constructive feedback for its development).
We would also be glad to hear from anyone who would like to support our activities.
Contact: Tomohiko Suda, representative [t@mshk1201.com]