Lean 4 Project Template

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

Install Lean 4

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

Use this Template

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.

Clone this Repository

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

Customize this Template

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:

   bashCopy
   python3 --version

3. Verify your Pip installation by running:

   bashCopy
   pip3 --version

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

   bashCopy
   cd path/to/your/project

5. Execute the customization script by running:

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

Configure GitHub Pages

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.

The workflow deploy-pages.yml builds the Jekyll site in
website, runs the
upstreaming-dashboard-action,
and deploys the result to GitHub Pages.

Repository Layout

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.
    • build-project.yml defines the workflow for building
      the Lean project on pushes, pull requests, and manual triggers. This is a minimalistic build
      workflow which is not necessary if you decide to generate a blueprint (see instructions below)
      and can be manually disabled by clicking on the Actions tab, selecting Build Project
      in the left sidebar, then clicking the horizontal triple dots (⋯) on the right,
      and choosing Disable workflow.
    • deploy-pages.yml defines the workflow for building
      and deploying the GitHub Pages site, including generation of the upstreaming dashboard.
    • create-release.yml: defines the workflow for creating a new Git tag and GitHub release when the lean-toolchain file is updated in the main branch. Ensure the following settings are configured under Settings > Actions > General > Workflow permissions: "Read and write permissions" and "Allow GitHub Actions to create and approve pull requests".
    • update.yml is the dependency
      update workflow to be triggered manually by default. [It's not documented yet, but it will be soon.]
  • 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 the
    current version of 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.
• website contains the Jekyll files for the GitHub Pages homepage that displays the
  upstreaming dashboard.
• .gitignore specifies files and folders to be ignored by Git.
  and environment.
• CODE_OF_CONDUCT.md should contain the code of conduct for the project.
• 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.

Blueprint

0. Selected Collaborative Projects

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

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

1. Install Dependencies

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

2. Install LeanBlueprint Package

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

bashCopy
pip install leanblueprint

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

bashCopy
pip install -U leanblueprint

3. Configure Blueprint

To set up the blueprint for your project, run:

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

consoleCopy
Proceed with blueprint creation? [y/n]

Respond affirmatively with y to the following prompt:

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

Respond negatively with n to the following prompt:

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

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

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

Selected Projects Using this Template

If you have used this template to create your own Lean project and would like to share it with the community, please consider opening a PR to add your project to this list:

• Infinity Cosmos by Emily Riehl et al.
• Analytic Number Theory Exponent Database by Terence Tao et al.
• Equational Theories by Terence Tao et al.
• Groupoid Model of Homotopy Type Theory by Sina Hazratpour et al.
• Soundness of FRI by Bolton Bailey et al.
• Weil's Converse Theorem by Chris Birkbeck et al.
• Proofs from THE BOOK by Moritz Firsching et al.
• Automata Theory by Stefan Hetzl et al.
• Dirichlet Nonvanishing by Chris Birkbeck et al.
• Seymour's Decomposition Theorem by Ivan Sergeyev et al.
• Spectral Theorem by Oliver Butterley and Yoh Tanimoto.
• NeuralNetworks by Matteo Cipollina.
• ABC Exceptions by Bhavik Mehta et al.
• Sphere Packing in 8 Dimensions by Maryna Viazovska et al.
• LeanBridge by Chris Birkbeck et al.