Workshop: Bridging between informal and formal

Monday

Aarne Ranta

Dennis Müller

Tuesday

Peter Koepke

Frederik Schaefer

Valeria de Paiva and Lucy Horowitz

Wojciech Nawrocki

Wednesday

Silvia de Toffoli

Stefania Dumbrava

Frederik Schaefer

Josef Urban

Sander Dahmen and Alain Chavarri Villarello

Thursday

Wenda Li

Carlos Zapata-Carratala

Moa Johansson

Natarajan Shankar

Workgroup - Moderation: Mateja Jamnik and Wenda Li

Friday

Emily Riehl

Adrian De Lon

Stefania Dumbrava (ENSIIE): Towards a Knowledge Graph of Formalised Mathematics

(No recording available)

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.

Peter Koepke (University Bonn): A Natural Language Formalization of Perfectoid Rings in Naproche

Wenda Li (University of Edinburgh): Autoformalisation: Bridging the Gap between Informal and Formal Proofs

Dennis Müller (FAU Erlangen-Nürnberg): Injecting Formal Mathematics into LaTeX

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.

Frederik Schaefer (Friedrich-Alexander-Universität Erlangen-Nürnberg): A Framework for Prototyping Symbolic Natural Language Understanding

Natarajan Shankar (SRI International Computer Science Laboratory): Cueology of Proof

Josef Urban (CIIRC - CTU): Autoformalization - ten years into the game

A 20-minute talk about the various past, current and future approaches/ideas.

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.

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.