(Tentative) Program for CICM 2024
Monday
August, 5th Tuesday August, 6th Wednesday August, 7th Thursday August, 8th Friday August, 9th Andrew Granville When our computers become better at proving theorems than we are Jennifer Paulhus LMFDB: the joys and challenges of developing a mathematical database Jacques Carette Learning from 'invisible mathematics' Amber Telfer TBD
Invited Talks
10:00 -10:30 hrs
Coffee Break 1
10:30 -12:00 hrs
12:00 -14:00 hrs
Lunch Break
14:00 -15:30 hrs
15:30 -16:00 hrs
Coffee Break 2
16:00 -17:30 hrs
FVPS
FVPS
Lurch
Lurch
WiFM, MathUI
WiFM, MathUI
WiFM, MathUI
AI and LLM
Proof Assistants #1
Doctoral Programme
Logical Frameworks and Transformations
System and Project Descriptions
Knowledge Representation and Certification
Proof Assistants #2
Proof Search and Formalization
Conference Dinner
09:00-10:00 hrs
A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving
Incorporating a database of graphs into a proof assistant
Formalizing Pick's Theorem in Isabelle/HOL
Generating Formally Verified Quantum Fourier Transform Algorithms
HOL4PRS: Proof Recommendation System for HOL4 Theorem Prover
Using General Large Language Models to Classify Mathematical Documents
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Developing a Remote Verification System in Mizar and Its Integration with the Emwiki Platform
A formalization of all notions in the statement of a theorem by Deligne
Re-Using Learning Objects via Theory Morphisms
Formalizing Coppersmith's Method in Isabelle/HOL
Transforming Optimization Problems into Disciplined Convex Programming Form
Formalizing Finite Ramsey Theory in Lean 4
A Logical Framework Perspective on Conservativity
Oruga: Implementation and Use of Representational Systems Theory
Partial proof terms in the study of idealized proof search
Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations
On modelling similarity of short mathematical texts
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
Towards semantic markup of mathematical documents via user interaction
Chaining extensionality lemmas in Lean's Mathlib
Differential Galois Theories of Difference Equations of Order Two on Elliptic Curves
Autoformalization of number theory in Lean
Domain-specific Type Theory for Finite Mathematics
Formal Analysis of Multibody Systems using Theorem Proving
Topics in Cylindrical Algebraic Decompositions
|
CICM 2024
17th Conference on Intelligent Computer Mathematics
August 5 - 9, 2024
Montréal, Québec, Canada
You must enable JavaScript to use this site