EuroProofNet School on
Natural Formal Mathematics
About the school
The international EuroProofNet School on Natural Formal Mathematics will be held from the 3rd to the 5th of June 2025 at the Mathematics Centre in Bonn, Germany. The programme will include talks on topics related to natural formal mathematics and hands-on tutorials. Related topics include
- proof assistants with an emphasis on naturalness, such as Mizar and Naproche;
- natural language understanding of mathematical texts: processing of natural language (controlled or free) with grammar-based or machine-learning-based approaches;
- AI in formal mathematics: autoformalization, autoinformalization, neural conjecturing, etc.;
- automated theorem provers: their theoretical foundations, implementation, and efficient use, as well as machine-learning-based methods in automated theorem proving;
- proof automation generally;
- experimental projects aiming to make existing proof assistants more natural;
- linguistics of mathematics.
Participants: David Alfaya, Santiago Arambillete, Antonella Bilotta, Julie Cailler, David Cerna, Garett Cunningham, Philippe de Groote, Adrian De Lon, Adam Dingle, Moa Johansson (remotely), Elliot Kaplan, Peter Koepke, Simon Korswird, Gwenaëlle Léon, Roussanka Loukanova, Adam Naumowicz, Auguste Poiroux, Mehmet Tahir Sandikkaya, Stephan Schulz, Marcel Schütz, Martin Suda, Josef Urban, Franziskus Wiesnet, Joshua Wirtz.
Schedule
| Tuesday, June 3rd | ||
| 10:00 | Peter Koepke (University of Bonn) |
Welcome & Naproche |
| 11:00 | Josef Urban (CIIRC CTU Prague) |
AI in Formal Mathematics |
| 12:00 | Lunch Break | |
| 13:30 | Julie Cailler (Loria, University of Lorraine, Inria) | Tableau & Goéland |
| 14:30 | Adam Naumowicz (University of Białystok) |
Mizar |
| 15:30 | Coffee and Tea Break | |
| 16:00 | Hands-on Session (Naproche resources) | |
| Wednesday, June 4th | ||
| 9:00 | Stephan Schulz (DHBW Stuttgart) |
Superposition & E |
| 10:00 | Moa Johansson (Chalmers) |
AI for Mathematical Discovery: Symbolic, Neural and Neuro-Symbolic Methods |
| 11:00 | Martin Suda (CIIRC CTU Prague) |
Efficient Neural Clause-Selection Reinforcement |
| 12:00 | Adrian De Lon (University of Bonn) |
Naproche-ZF |
| 13:00 | Lunch Break | |
| 14:30 | Hands-on Session | |
| 15:30 | Coffee and Tea Break (outdoors, weather permitting) | |
| 16:00 | Hands-on Session | |
| Thursday, June 5th | ||
| 10:00 | Roussanka Loukanova (Bulgarian Academy of Sciences) |
Approaches to Computational Grammar of Natural Language |
| 11:00 | David Cerna (Czech Academy of Sciences) |
Anti-unification: The Other Operation |
| 12:00 | Lunch Break | |
| 13:30 | Adam Dingle (Charles University) |
Natty |
| 14:30 | Philippe de Groote (Inria Nancy) |
MALINCA (MAthematicae LINgua franCA) project presentation |
| 15:30 | Coffee and Tea Break | |
| 16:00 | Open Session / Discussion | |
Registration and application for funding
The school was free to attend and participants were able to apply for reimbursement of travel expenses through the COST Action EuroProofNet. The deadline for funding applications was April 27th and notifications were sent out on April 30th.
Location
The lectures and tutorials took place in the Lipschitz-Saal at the Mathematics Center of the University of Bonn. The address is:
Endenicher Allee 6053115 Bonn, Germany
This lecture hall is the main hall of the mathematics building and is located centrally on the first floor. If you go up the stairs outside and enter the building through its main entrance, you will find the lecture hall right across the foyer.