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