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

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