This repository contains a template for blueprint-driven formalization projects in Lean 4.

This is the video recording of the tutorial talk I presented at the Hausdorff Research Institute for Mathematics (HIM) in Bonn.

It was designed for mathematicians at all levels to provide a comprehensive introduction to the design, management, and implementation of blueprint-driven formalisation projects in Lean, with almost no prerequisite knowledge of Git, GitHub, continuous integration systems, and other technical tools.

Ensure that you have a functioning Lean 4 installation. If you do not, please follow the Lean installation guide.

To create a new repository using this template, ensure you are on the correct repository page (LeanProject) and then follow these steps:

1. Click the Use this template button located at the top right of the repository page.
2. Click the Create a new repository button.
3. Select the account or organization where you want to create it, choose a name for the new repository, and click the Create repository button.

To set up GitHub Pages for your repository, follow these steps:

1. Go to the Settings tab of your repository.
2. In the left sidebar, click on the Pages section.
3. In the Source dropdown, select GitHub Actions.

To clone this repository to your local machine, please refer to the relevant section of the GitHub documentation here.

The template repository is organized as follows (listing the main folders and files):

• .github contains GitHub-specific configuration files and workflows.
  • workflows contains GitHub Actions workflow files.
    • lint.yml is the style lint workflow triggered on push and pull request events.
    • update.yml is the dependency update workflow triggered manually by default.
  • dependabot.yml is the configuration file to automate CI dependency updates.
• .vscode contains Visual Studio Code configuration files
  • extensions.json recommends VS Code extensions for the project.
  • settings.json defines the project-specific settings for VS Code.
• Project should contain the Lean code files.
  • Mathlib should contain .lean files with declarations missing from existing Mathlib developments.
  • ForMathlib should contain .lean files with new declarations to be upstreamed to Mathlib.
  • Example.lean is a sample Lean file.
• scripts contains scripts to update Mathlib ensuring that the latest version is fetched and integrated into the development environment.
• .gitignore specifies files and folders to be ignored by Git. and environment.
• CONTRIBUTING.md should provide the guidelines for contributing to the project.
• lakefile.toml is the configuration file for the Lake build system used in Lean projects.
• lean-toolchain specifies the Lean version and toolchain used for the project.

To tailor this template to your specific project, follow these steps:

1. If you don't have a Python environment, you can install one by following the instructions in the Python installation guide.
2. Verify your Python installation by running:

   python3 --version

3. Verify your Pip installation by running:

   pip3 --version

4. Ensure your terminal is in the project directory by running the following command:

   cd path/to/your/project

5. Execute the customization script by running:

   python3 scripts/customize_template.py NewProject

   where NewProject must be replaced by the name of your project.

The script customize_template.py will automatically rename the project folder and update the necessary files and configurations to match the new project name.

• Fermat's Last Theorem for Exponent 3 led by Riccardo Brasca.
• Polynomial Freiman-Ruzsa Conjecture led by Terence Tao.
• Fermat's Last Theorem led by Kevin Buzzard.
• Carleson Operators on Doubling Metric Measure Spaces led by Floris van Doorn.
• Bonn Collaborative Formalization Seminar Series in Analysis led by Floris van Doorn.
• Prime Number Theorem and More led by Alex Kontorovich.
• Infinity Cosmos led by Emily Riehl.
• Analytic Number Theory Exponent Database led by Terence Tao.
• Groupoid Model of Homotopy Type Theory led by Sina Hazratpour.
• Equational Theories led by Terence Tao.

For more examples of completed and ongoing Lean projects and libraries, please see the Lean Reservoir.

To install the necessary dependencies, follow the instructions in the PyGraphViz installation guide.

Assuming you have a properly configured Python environment, install LeanBlueprint by running:

pip install leanblueprint

If you have an existing installation of LeanBlueprint, you can upgrade to the latest version by running:

pip install -U leanblueprint

To set up the blueprint for your project, run:

leanblueprint new

Then, follow the prompts and answer the questions as you like, except for a few specific questions which should be answered as indicated below to ensure compatibility with this template.

Respond affirmatively with y to the following prompt:

Proceed with blueprint creation? [y/n]

Respond affirmatively with y to the following prompt:

Modify lakefile and lake-manifest to allow checking declarations exist? [y/n] (y)

Respond affirmatively with y to the following prompt:

Modify lakefile and lake-manifest to allow building the documentation? [y/n] (y):

If you want to generate a Jekyll-based home page for the project, respond affirmatively with y to the following prompt:

Do you want to create a home page for the project, with links to the blueprint, the API documentation and the repository? [y/n]:

Respond affirmatively with y to the following prompt:

Configure continuous integration to compile blueprint? [y/n] (y):

For more details about the LeanBlueprint package and its commands, please refer to its documentation.

After configuring the blueprint, please wait for the GitHub Action workflow to finish. You can keep track of the progress in the Actions tab of your repository.

• Infinity Cosmos led by Emily Riehl.
• Analytic Number Theory Exponent Database led by Terence Tao.
• Equational Theories led by Terence Tao.
• Groupoid Model of Homotopy Type Theory led by Sina Hazratpour.
• Soundness of FRI led by Bolton Bailey.
• Weil's Converse Theorem led by Chris Birkbeck.
• Proofs from THE BOOK led by Moritz Firsching.
• Automata Theory led by Stefan Hetzl.