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 Naproche and Mizar;
- 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.
Speakers and topics
| Moa Johansson | Chalmers | AI for Mathematical Discovery: Symbolic, Neural and Neuro-Symbolic Methods |
| Josef Urban | CIIRC CTU Prague | AI in Formal Mathematics |
| Roussanka Loukanova | Institute of Mathematics and Informatics of the Bulgarian Academy of Sciences | Approaches to Computational Grammar of Natural Language |
| Julie Cailler | Loria, University of Lorraine, Inria | Tableau-based Automated Theorem Proving, Goéland |
| Martin Suda | CIIRC CTU Prague | Superposition-based Automated Theorem Proving, Vampire |
| Stephan Schulz | DHBW Stuttgart | Superposition-based Automated Theorem Proving, E |
| David Cerna | Czech Academy of Sciences | Anti-unification |
| Adam Naumowicz | University of Bialystok | Mizar |
| Peter Koepke Adrian De Lon |
University of Bonn | Naproche |
| Adam Dingle | Charles University | Natty |
| Paul-André Melliès | IRIF, Inria | MALINCA (MAthematicae LINgua franCA) project presentation and overview |
| Philippe de Groote | Inria Nancy |
Registration and application for funding
The school is free of charge. Please register before attending by filling out the registration form and sending it to adelon@uni-bonn.de.
For registration, please tell us your full name and provide your CV.
Select applicants will have their travel costs reimbursed through the COST Action EuroProofNet. The application deadline was April 27th. The deadline for funding applications was April 27th; notifications for funding will be sent out by April 30th.
If you did not receive a reply to your registration or funding application within a few days, please try submitting it again (if possible from a different email address).
Location
The lectures and tutorials will take place in the Lipschitz-Saal at the Mathematics Center of the University of Bonn. The address is:
Endenicher Allee 6053115 Bonn
Germany
Bonn can be reached by train via Bonn Hbf or by airplane via Cologne Bonn Airport. Bonn's central station (Bonn Hbf) is right in the city centre, a 1 km walk or 5 minute bus ride from the Mathematics Center.
Accommodation
Participants will make their own accommodation arrangements. There are many hotels around the city centre of Bonn. We recommend making a refundable booking as early as possible.
Questions and support
Please contact Adrian De Lon at adelon@uni-bonn.de for any questions.