Intelligent Computer Mathematics
Description
This book constitutes the refereed proceedings of the 18th International Conference on Intelligent Computer Mathematics, CICM 2025, held in Brasilia, Brazil, during October 6-11, 2025.
The 24 full papers were presented in this volume were carefully reviewed and selected from 34 submissions. They were organized in the following topical sections as follows : Automated Reasoning; Formal Libraries; Logical and Linguistic Foundations; Mathematical Knowledge Management; Neural Language Models; and Proof Assistants and Formalizations.
More details
Other editions
Additional editions
Content
.- Automated Reasoning .
.- Hammering Higher Order Set Theory.
.- Synthesis Benchmarks for Automated Reasoning.
.- Automated Symmetric Constructions in Discrete Geometry.
.- Formal Libraries .
.- Growing Mathlib: Maintenance of a Large Scale Mathematical Library.
.- Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
.- Supporting Maintenance of Formal Mathematics with Similarity Search.
.- Logical and Linguistic Foundations .
.- Graded Quantitative Narrowing.
.- Equational Generalization Problems with Atom-Variables.
.- Extending Flexible Boolean Semantics for the Language of Mathematics.
.- A Formal Definition of an Algorithm Suitable for Parsing the Language of Mathematics.
.- Mathematical Knowledge Management .
.- Reaping the Benefits of Modularization in Flexiformal Mathematics by GFbased AST Transformations.
.- Semantic Authoring in a Flexiformal Context - Bulk Annotation of Rigorous Documents.
.- Michael Kohlhase and Jan Frederik Schaefer Lightweight Realms.
.- Indexing and Retrieval in a Heterogeneous Formal Library.
.- Neural Language Models .
.- Exploring Proof Autoformalization with Mistral on Herald.
.- Boosting Math Problem Solving in Small LLMs via Ensembles.
.- Proof Assistants and Formalizations .
.- Formalizing a Classification Theorem for Low-Dimensional Solvable Lie Algebras in Lean.
.- Certified Algorithms for Numerical Semigroups in Rocq.
.- Formalizing the Solow Model in Naproche.
.- Formalizing MLTL Formula Progression in Isabelle/HOL.
.- Formalising Fairness in the Assignment Problem with Ordinal Preferences in Isabelle/HOL.
.- A PVS Library on the Infinitude of Primes.
.- Vector Graphics through Category Theory.
.- A Lean-Based Language for Teaching Proof in High School.
