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

---------------------------------------------------------------------------------------- 
         
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

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.