You must enable JavaScript to use this site
  • (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
    09:00-10:00 hrs
    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
    Mohamed Abdelghany, Adnan Rashid and Sofiene Tahar A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving
    Andrej Bauer, Katja Berčič, Gauvain Devillez and Jure Taslak Incorporating a database of graphs into a proof assistant
    Sage Binder and Katherine Kosaian Formalizing Pick's Theorem in Isabelle/HOL
    Patrick Brinich and Jeremy Johnson Generating Formally Verified Quantum Fourier Transform Algorithms
    Nour Dekhil, Adnan Rashid and Sofiène Tahar HOL4PRS: Proof Recommendation System for HOL4 Theorem Prover
    Patrick Ion and Stephen Watt Using General Large Language Models to Classify Mathematical Documents
    Jan Jakubuv, Mikolas Janota and Josef Urban Solving Hard Mizar Problems with Instantiation and Strategy Invention
    Toshiki Kai, Yuta Teruya and Kazuhisa Nakasho Developing a Remote Verification System in Mizar and Its Integration with the Emwiki Platform
    Michail Karatarakis A formalization of all notions in the statement of a theorem by Deligne
    Michael Kohlhase and Marcel Schütz Re-Using Learning Objects via Theory Morphisms
    Katherine Kosaian, Yong Kiam Tan and Kristin Rozier Formalizing Coppersmith's Method in Isabelle/HOL
    Ramon Fernández Mir, Paul Jackson, Siddharth Bhat, Andrés Goens and Tobias Grosser Transforming Optimization Problems into Disciplined Convex Programming Form
    David Narváez, Congyan Song and Ningxin Zhang Formalizing Finite Ramsey Theory in Lean 4
    Florian Rabe A Logical Framework Perspective on Conservativity
    Daniel Raggi, Gem Stapleton, Aaron Stockdill, Grecia Garcia Garcia, Peter Cheng and Mateja Jamnik Oruga: Implementation and Use of Representational Systems Theory
    José Espírito Santo and Ana Catarina Sousa Partial proof terms in the study of idealized proof search
    Ruocheng Shan and Abdou Youssef Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations
    Christian Steinfeldt and Helena Mihaljević On modelling similarity of short mathematical texts
    Bernardo Subercaseaux, John Mackey, Marijn Heule and Ruben Martins Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
    Luka Vrečar, Joe Wells and Fairouz Kamareddine Towards semantic markup of mathematical documents via user interaction
    Eric Wieser Chaining extensionality lemmas in Lean's Mathlib
    Matthew Babbitt Differential Galois Theories of Difference Equations of Order Two on Elliptic Curves
    Michail Karatarakis Autoformalization of number theory in Lean
    Jure Taslak Domain-specific Type Theory for Finite Mathematics
    Kubra Aksoy Formal Analysis of Multibody Systems using Theorem Proving
    Corin Lee Topics in Cylindrical Algebraic Decompositions
  • News

    • 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







Privacy policy and legal information
Last modified: July 16 2024 08:35:41 CEST