Repository files navigation

This repository contains the resources for the Lean demo session of my talkAn 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 Codewebsite.
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 theExtensions sidebar by clicking on the square icon on the left panel.
   • Search forLean 4 in the search bar and install theLean 4 extension.

   

2. Access the Lean 4 Setup Guide:

   • Create a new text file by selectingFile > New Text File or using the keyboard shortcut (Ctrl + N on Windows/Linux orCmd + N on macOS).
   • Click on the$\forall$-symbol located in the top right corner of the window.
   • From the dropdown menu, selectDocumentation… > 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 theGitHub documentationon cloning repositories.

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

cd LeanCHANGE/lake exe cache get