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?
Sander Dahmen and Alain Chavarri Villarello (VU Amsterdam): Computation and formalization - case studies in computational number theory
Sander Dahmen and Alain Chavarri Villarello: Computation and formalization - case studies in computational number theory
Adrian De Lon (Universität Bonn): Natural theorem proving with Naproche-ZF
Adrian De Lon: Natural theorem proving with Naproche-ZF
Stefania Dumbrava (ENSIIE): Towards a Knowledge Graph of Formalised Mathematics
(No recording available)
Video not found
Moa Johansson (Chalmers University of Technology): Neuro-symbolic architectures for asssisting auto-formalisation and mathematical discovery
This will be an overview of recently started and aboutto-start work using neural networks to help with lemma discovery and "co-piloting" for proof assistants.
Moa Johansson: Neuro-symbolic architectures for asssisting auto-formalisation and mathematical discovery
Wenda Li (University of Edinburgh): Autoformalisation: Bridging the Gap between Informal and Formal Proofs
Wenda Li: Autoformalisation: Bridging the Gap between Informal and Formal Proofs
Dennis Müller (FAU Erlangen-Nürnberg): Injecting Formal Mathematics into LaTeX
Dennis Müller: Injecting Formal Mathematics into LaTeX
Wojciech Nawrocki (Carnegie Mellon University): Commutative diagrams in Lean (Demo)
Wojciech Nawrocki: Commutative diagrams in Lean (Demo)
Valeria de Paiva (Topos Institute) and Lucy Horowitz (University of Chicago): Three prototypes demo (Alignments)
Valeria de Paiva and Lucy Horowitz: Three prototypes demo (Alignments)
Aarne Ranta (University of Gothenburg): Informath: Informalization of Formal Mathematics
Formal mathematics, implemented in systems such as Lean, Coq, and Agda, comprises an increasing amount of mathematical knowledge. The project Informath aims to establish mappings between formal mathematics and ordinary mathematical language. This would make the results of formal mathematics more available both to mathematicians and to a wider audience. It would also help AI systems to construct formal proofs by making informal mathematics available as training material.
The core of Informath is multilingual grammars defined in GF, Grammatical Framework. Numerous earlier projects have shown the potential of GF in mapping between formal and informal languages. Building on their results and experiences, and developing some new methods, Informath aims to extend the coverage to a new level. The first concrete goal is to cover an undergraduate mathematics curriculum as defined in the MathGloss project of de Paiva and Horowitz, and convert its definitions and theorems, as formalized in Lean, to Wikipedia articles in ten human languages.
Aarne Ranta: Informath: Informalization of Formal Mathematics
Emily Riehl (Johns Hopkins University): Formalizing post-rigorous mathematics
Emily Riehl: Formalizing post-rigorous mathematics
Frederik Schaefer (Friedrich-Alexander-Universität Erlangen-Nürnberg): A Framework for Prototyping Symbolic Natural Language Understanding
Frederik Schaefer: A Framework for Prototyping Symbolic Natural Language Understanding
Frederik Schaefer (Friedrich-Alexander-Universität Erlangen-Nürnberg): Annotating and Spotting in Mathematical Corpora (concepts and tools)
Frederik Schaefer: Annotating and Spotting in Mathematical Corpora (concepts and tools)
Silvia de Toffoli (IUSS Pavia): Diagrams and Proofs
Silvia de Toffoli: Diagrams and Proofs
Josef Urban (CIIRC - CTU): Autoformalization - ten years into the game
A 20-minute talk about the various past, current and future approaches/ideas.
Josef Urban: Autoformalization - ten years into the game
Carlos Zapata-Carratala (Wolfram Institute): Hypergraph Rewriting as a Foundation for Diagrammatic Calculus
Diagrammatic and graphical reasoning has proven exceptionally powerful for the development and pedagogy of Category Theory. I will show that similar diagrammatic approaches recover all manner of algebraic structures; ranging from familiar ones such as monoid actions to exotic higher-arity ones such as semiheaps or Bhattacharya-Mesner algebras. I will present a computational foundation for diagrammatic calculus based on hypergraph rewriting together with an implementation as a Mathematica paclet available in beta for anyone to try.
Carlos Zapata-Carratala: Hypergraph Rewriting as a Foundation for Diagrammatic Calculus
Workgroup - Moderation: Mateja Jamnik (University of Cambridge) and Wenda Li (University of Edinburgh)
The role and challenges of LLMs/neural methods in autoformalisation. We will be extremely interested in inputs from experts who use sympolic methods to parse natural languages, which are very likely to complement the neural approaches.
Workgroup 1 - Moderation: Mateja Jamnik and Wenda Li