Abstract is missing.
- A Modular First Formalisation of Combinatorial Design TheoryChelsea Edmonds, Lawrence C. Paulson. 3-18 [doi]
- Beautiful Formalizations in Isabelle/NaprocheAdrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Erik Sturzenhecker. 19-31 [doi]
- Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOLAsta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen. 32-46 [doi]
- Formalization of RBD-Based Cause Consequence Analysis in HOLMohamed AbdelGhany, Sofiène Tahar. 47-64 [doi]
- Online Machine Learning Techniques for Coq: A ComparisonLiao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban. 67-83 [doi]
- Improving Stateful Premise Selection with TransformersKrsto Prorokovic, Michael Wand 0002, Jürgen Schmidhuber. 84-89 [doi]
- Towards Math Terms Disambiguation Using Machine LearningRuocheng Shan, Abdou Youssef. 90-106 [doi]
- Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem ProvingEdvard K. Holden, Konstantin Korovin. 107-123 [doi]
- Inductive Benchmarks for Automated ReasoningMárton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov. 124-129 [doi]
- A Heuristic Prover for Elementary Analysis in TheoremaTudor Jebelean. 130-134 [doi]
- Searching for Mathematical Formulas Based on Graph Representation LearningYujin Song, Xiaoyu Chen. 137-152 [doi]
- 10 Years Later: The Mathematics Subject Classification and Linked Open DataSusanne Arndt, Patrick Ion, Mila Runnwerth, Moritz Schubotz, Olaf Teschke. 153-158 [doi]
- WebMIaS on Docker - Deploying Math-Aware Search in a Single Line of CodeDávid Lupták, Vít Novotný, Michal Stefánik, Petr Sojka. 159-164 [doi]
- Learning to Solve Geometric Construction Problems from ImagesJaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic. 167-184 [doi]
- Automated Generation of Exam Sheets for Automated DeductionPetra Hozzová, Laura Kovács, Jakob Rath. 185-196 [doi]
- Gauss-Lintel, an Algorithm Suite for Exploring Chord DiagramsAbdullah Khan, Alexei Lisitsa, Alexei Vernitski. 197-202 [doi]
- A New Export of the Mizar Mathematical LibraryColin Rothgang, Artur Kornilowicz, Florian Rabe 0001. 205-210 [doi]
- A Language with Type-Dependent EqualityFlorian Rabe 0001. 211-227 [doi]
- Generating Custom Set Theories with Non-set Structured ObjectsCiarán Dunne, J. B. Wells, Fairouz Kamareddine. 228-244 [doi]
- CICM'21 Systems EntriesMartin Líska, Dávid Lupták, Vít Novotný, Michal Ruzicka, Boris Shminke, Petr Sojka, Michal Stefánik, Makarius Wenzel. 245-248 [doi]