Intelligent Computer Mathematics: 16th International Conference, CICM 2023, Cambridge, UK, , September 5–8, 2023 Proceedings

This book constitutes the refereed proceedings of the 16th International Conference on Intelligent Computer Mathematics, CICM 2023, held in Cambridge, UK, in September 2023. The 14 full papers, 2 project/survey papers, 6 short papers, and 1 tool paper presented were carefully reviewed and selected from a total of 37 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teaching and geometric reasoning, and logic and systems, among other topics. Preface Organization Abstracts of Invited Talks Progress on Proof System Interoperability How Can We Make Trustworthy AI? Contents Invited Talks Large-Scale Formal Proof for the Working Mathematician—Lessons Learnt from the ALEXANDRIA Project 1 Introduction 2 A Brief Prehistory of the Formalisation of Mathematics 3 ALEXANDRIA: Warmup Formalisation Exercises 4 Advanced Formalisations 5 Seriously Deep Formalisation Projects 5.1 Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions 5.2 Additive Combinatorics 5.3 Other Formalisation Projects 5.4 On Legibility of Formal Proofs 6 Library Search and Machine Learning Experiments 7 Evaluation 8 Conclusions References Never Trust Your Solver: Certification for SAT and QBF 1 Introduction 2 Preliminaries 3 Certification for SAT 3.1 CDCL-Based SAT Solving 3.2 Certificates Based on Resolution 3.3 Certificates Based on Reverse Unit Propagation 3.4 Certificates Based on Resolution Asymmetric Tautologies 4 Certification for QBF 4.1 Certificates Based on Q-Resolution 4.2 Certificates Based on Exp+Res 4.3 Certificates Based on QRAT 5 Conclusion References Regular Papers Evasiveness Through Binary Decision Diagrams 1 Introduction 2 Preliminaries 2.1 Boolean Functions, BDDs, Evasiveness 2.2 Alexander Dual, Dismantling 3 Ligneous Boolean Functions 4 Dismantlable Implies Ligneous 5 Formalisation in Isabelle/HOL 6 Conclusions and Further Work References Nominal AC-Matching 1 Introduction 2 Background 2.1 Nominal Terms, Permutations and Substitutions 2.2 Freshness and -Equality 2.3 Solution to Quintuples and Additional Notation 3 Algorithm 3.1 Functions chooseEq and decompose 3.2 Handling Freshness Constraints - Functions freshSubs? and fresh? 3.3 The Function applyACStep 3.4 An Example of First-Order AC-Unification and How We Adapted It to the Nominal Setting 4 Formalisation 4.1 Nice Inputs 4.2 Termination 4.3 Soundness 4.4 Completeness 5 Towards a Nominal AC-Unification Algorithm 6 Conclusion and Future Work References Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation 1 Introduction 2 Category Theory from a Free Logic Perspective 2.1 Free Logic and Its SSE into Isabelle/HOL 2.2 Formalization of Axiomatic Category Theory 3 Formalization of Elementary Topoi 4 Formalization of the Categorical Model of IMLL 4.1 IMLL and Its Categorical Model 4.2 Isabelle/HOL Formalization of the IMLL Categorical Model 5 Conclusions References Learning Support Systems Based on Mathematical Knowledge Management 1 Introduction 2 Assembling an Educational Dialogue 3 The VoLL-KI ALeA System 3.1 The Learning Object Server (LOS) 3.2 The Learner Model Server (LMS) 3.3 The Course Fragment Server (CFS) 4 The Rhetoric/Didactic Model 5 Conclusion, Evaluation, and Future Work References Isabelle Formalisation of Original Representation Theorems 1 Introduction 2 Event Structures and Full Graphs 2.1 Event Structures 2.2 Full Graphs 3 Connecting ES's and FGs 4 Formalisation and Verification: Introduction 5 Formalisation and Verification: Proof Structure for bijection 6 Formalisation and Verification: Proof Structure for representation 6.1 Proof of main2 6.2 Proof of main1 7 The Formalisation Process 8 Conclusions References Teaching Linear Algebra in a Mechanized Mathematical Environment 1 Overview 1.1 Active Learning in a Mechanized Environment 1.2 How to Teach with Technology 1.3 What to Teach, When Technology Is Involved 1.4 Outline of the Paper 2 Tools 2.1 Proprietary Tools 2.2 Free Software 2.3 Visualization 2.4 Programming 3 Topics 3.1 The Language of Matrices 3.2 Parametric Linear Algebra 3.3 Factoring Matrices 3.4 Determinant 3.5 Eigenvalues and Floating-Point 3.6 Special Matrices 3.7 Proof and Formal Methods 4 Assessment 5 Promoting Agreement on Syllabus Change 6 Concluding Remarks References Highlighting Named Entities in Input for Auto-formulation of Optimization Problems 1 Introduction 2 Related Work 3 Proposed Approach 4 Experiments 4.1 Dataset 4.2 Training Details 4.3 Evaluation Metrics 4.4 Results 4.5 Error Analysis 4.6 Ablation Study 5 Datasets Without Labeled Named Entities 5.1 Noisy Named Entities 5.2 Results 5.3 Generality of the Proposed Approach 6 Conclusion References Formalization Quality in Isabelle 1 Introduction 2 Code Quality in Software Engineering 3 Analysis of Formalization Quality 3.1 Maintenance Effort 3.2 Lints and Formalization Structure 3.3 Comparison with Perceived Quality 4 Discussion 4.1 Limitations 4.2 Future Work 1 Graph Features 2 Large Language Model Analysis References Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem 1 Introduction 2 Mathematical Preliminaries 3 Formalisation of Basic Constructions 4 The Word and Conjugacy Problems for Free Groups 5 The Nielsen-Schreier Theorem 6 Discussion 7 Related Works 8 Conclusions and Future Work References Morphism Equality in Theory Graphs 1 Introduction and Related Work 2 Preliminaries 2.1 LF-Expressions 2.2 Theory Graphs in MMT 3 Propositional Equality of LF-Expressions 4 Propositional Equality of MMT-Morphisms 5 Case Studies 6 Conclusion and Future Work References Towards an Annotation Standard for STEM Documents 1 Introduction 2 Related Work 3 Accumulating Semantic Information 4 The Document Corpus 5 Annotations as RDF Triples 5.1 Annotation Targets 5.2 Annotation Bodies 5.3 Discontinuous Targets 5.4 Querying Annotations with SPARQL 6 SpotterBase 6.1 JSON Serialization of Annotations 6.2 Document Narrative Model 6.3 Document Pre-processing 7 Datasets, Spotters and Experiences 8 Conclusion, Ongoing and Future Work References Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method 1 Introduction 2 Overview of Iterative Methods and Our Proof Structure 3 Parametric Models and Proofs; Important Constants 4 Forward Error Bound for Dot Product 5 Jacobi Forward Error 6 Convergence Guarantee: Absence of Overflow 7 An Efficient and Correct C Program 7.1 Sparse Matrix-Vector Multiply 7.2 Jacobi Iteration 8 The Main Theorems, Residuals, and Stopping Conditions 9 Related Work 10 Conclusion and Future Work References Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies 1 Introduction 2 Types of Structure Inheritance 2.1 Flat Structures 2.2 Nested Structures 3 Typeclasses Depending on Typeclasses 3.1 Equality of Typeclass Arguments 3.2 Inequality of Typeclass Arguments 3.3 Impact of the Inheritance Strategy 3.4 Other Examples in mathlib 4 Mitigation Strategies 4.1 Perform -Reduction of Structures in the Kernel 4.2 Use ``Flat'' Inheritance 4.3 Carefully Select ``Preferred'' Paths 4.4 Ban Non-root Structures in Dependent Arguments 5 Implications for Packed Structures 6 Related Work 7 Conclusion References CoProver: A Recommender System for Proof Construction*-1pc 1 Introduction 2 CoProver Overview 3 Data Generation 4 Command Prediction 5 Lemma Retrieval 6 Experiments and Results 6.1 Command Prediction 6.2 Lemma Retrieval 7 Related Work 8 Conclusions References Project and Survey Papers Proving an Execution of an Algorithm Correct? 1 Introduction 2 SAT Solving 3 Polynomial Factorisation 3.1 Univariate Polynomials 3.2 Comments on Research Question 2 3.3 Multivariate Polynomials 4 Integration ``in Closed Form'' 4.1 What Exactly Do We Mean? 4.2 The Algebraic Theory of Integration ch17Ritt1948,ch17Ritt1950 4.3 Liouville's Principle ch17Liouville1835,ch17Ritt1950 4.4 Risch's Idea ch17Risch1969a 4.5 Producing a Proof of 5 Real Geometry and Quantifier Elimination 5.1 Real Quantifier Elimination 5.2 The [Sampled] Cylindrical Algebraic Decomposition Algorithm 5.3 Challenges with Cylindrical Algebraic Decomposition 5.4 Proving Cylindrical Algebraic Decomposition Correct 5.5 Solving Problem 6 via CAD 6 Cylindrical Algebraic Coverings (CAC) 6.1 The Algorithm 6.2 How Might a CAC Be Verifiable? 7 Conclusions References Proving Results About OEIS Sequences with Walnut 1 Introduction 2 What is Walnut? 3 An Example 4 A More Serious Example 5 How Does Walnut Work? 6 Another Example 7 Proving Conjectures by Guessing the Automaton 8 Other Capabilities of Walnut 9 Common Mistakes When Using Walnut 10 Tips for Using Walnut 11 A Final Word References System and Dataset Descriptions ProofLang: The Language of arXiv Proofs 1 Introduction 2 Constructing the ProofLang Corpus 3 Experimenting with the Corpus 3.1 Identifying Collocations 3.2 Testing the NLTK Part-of-Speech Tagger 4 Conclusion and Future Work References True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers 1 Introduction 2 Preliminaries 3 Two Families of True Formulas 4 Evaluation 5 Conclusion References An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning 1 Introduction 2 The Proposed MetiTarski Dataset Setup 2.1 MetiTarski Datasets 2.2 Feature Engineering and Labeling 2.3 Models 3 Evaluation 4 Conclusion References VizAR: Visualization of Automated Reasoning Proofs (System Description) 1 Introduction 2 VizAR: The Proof Navigator 3 Conclusions and Future Work References Extending Numeric Automation for Number Theory Formalizations in Mizar 1 Introduction 2 Number Theory Automations 3 New Directive: requirements INT_D 3.1 Functors div and mod 3.2 Functors lcm and gcd 3.3 Predicate divides 3.4 Attribute prime 4 Conclusions References Extracting Theory Graphs from Aldor Libraries 1 Background 2 Modeling Aldor in MMT 3 Conclusions and Future Work References System Entry GeoGebra Discovery Reference Author Index