Accepted Papers
        
        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
     
 | 
		  
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
	  
	- 
	      
News
- CICM concluded successfully!
 - CICM started!
 - Final Program published
 - Doctoral Programme established
 - Tentative Program out
 - Accepted papers announced
 - Extended deadlines
 - Invited speakers confirmed
 - First CFP is out
 - Confirmed Springer LNAI proceedings
 - Initial website online
 
Sponsors
Institutional Support