AI4M Tutorials

This repository contains tutorials on AI for Mathematics (AI4M) topics, focusing on LLM-driven automated theorem proving in Lean.

Workshop Context

These tutorials were developed for the MATRIX-MFO Tandem Workshop: Machine Learning and AI for Mathematics held on September 22-26, 2025.

Getting Started

Lean Environment Setup

This project requires Lean 4 and Mathlib 4 at version v4.22.0 for compatibility.

1. Install Lean 4 and Elan by following the instructions at Install Lean. Make sure elan binary is in your PATH.

2. Obtain the Mathlib 4 repository at the specified version. We have included a submodule for Mathlib 4. To initialize and update the submodule, run:

   git submodule update --init --recursive
   cd mathlib4
   git checkout v4.22.0

   Then build Mathlib 4:

   lake exe cache get
   lake build

Python Environment Setup

This project uses uv to configure the Python environment:

1. Install uv, see link for your operating system.

2. Set up the environment with:

   uv sync

Start your journey

Just begin with the tutorials/build_your_prover.ipynb notebook. Click select kernel in the top right corner and choose the uv kernel named ai4m-tut. Install any missing packages if prompted.

Development Status

These tutorials are under active development and will be continuously updated based on user feedback and evolving best practices.