Automating Mathematical Reasoning: Interactions Between Proof Assistants, Computer Algebra Systems (CAS) and Generative AI
Session Organizers:
Session Abstract:
Proof assistants such as Lean, Isabelle, and Rocq are enabling
unprecedented levels of certified mathematical reasoning and
collaboration among mathematicians. This momentum is further
strengthened by advances in computer algebra systems (e.g., SageMath,
Mathematica, Maple) for efficient symbolic computation, and by recent
generative AI technologies that facilitate rapid prototyping of both
informal and formal proofs. This session focuses on recent progress at
the intersection of proof assistants, computer algebra
systems/algorithms, and generative AI aimed at automating mathematical
reasoning. We welcome contributions on topics such as algebraic
specification and formal semantics of symbolic algorithms, as well as
AI-guided and generative methods for interactive theorem proving. The
session aims to foster technical discussion on interoperability,
correctness, and scalability, highlighting frameworks that integrate the
deductive rigour of proof assistants with the computational power of CAS
and the heuristic strengths of modern AI systems.
Session Talks:
tba