Intelligent Computer Mathematics : 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5–9, 2024, Proceedings

Preface
Organization
Abstracts of Invited Speakers
	Learning from “Invisible Mathematics”
	LMFDB: The Joys and Challenges of Developing a Mathematical Database
	Contents
AI and LLM
Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations
	1 Introduction
	2 Related Works
		2.1 The DLMF Dataset
		2.2 LLMs for Data Annotation
		2.3 Prompt Engineering
	3 Experiment
		3.1 System Architecture
		3.2 Data Preparation
		3.3 Prompting
		3.4 LLM-Based Evaluation of Math Annotation
		3.5 Prompt for Annotation-Evaluation as a Binary Classification
		3.6 Prompt for Annotation-Evaluation as Multi-class Classification
	4 Performance Evaluation and Analysis
		4.1 LLM Cost
		4.2 Binary Classification
		4.3 Multi-class Classification
		4.4 Error Analysis
	5 Conclusion and Future Work
	References
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
	1 Introduction
	2 Background
	3 Encoding and Stochastic Local Search
	4 Realizability
	5 Constructions
		5.1 The Pinwheel Construction
		5.2 The Parabolic Construction
	6 Odd-Even Implication
	7 MaxSAT Verification
		7.1 MaxSAT Encoding
	8 Concluding Remarks and Future Work
	References
Using General Large Language Models to Classify Mathematical Documents
	1 Introduction
	2 An Initial Example
	3 Methods
	4 Results
	5 Discussion
	6 Future Directions
	7 Conclusions
	References
Proof Assistants
Chaining Extensionality Lemmasin Lean\'s Mathlib
	1 Introduction
	2 Chaining Extensionality Lemmas
	3 Wider applications
	4 Point-free statements
	5 Conclusion
	Acknowledgments
	References
	A Extensionality lemmas contributed by the author
		A.1 Algebra morphisms
		A.2 Linear maps
		A.3 Other morphisms
A Formalization of All Notions in the Statement of a Theorem by Deligne
	1 Introduction
		1.1 Structure of the Paper
	2 Lean Formalization
	3 Formal Proof Sketches
		3.1 Levels of Formalization
	4 Ramification Theory of Valuations
		4.1 Decompositions and Inertia Groups
		4.2 Formalizing the Frobenius Element
	5 Galois Representations
	6 Hecke Operators and Eigenforms
	7 The Final Statement
	8 Conclusion and Future Work
	References
Formalizing Finite Ramsey Theory in Lean 4
	1 Introduction
	2 Related Work
	3 van der Waerden Numbers
	4 Small Ramsey Numbers
		4.1 Graph Ramsey Numbers
		4.2 2-Color Ramsey Numbers
		4.3 Multicolor Ramsey Numbers
	5 Summary and Future Work
	References
Formalizing Pick\'s Theorem in Isabelle/HOL
	1 Introduction
	2 Related Work
	3 Our Proof Approach
		3.1 Preliminaries
		3.2 The Triangle Case
		3.3 The Convex Case
		3.4 The Non-Convex Case
		3.5 Top-Level Result
	4 Formalization Details
		4.1 Polygon Properties
		4.2 Unit Geometry
		4.3 Convex Hull Properties
	5 Conclusion and Future Work
	References
Formalizing Coppersmith\'s Method in Isabelle/HOL
	1 Introduction
	2 Related Work
	3 Coppersmith\'s Method and Formalization Overview
		3.1 Howgrave-Graham\'s Theorem
		3.2 A Stepping Stone
		3.3 Coppersmith\'s Method
	4 Formalization Details
		4.1 Type Conversion Woes
		4.2 Arithmetic
		4.3 Library Contributions
		4.4 Retrospective Generalization
	5 Conclusion and Future Work
	References
Incorporating a Database of Graphs into a Proof Assistant
	1 Introduction
	2 The House of Graphs
	3 Lean 4
	4 The Lean-HoG Library
		4.1 Interfacing with the HoG Database Through JSON
		4.2 A Computationally Efficient Formalization of Graphs
	5 Formalization of Graph Invariants
		5.1 Bipartiteness
		5.2 Connected Components
		5.3 Neighborhood Maps
		5.4 NP-Complete Invariants
	6 Loading, Visualizing and Searching Graphs
		6.1 Loading and Verifying JSON Data
		6.2 Graph Visualization
		6.3 The Search Interface
	7 Related Work
	8 Conclusion
	References
Logical Frameworks and Transformations
Reusing Learning Objects via Theory Morphisms
	1 Introduction
	2 Motivating Example
		2.1 Generalization and Exemplification
		2.2 Recontextualizing Statements
		2.3 Recontextualizing Problems
	3 Recontextualizing Learning Objects
		3.1 Presenting Views
		3.2 Recontextualizing Mathematical Statements
		3.3 Recontextualizing Problems/Solutions/Feedback
		3.4 Implementation
	4 Conclusion and Future Work
	References
