Intro
Preface
Organization
Invited Talks
Logics at Work, and Some Challenges for Computer Mathematics
Induction in Saturation-Based Reasoning
Doing Number Theory in Weak Systems of Arithmetic
Contents
Formalizations
A Modular First Formalisation of Combinatorial Design Theory
1 Introduction
2 Background
2.1 Mathematical Background
2.2 Isabelle and Locales
3 The Basic Design Formalisation
3.1 Pre-designs
3.2 Basic Design Properties
3.3 Basic Design Operations
4 The Block Design Hierarchy
4.1 Restricting Block Size
4.2 Balanced Designs

4.3 T-Designs
4.4 Uniform Replication Number
4.5 BIBDs and Proofs
4.6 BIBD Extensions
5 Extending the Formalisation
5.1 Resolvable Designs
5.2 Group Divisible Designs
5.3 Design Isomorphisms
5.4 Graph Theory
6 The Modular Approach
6.1 The Formal Design Hierarchy
6.2 The Little Theories Approach
6.3 Notational Benefits
6.4 Reasoning on Locales
6.5 Limitations
7 Conclusion and Future Work
References
Beautiful Formalizations in Isabelle/Naproche
1 Introduction
2 Naproche, ForTheL, and LaTeX
3 Example: Cantor's Theorem

4 Example: König's Theorem
5 Example: Euclid's Theorem
6 Example: Furstenberg's Topological Proof
7 Example: The Knaster-Tarski Theorem
8 Outlook
References
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
1 Introduction
2 Related Work
3 Implication and Falsity
3.1 Language
3.2 Wajsberg 1937
3.3 Wajsberg 1939
3.4 Shortest Axiom
4 Disjunction and Negation
4.1 Language
4.2 Rasiowa 1949
4.3 Russell 1908 and Bernays 1926
4.4 Whitehead and Russell 1910
5 Challenges and Benefits
6 Conclusion
References

Formalization of RBD-Based Cause Consequence Analysis in HOL
1 Introduction
2 Preliminaries
2.1 RBD Formalization
2.2 ET Formalization
3 Cause-Consequence Diagram Formalization
3.1 Formal CCD Modeling
3.2 Formal CCD Analysis
4 Conclusion
References
Automatic Theorem Proving and Machine Learning
Online Machine Learning Techniques for Coq: A Comparison
1 Introduction
1.1 Contributions
2 Tactic and Proof State Representation
3 Prediction Models
3.1 Locality Sensitive Hashing Forests for Online k-NN
3.2 Online Random Forest
3.3 Boosted Trees

4 Experimental Evaluation
4.1 Split Evaluation
4.2 Chronological Evaluation
4.3 Evaluation in Tactician
4.4 Feature Evaluation
5 Related Work
6 Conclusion
References
Improving Stateful Premise Selection with Transformers
1 Introduction
2 Data
3 Experiments
4 Conclusion and Future Work
References
Towards Math Terms Disambiguation Using Machine Learning
1 Introduction
2 Related Works
2.1 The DLMF Dataset
2.2 Part-of-Math Tagger
2.3 Word Sense Disambiguation in NLP
2.4 Machine Learning Models
2.5 Math Language Processing
3 The Dataset