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
(Pending permission to publish the recording)
Video not found
Adrian De Lon (Universität Bonn): Natural theorem proving with Naproche-ZF
(The recording has not been edited, yet)
Video not found
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)
(Pending permission to publish the recording)
Video not found
Valeria de Paiva (Topos Institute) and Lucy Horowitz (University of Chicago): Three prototypes demo (Alignments)
(Pending permission to publish the recording)
Video not found
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
(The recording has not been edited, yet)
Video not found
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)
(Pending permission to publish the recording)
Video not found
Silvia de Toffoli (IUSS Pavia): Diagrams and Proofs
(Pending permission to publish the recording)
Video not found
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