Transforming Optimization Problems into Disciplined Convex Programming Form
	1 Introduction
	2 Background
		2.1 Disciplined Convex Programming
		2.2 Equivalence of Problems
		2.3 E-Graph-Based Rewriting Systems
	3 Automating Transforming Problems into DCP Form
		3.1 Problem Transformation Tactics
		3.2 Rephrasing Using Atoms
		3.3 Initialising E-Graphs
		3.4 Rewriting Until DCP Form Reached
		3.5 Generating Equivalence Explanations
		3.6 Replaying Explanations as Proofs in Lean
	4 Experiments and Discussion
	5 Related Work
	6 Conclusion and Future Work
	References
A Logical Framework Perspective on Conservativity
	1 Introduction
	2 Logics
		2.1 Abstract Logics
		2.2 The LF Type Theory
		2.3 Concrete Logics in LF
	3 Conservative Theory Morphisms
		3.1 Admissibility and Derivability
		3.2 Conservativity Between Logics
		3.3 Conservativity Within a Logic
		3.4 The Conservativity Spectrum
	4 Conservativity and Completeness
	5 Conclusion
	References
Knowledge Representation and Certication
Towards Semantic Markup of Mathematical Documents via User Interaction
	1 Introduction
	2 Background
		2.1
		2.2 The (Untyped) -calculus
	3 Laying the Groundwork
		3.1 Identifying the Required  Macros
		3.2 Parsing Formulas with parglare
	4 A Disambiguation GUI for Parsing During -ification
		4.1 Overview
	5 Grammar Generation
		5.1 Initial Approach
		5.2 Adding Types
		5.3 Using Precedence to Restrict Grammars Further
		5.4 Standardising Grammars and Parse Actions
		5.5 Current State and Issues to Address
		5.6 Alternatives
	6 Conclusion and Future Work
	References
Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts
	1 Introduction
	2 State of Research
		2.1 Vector Representations of Short Documents
		2.2 Domain Adaptation
	3 Data and Methods
		3.1 Mathematical Text Corpora
		3.2 Models
		3.3 Similarity-Related Tasks
		3.4 Classification Code Recommendation as a Downstream Task
	4 Results
		4.1 Comparison of Base- and Domain-Adapted Models
		4.2 Comparison of Fine-Tuned Models
		4.3 Evaluation of Classification Code Recommendation
	5 Summary and Discussion
	References
Generating Formally Verified Quantum Fourier Transform Algorithms
	1 Introduction
	2 Overview
		2.1 Preliminaries
		2.2 Quantum Computation
		2.3 The DFT and the QFT
		2.4 Efficient DFT and QFT Algorithms
		2.5 Generating and Compiling Correct QFT Algorithms
	3 Verified QFT Algorithm Generation
		3.1 Cooley-Tukey Factorizations for the QFT
		3.2 From Twiddle Factors to Controlled Rotations
		3.3 From Permutations to Swaps
		3.4 A DSL for QFT Algorithms
		3.5 Verified Rewrite Rules
		3.6 Searching the Algorithm Space
	4 Verified Compilation
	5 Coq Development Details
	6 Conclusion, Related Work, and Future Work
	References
Proof Search and Formalization
Partial Proof Terms in the Study of Idealized Proof Search
	1 Introduction
	2 Sequent Calculus LJT
	3 Proof Search in LJT
	4 The Natural Deduction System NJT
	5 Proof Search in NJT
	6 Focusing Versus Bidirectionality
	7 Final Remarks
	References
A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving
	1 Introduction
	2 Proposed Framework
	3 Event Trees (ETs)
	4 Functional Block Diagrams (FBDs)
	5 Cause Consequence Diagrams (CCDs)
	6 Current Status and Future Milestones
	7 Conclusion
	References
Solving Hard Mizar Problems with Instantiation and Strategy Invention
	1 Introduction: Mizar, ATPs, Hammers
		1.1 Contributions
	2 Instantiation-Based Methods
	3 Grackle: Targeted Strategy Invention for Cvc5
	4 Experiments
		4.1 Dataset
		4.2 Overview of the Experiments
		4.3 Experiments with Grackle Strategy Invention
		4.4 Experiments with Higher Time Limits
		4.5 Experiments with Clausification Methods
		4.6 Experiments on Premise Selection Slices
		4.7 Transfer to New MML
	5 Analysis of the Invented Strategies
	6 Interesting Mizar Problems Proved
	7 Conclusions and Future Work
	References
System Descriptions
Remote Verification System for Mizar Integrated with Emwiki
	1 Introduction
	2 Related Works
		2.1 Remote Verification Environements for ITPs
		2.2 Existing Utilities for Mizar
	3 Remote Development Environment
		3.1 Mizar Verification Server
		3.2 VSCode for the Web Extension
		3.3 Linking Emwiki and Remote Verification Environment
		3.4 Implemented Features
	4 Evaluation
	5 Conclusion and Future Work
	References
Oruga: Implementation and Use of Representational Systems Theory
	1 Introduction
	2 Oruga\'s Core
		2.1 Writing Oruga Documents
	3 Oruga for Inference and Transformation
		3.1 Transfer
	4 Conclusion
	References
HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover
	1 Introduction
	2 Proposed Methodology
	3 Dataset and Deep Learning Models
	4 Experimental Results
	5 Related Work
	6 Conclusion
	References
Author Index