Mathlib4 Help

This is a list of the output of #help command of mathlib4. see GitHub Page!

This is heavily inspired by haruhisa-enomoto/mathlib4-all-tactics.

This web page is automatically updated by GitHub Action.

How to install dependencies

# activate virtual environment
py -m venv .venv
.venv\Scripts\activate

# install dependencies
pip install -r requirements.txt

How to generate markdown file

First, install Lean and Python 3.10, and then run the following commands:

./scripts/build.ps1
python3 script.py

How to serve website

python -m mkdocs serve