Workshop: Bridging between informal and formal

Dates: July 8 - 12, 2024
Venue: HIM lecture hall, Poppelsdorfer Allee 45, Bonn
Organizers: Kevin Buzzard (London), Jacques Carette (Hamilton), Valeria de Paiva (Berkeley), Michael Kohlhase (Erlangen), Josef Urban (Praha)

Description:

This workshop focusses on the man / machine interaction in Formal Mathematics.  Presently, most formal proofs are practically unreadable by average mathematicians, as they appear like specialized computer code. Can this be improved by making proof languages "readable", or by automatic translation from formalizations into a natural language-like format?

On the other hand, can the formalization process be made as natural for mathematicians as typing texts into LaTeX, so that formalization and proof-checking happen concurrently without appreciable extra effort? Can AI-methods help with translations from informal to formal? Could (AI) translation techniques translate parts of the vast corpus of existing mathematical texts into formalizations?

Trimester Program guests, who were invited and have confirmed to be at HIM during the period of this workshop, are eligible to attend this event.