Proceedings Papers
This volume contains the proceedings of the International Congress on
Mathematical Software (ICMS) 2026, held in Waterloo, Ontario, Canada, from
July 20 to 23, 2026, hosted jointly by Wilfrid Laurier University and the
University of Waterloo. ICMS is a biennial meeting devoted to all aspects of
mathematical software, bringing together developers and users of computer
algebra systems, numerical software, and formal proof tools. The 2026 edition
featured sessions on automating mathematical reasoning through interactions
between proof assistants, computer algebra systems, and generative AI;
algebraic solvers for polynomial systems; computational category theory;
parallel methods, AI, and applications of computer algebra in physics;
mathematics in Lean; high-performance computer algebra; computing methods in
(dual) quaternion matrix/tensor computation; software for enumerative and
analytic combinatorics; biological applications of computer algebra; design
and implementation of computer algebra systems and software; mathematical
knowledge management; computational methods in combinatorial algebra and
geometry; symbolic-numeric computation; and a general session.
Automating Mathematical Reasoning: Interactions Between Proof Assistants, Computer Algebra Systems (CAS) and Generative AI
- Automated Tactics for Polynomial Reasoning in Lean~4
Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi
[pdf]
- Formalizing the Wu-Ritt Characteristic Set Method in
Lean 4,
Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, Lihong Zhi
[pdf]
- A Macaulay2-Lean interface for proofs in Lean,
Matthew Ballard, Anton Leykin, Michael E. Stillman, Damiano Testa, Douglas A. Torrance, Jay Yang
[pdf]
- Proof-of-work protocols for AI-generated solutions in mathematics,
Erich L. Kaltofen
[pdf]
Computational Category Theory
- Relational to RDF Data Migration by Query Co-Evaluation - Extended Abstract,
Ryan Wisnesky, Daniel Filonik
[pdf]
- Implementing the biset category of finite groups,
Mohamed Barakat, Marc Talleux, Fabian Zickgraf
[pdf]
Mathematics in Lean
- Reflections on Trusting Lean,
Lorenzo Bresolin, Marcello Mamino
[pdf]
- Progress in Formalizing Sphere Packing in Dimension 8,
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska
[pdf]
- Formalizing Quasi-Borel Spaces in Lean 4,
Anthony Vandikas, Kiarash Sotoudeh
[pdf]
High-Performance Computer Algebra
- Parallelizing the F4 Algorithm,
Roman Pearce
[pdf]
- Fast GPU Linear Algebra via Compile Time Expression Fusion,
Ryan R. Curtin, Marcus Edel, Conrad Sanderson
[pdf]
- Multiple Double Arithmetic on NVIDIA Tensor Cores,
Howard Chen, Jan Verschelde
[pdf]
- Remarks about complexity and implementation of bivariate Gr\"obner bases,
Xavier Dahan
[pdf]
- Parallel Computation of the Power Series Solutions to
Algebraic and Differential Equations,
Greg Alejandro Solis-Reyes, Marc Moreno Maza, Alexander Brandt
[pdf]
- Groebner.jl: Fast Gr\"obner Tracing in Julia,
Alexander Demin
[pdf]
- Sparse Polynomial Multiplication on Chiplet-based Architectures,
Miriam Okutuo, Alexander Brandt
[pdf]
- Parallel Computations of Transversal Hypergraphs,
Adam Murdock Gale, Marc~Moreno~Maza
[pdf]
Computing Methods in (Dual) Quaternion Matrix/Tensor
- Subresultants of Several Ore Polynomials,
Jiaqi Meng, Jing Yang
[pdf]
- Efficient Computational Framework for Matrix Equations over n-Generalized Quaternions,
Lei Shi, Yang Zhang
[pdf]
- Lower and upper bounds of quaternion tensor ranks ,
K.M.D.H. Kulathunga, Yang Zhang
[pdf]
Software for Enumerative and Analytic Combinatorics
- CombOL: a Library for Practical Enumeration and Boltzmann Sampling of Combinatorial Classes,
Casper Asbjørn Eriksen, Daniel Merkle
[pdf]
- SagePeriods: A SageMath Package for Fast Diagonals of Rational Functions,
Stephen Melczer, John Hunn Smith
[pdf]
- nth: Open-Source Generic Combinatorial (Un)ranking via the Symbolic Method,
Marcos Tomaszewski, Gustavo Zambonin, Jean Everson Martina, Ricardo Cust\'odio
[pdf]
- Quasi-polynomials, Z-polyhedra and parametric integer linear programming,
Rui-Juan Jing, Yuzhuo Lei, Marc~Moreno~Maza, Chirantan~Mukherjee
[pdf]
Biological Applications of Computer Algebra
- Computational and Algebraic Questions in Causal Inference,
Alex Markham, Erin E.~Gabriel, Michael C.~Sachs
[pdf]
Design and Implementation of Computer Algebra Systems and Software
- The Ax Computer Algebra System,
Roman Pearce
[pdf]
- Simplified Index Rules for Integrating Tensor Index Notation into Programming Languages with Static Type Systems,
Satoshi Egi
[pdf]
- Using an ML Model for Handwritten Digit Recognition in GeoGebra,
Mitsushi Fujimoto
[pdf]
- Implementing sparse rational function interpolation in Maple with application to solving parametric linear systems,
Michael Monagan, Mantej Sokhi, Archit Srivastava
[pdf]
- Implementing p-adic numbers in Macaulay2 using its foreign function interface and FLINT,
Douglas A. Torrance
[pdf]
Mathematical Knowledge Management
- Scaling Accessible Mathematics on arXiv: HTML Conversion and MathML 4,
Deyan Ginev, Bruce R. Miller, Brian Caruso, Jacob Weiskoff, Jeff Sank
[pdf]
- Extend your Math with Semantics and Services,
Dennis Müller, Michael Kohlhase
[pdf]
- How to Build a Formal Mathematical Library,
William M. Farmer
[pdf]
- NuFrameIT: Serious Games via Computation and Reasoning,
Stefanie Heim, Michael Kohlhase, Silas Kuder, Florian Rabe
[pdf]
- MathBases: Indexing and Creating Mathematical Databases,
Katja Ber\v{c}i\v{c}, Edgar Costa, David Roe
[pdf]
Computational Methods in Combinatorial Algebra and Geometry
- Fast Isotopy Computation for T-Curves,
Zoe Geiselmann, Michael Joswig, Lars Kastner, Konrad Mundinger, Sebastian Pokutta, Christoph Spiegel, Marcel Wack, Max Zimmer
[pdf]
- Enumeration of Coherent Matching Fields Modulo Symmetry,
Xavier Allamigeon, Yiyuan Chen
[pdf]
- Euclidean Distance Degrees in Macaulay2,
William Huang, Jose Israel Rodriguez
[pdf]
Symbolic-Numeric Computation
- Mixed volume and ramification points of sparse homotopies,
Joseph Cummings, Jonathan D. Hauenstein
[pdf]
- Eigensolvers for polynomial roots and tensor decomposition,
Enrica Barrilli, Bernard Mourrain
[pdf]
- Holonomic gradient method --- a symbolic-numeric method to evaluate integrals with parameters,
Nobuki Takayama,Takaharu Yaguchi, Yi Zhang
[pdf]
- Belyi map verification using certified path tracking,
Alexandre Guillemot, John Voight
[pdf]
- Low-Memory Numerical Certification,
Paul Breiding, Taylor Brysiewicz, David K. Johnson
[pdf]
- Approximating Periodic Orbits with Algebraic Curves and Related Minimal Problems,
Ruiqi Huang, Anton Leykin
[pdf]
- Mathematical Software for the Evaluation of Distribution Functions of Quadratic Forms of Gaussian Random Variables,
Denis Arzelier, Florent Bréhard, Mioara Joldes
[pdf]
- Taylor Tube Method for Validated IVP,
Bingwei Zhang, Chee Yap
[pdf]
- Heuristic Acceleration of Near-Optimal Polynomial Root-Finders,
Soo Go, Won Geun Kim, Victor Y. Pan
[pdf]
- Computing Periodic Golay Pairs Using SAT Solvers,
Bernhard Andraschko, Ilias Kotsireas, Martin Kreuzer
[pdf]
- Fast Rational Univariate Representation via Gaussian Elimination,
Alexander Demin, Fabrice Rouillier
[pdf]
General topics
- Arc-Length Parameterized Interpolating Splines,
Dafna K. Matsegora, Stephen M. Watt
[pdf]
- WebAssembly for browser-based scientific computing: neural simulation and Xiangqi (chinese chess),
Martin D. Pham
[pdf]
- A Database of Binary Septics and Applications to Galois Theory and Coding,
Jurgen Mezinaj
[pdf]