Abstract is missing.
- Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA ProjectLawrence C. Paulson. 3-15 [doi]
- Never Trust Your Solver: Certification for SAT and QBFMartina Seidl. 16-33 [doi]
- Evasiveness Through Binary Decision DiagramsJesús Aransay, Laureano Lambán, Julio Rubio 0001. 37-52 [doi]
- Nominal AC-MatchingMauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes Sobrinho. 53-68 [doi]
- Category Theory in Isabelle/HOL as a Basis for Meta-logical InvestigationJonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott. 69-83 [doi]
- Learning Support Systems Based on Mathematical Knowledge ManagementMarc Berges, Jonas Betzendahl, Abhishek Chugh, Michael Kohlhase, Dominic Lohr, Dennis Müller 0001. 84-97 [doi]
- Isabelle Formalisation of Original Representation TheoremsMarco B. Caminati. 98-112 [doi]
- Teaching Linear Algebra in a Mechanized Mathematical EnvironmentRobert M. Corless, David J. Jeffrey, Azar Shakoori. 113-129 [doi]
- Highlighting Named Entities in Input for Auto-formulation of Optimization ProblemsNeeraj Gangwar, Nickvash Kani. 130-141 [doi]
- Formalization Quality in IsabelleFabian Huch, Yiannos Stathopoulos. 142-157 [doi]
- Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy ProblemAabid Seeyal Abdul Kharim, T. V. H. Prathamesh, Shweta Rajiv, Rishi Vyas. 158-173 [doi]
- Morphism Equality in Theory GraphsFlorian Rabe 0001, Franziska Weber. 174-189 [doi]
- Towards an Annotation Standard for STEM Documents - Datasets, Benchmarks, and SpottersJan Frederik Schaefer, Michael Kohlhase. 190-205 [doi]
- Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi MethodMohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin. 206-221 [doi]
- Multiple-Inheritance Hazards in Dependently-Typed Algebraic HierarchiesEric Wieser. 222-236 [doi]
- CoProver: A Recommender System for Proof ConstructionEric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar. 237-251 [doi]
- Proving an Execution of an Algorithm Correct?James Harold Davenport. 255-269 [doi]
- Proving Results About OEIS Sequences with WalnutJeffrey O. Shallit. 270-282 [doi]
- ProofLang: The Language of arXiv ProofsHenry Hammer, Nanako Noda, Christopher A. Stone. 285-290 [doi]
- True Crafted Formula Families for Benchmarking Quantified Satisfiability SolversSimone Heisinger, Martina Seidl. 291-296 [doi]
- An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine LearningJohn Hester, Briland Hitaj, Grant O. Passmore, Sam Owre, Natarajan Shankar, Eric Yeh. 297-302 [doi]
- VizAR: Visualization of Automated Reasoning Proofs (System Description)Jan Jakubuv, Cezary Kaliszyk. 303-308 [doi]
- Extending Numeric Automation for Number Theory Formalizations in MizarAdam Naumowicz. 309-314 [doi]
- Extracting Theory Graphs from Aldor LibrariesFlorian Rabe 0001, Stephen M. Watt. 315-320 [doi]