This repository contains the resources for the Lean demo session of my talk An Invitation to Blueprint-Driven Formalisation of Mathematical Research in Lean presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

VS Code is the recommended IDE for working with Lean 4. To install VS Code, follow these steps:

1. Visit the official VS Code website.
2. Download the latest version of VS Code for your operating system (Windows, macOS, or Linux).
3. Follow the installation instructions provided on the website to complete the setup process.

Once the installation is complete, you can proceed with configuring VS Code for Lean 4 development.

To install Lean 4, please follow these instructions:

1. Install the Lean 4 Extension in VS Code:

   • Open VS Code.
   • Navigate to the Extensions sidebar by clicking on the square icon on the left panel.
   • Search for Lean 4 in the search bar and install the Lean 4 extension.

   

2. Access the Lean 4 Setup Guide:

   • Create a new text file by selecting File > New Text File or using the keyboard shortcut (Ctrl + N on Windows/Linux or Cmd + N on macOS).
   • Click on the $\forall$-symbol located in the top right corner of the window.
   • From the dropdown menu, select Documentation… > Docs: Show Setup Guide.

   

3. Follow the Instructions in the Setup Guide:

   • Carefully read and follow the instructions provided in the Lean 4 setup guide to complete the installation process.

   

To clone this repository, run the following command:

git clone /~https://github.com/pitmonticone/LeanCHANGE.git

For detailed instructions, please refer to the GitHub documentation on cloning repositories.

After successfully cloning the repository, navigate into the project directory and execute the following command to retrieve the necessary cached dependencies:

cd LeanCHANGE/
lake exe cache get