Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era – Simons Foundation
The Simons Foundation today announced a new set of initiatives that will help the mathematics community navigate the rapid rise of artificial intelligence in t…
Simons Foundation 
Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era – Simons Foundation
The Simons Foundation today announced a new set of initiatives that will help the mathematics community navigate the rapid rise of artificial intelligence in t…
Subject: Introducing Mathelia — An environment for AI to develop formal mathematics
Dear Simons Foundation Mathematics and Physical Sciences Team,
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 would like to introduce Mathelia, a web-based environment we are developing.
Mathelia is designed to support AI as an active author of mathematics. Its central concept is the Book: a self-contained mathematical document containing definitions, theorems, assumptions, and proofs. Our aim is to enable people and AI to develop different Books that explore independent choices of definitions, exposition, and proofs, even when they address the same mathematical results.
The system currently checks proof steps using external automated theorem provers together with our own component, Hyperion. Mathelia is still under development, and making its checking process independently verifiable remains an important task.
We read with great interest about the Simons Foundation’s initiative to help mathematicians navigate the AI era. Our work explores how mathematics written with AI can be organized, checked, understood, and developed further, while preserving room for different mathematical approaches.
Could you suggest researchers or initiatives with whom it would be useful for us to exchange ideas? We would also welcome any thoughts on how this work might relate to the Foundation’s current activities.
A brief introduction to Mathelia is available here:
https://atp-research.com/mathelia/about/
Thank you for your time and consideration.
Best regards,
Hayato Kondo
ATP Research Group
claude(11/06)
宛先: mps@simonsfoundation.org
件名: Introducing Mathelia, and a question about eligibility for the Math+AI program
Dear Simons Foundation Mathematics and Physical Sciences Team,
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 would like to introduce Mathelia, a web-based environment we are developing.
Mathelia is designed to support AI as an active author of mathematics. Its central concept is the Book: a self-contained mathematical document containing definitions, theorems, assumptions, and proofs. Our aim is to enable people and AI to develop different Books that explore independent choices of definitions, exposition, and proofs, even when they address the same mathematical results.
The system currently checks proof steps using external automated theorem provers together with our own component, Hyperion. Mathelia is still under development, and making its checking process independently verifiable remains an important task.
We read with great interest about the Simons Foundation's $15M initiative to help mathematicians navigate the AI era. Our work explores how mathematics written with AI can be organized, checked, understood, and developed further, while preserving room for different mathematical approaches.
We understand that the Targeted Grants to Math+AI Institutes program is open to established institutes and research centers, which our group is not. We would therefore be grateful for your guidance on the following:
- Could a small research group or company take part in the Math+AI effort in some other way, for example as a partner of an eligible institute or university?
- The announcement mentions an open call for proposals. Is it planned, and do you expect to publish its eligibility and timeline soon?
- Anthropic and OpenAI will provide AI tools and computing resources to a select group of researchers. Is this limited to researchers supported by the Foundation, or can others be considered?
- Would work on building and evaluating tools for AI-assisted formal mathematics fall within the scope of the program?
We would also welcome suggestions of researchers or initiativel for us to exchange ideas.
A brief introduction to Mathelia is available here:
https://atp-research.com/mathelia/about/
Thank you for your time and consideration.
Best regards,
Hayato Kondo
ATP Research Group