Tutorial Machine learning for the Isabelle proof assistant

            18th Conference on Intelligent Computer Mathematics
                                - CICM 2025 -
                             October 6-10, 2025
                               Brasilia, Brazil 
                     http://www.cicm-conference.org/2025

---------------------------------------------------------------------------------------- 
 ROOM: Multiuso CIC
---------------------------------------------------------------------------------------- 

The tutorial is intended to present a growing collection of libraries for
performing machine learning (ML) experiments [1, 2] on the Isabelle proof assistant.
The framework has capabilities for extracting proof data, interacting programmatically
with Isabelle, and using an ML model to attempt an Isabelle proof. The data extraction
can be done from a .thy file, a directory with several .thy files, or an organised
Isabelle development with ROOTS and ROOT files such as the Archive of Formal Proofs
(AFP). The framework provides two read-eval-print-loops (REPLs) for the interaction
with Isabelle, one in Scala and one in Python. The tutorial's objective is to showcase
the library functions to enable people to extend the framework and extract the data
suited for their purposes. It will present a data extraction example, live user proofs
of simple Isabelle facts via the Python REPL, and usage of large language models for
completing simple proofs in Isabelle. It will include a brief description of the internal
behaviour of Isabelle and the framework interaction with the prover, as well as examples
of applications using the framework.

 References

 [1] Jonathan Julián Huerta y Munive. DeepIsaHOL, November 2023.
https://github.com/yonoteam/DeepIsaHOL

[2] Jonathan Juli ́an Huerta y Munive. Snapshot of contributions from the article ”pro-
totypical data extraction and interaction for the Isabelle proof assistant”, March 2025.
https://doi.org/10.5281/zenodo.15080049

  Requirements 

Please install the following tools:
 - [Isabelle 2025](https://isabelle.in.tum.de/)
 - the [sbt (build tool)](https://www.scala-sbt.org/)
 - [Miniconda](https://www.anaconda.com/download/success) or
   [Miniforge](https://github.com/conda-forge/miniforge)

 These have been tested in Unix systems. Windows users will probably require a Unix-like
 shell, e.g. [Git Bash](https://git-scm.com/downloads).

 Please download the tutorial materials from this [link]
 (guaranteed to work until the 11th of October 2025).

  CICM Tutorial program 

**Session 1 - Introduction**: (50 minutes 14:00 - 14:50 hrs)
  * First encounter with Isabelle (10 minutes)
  * Motivation of the work (10 minutes)
    - Dream vs Duty
    - LLM prompt showcase: ChatGPT, Gemini (2.5 Flash), Claude (Opus 4.1)
    - Recent historical results
  * Introduction to the Isabelle proof assistant (10 minutes)
  * Practical session, proving theorems in Isabelle (20 minutes)

**Session 2**: (60 minutes 15:00 - 16:00 hrs)
  * Brief demo of generated tools: 
    * How to use `try_sketch` (5 minutes)
    * How to use `super_fix` (8 minutes)
    * How to use the `writer` (5 minutes)
    * Proving theorems in the `repl` (5 minutes)
    * Proving theorems with the `dfs` (7 minutes)
  * Presentation of the small experiment evaluating various LLMs (10 minutes)
  * Exercises using the project's tools (20 minutes)

**Session 3**: (50 minutes 16:30 - 17:20 hrs)
  * Brief presentation of Isabelle/ML (10 minutes)
  * Presentation of the deepIsaHOL libraries at the ML level (10 minutes)
  * Exercises (30 minutes)

**Session 4**: (50 minutes 17:30 - 18:20 hrs)
  * Project for those interested (30 minutes): 
    - e.g. get `ollama` to work with the libraries
  * Presentation in teams of the project's progress (20 minutes)

Speaker

  Jonathan Julian Huerta y Munive/ Czech Institute of Informatics, Robotics and Cybernetics, 
                                                         Czech Technical University in Prague 

Acknowledgments 
A Horizon MSCA 2022 Postdoctoral Fellowship (project acronym Deep-IsaHOL and number 101102608)
support this project.