### Initialize a New Blueprint

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Run the interactive setup command within an existing Lean 4 project directory.

```bash
# Navigate to your Lean project root (must have lakefile.lean or lakefile.toml)
cd my-lean-project

# Ensure you have committed changes and configured GitHub remote
git status  # Should show clean working directory

# Run interactive blueprint creation
leanblueprint new

# Example interactive session:
# Project title [My formalization project]: Fermat's Last Theorem
# Lean library name [FLT]: FLT
# Author: Kevin Buzzard \and Richard Taylor
# URL of GitHub repository [https://github.com/user/flt]:
# URL of project website [https://user.github.io/flt]:
# URL of project API documentation [https://user.github.io/flt/docs]:
# LaTeX document class [report]: book
# LaTeX paper [a4paper]: a4paper
# Show buttons allowing to show or hide all proofs [Y/n]: Y
# Table of contents depth [3]: 3
# Split file level [0]: 1
# Per html file local table of contents depth [0]: 2
# Proceed with blueprint creation? [y/N]: y
# Modify lakefile to allow checking declarations exist? [Y/n]: Y
# Modify lakefile to allow building documentation? [Y/n]: Y
# Do you want to create a home page? [y/N]: y
# Configure continuous integration? [Y/n]: Y
# Commit to git repository? [y/N]: y
# Commit message [Setup blueprint]: Initial blueprint setup
```

--------------------------------

### Preview Blueprint Locally

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Start a local web server to view the compiled HTML blueprint.

```bash
# Start local server (tries ports 8000-8009)
leanblueprint serve

# Output:
# Serving http://localhost:8000/
# Press Ctrl-c to interrupt.

# Open browser to http://localhost:8000 to view blueprint
```

--------------------------------

### Install Lean Blueprint

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Install the package and required system dependencies on Debian/Ubuntu systems.

```bash
# Install system dependencies (Debian/Ubuntu)
sudo apt install graphviz libgraphviz-dev

# Install leanblueprint package
pip install leanblueprint

# Upgrade to latest version
pip install -U leanblueprint
```

--------------------------------

### Initialize a new blueprint

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Run this command within your project folder to start the interactive configuration process for a new blueprint.

```bash
leanblueprint new
```

--------------------------------

### Install leanblueprint via pip

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Installs the leanblueprint package and its dependencies, including plasTeX.

```bash
pip install leanblueprint
```

--------------------------------

### Upgrade leanblueprint via pip

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Upgrades the existing leanblueprint installation to the latest version.

```bash
pip install -U leanblueprint
```

--------------------------------

### Run Full Build Pipeline

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Execute the complete build process including PDF, HTML, and declaration verification.

```bash
# Run complete build pipeline
leanblueprint all

# Equivalent to running:
# leanblueprint pdf
# leanblueprint web
# lake build
# leanblueprint checkdecls
```

--------------------------------

### Implement Blueprint Macros for Theorems and Definitions

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use standard LaTeX environments combined with \lean, \leanok, \uses, and \discussion macros to link documentation to Lean code.

```latex
% content.tex
\chapter{Main Results}

\begin{definition}
  \label{def:immersion}
  \lean{Immersion}
  \leanok
  A smooth map $f : M \to N$ is an \emph{immersion} if $Df_p$ is injective
  for all $p \in M$.
\end{definition}

\begin{definition}
  \label{def:ample}
  \lean{AmpleRelation}
  \notready  % Still working on blueprint
  A first-order partial differential relation $\mathcal{R}$ is \emph{ample}
  if it satisfies the h-principle.
\end{definition}

\begin{lemma}
  \label{lem:immersion_ample}
  \lean{immersion_ample}
  \leanok
  \uses{def:immersion, def:ample}
  \discussion{15}  % See GitHub issue #15
  The immersion relation is ample for $\dim M < \dim N$.
\end{lemma}

\begin{theorem}[Sphere Eversion]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There exists a regular homotopy from the standard embedding of $S^2$
  in $\mathbb{R}^3$ to the antipodal embedding.
\end{theorem}

\begin{proof}
  \leanok
  \uses{lem:immersion_ample, thm:h_principle}
  Apply the h-principle for ample relations to the immersion relation.
  Since immersions form an ample relation by \ref{lem:immersion_ample},
  the result follows from the general h-principle.
\end{proof}
```

--------------------------------

### Compile HTML Blueprint

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Generate the HTML version of the blueprint with interactive dependency graphs.

```bash
# Compile HTML version (output in blueprint/web/)
leanblueprint web

# Output structure:
# blueprint/web/
# ├── index.html
# ├── chapter1.html
# ├── dep_graph.html        # Interactive dependency graph
# ├── dep_graph_document.html
# └── ...
```

--------------------------------

### Configure Blueprint Package Options

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Configure the dependency graph behavior by specifying which theorem environments to track. Options include default tracked environments or custom sets.

```latex
% In web.tex preamble
% Default tracked environments: definition, lemma, proposition, theorem, corollary
\usepackage[dep_graph]{blueprint}
```

```latex
% Custom tracked environments (short names)
\usepackage[thms=dfn+lem+prop+thm+cor]{blueprint}
```

```latex
% Enable show/hide proof buttons (requires plastexshowmore plugin)
\usepackage[showmore, dep_graph]{blueprint}
```

```latex
% Combined options
\usepackage[showmore, thms=definition+theorem+lemma, dep_graph]{blueprint}
```

--------------------------------

### Compile PDF Blueprint

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Generate the PDF version of the blueprint using latexmk.

```bash
# Compile PDF (output in blueprint/print/print.pdf)
leanblueprint pdf

# The PDF is generated at: blueprint/print/print.pdf
# Bibliography (.bbl) is copied to blueprint/src/web.bbl for web version
```

--------------------------------

### Defining Theorems and Proofs with Lean Macros

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Use these macros within theorem and proof environments to link LaTeX content to Lean declarations and track dependencies.

```latex
\begin{theorem}[Smale 1958]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There is a homotopy of immersions of $𝕊^2$ into $ℝ^3$ from the inclusion map to
  the antipodal map $a : q ↦ -q$.
\end{theorem}
  
\begin{proof}
  \leanok
  \uses{thm:open_ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end{proof}
```

--------------------------------

### Run plasTeX with the plugin

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Alternative method to invoke the plugin directly via plasTeX without using the CLI tool.

```bash
plastex --plugins leanblueprint my_file.tex
```

--------------------------------

### Configure GitHub Actions for Blueprint Deployment

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Automate the build and deployment of Lean projects and blueprints using the provided GitHub Actions workflow configuration.

```yaml
# .github/workflows/blueprint.yml (auto-generated)
name: Compile blueprint

on:
  push:
    branches:
      - main
  workflow_dispatch:

permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  build_project:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        with:
          fetch-depth: 0

      - name: Build and lint project
        uses: leanprover/lean-action@v1
        with:
          build: true
          lint: true

      - name: Compile blueprint and documentation
        uses: leanprover-community/docgen-action@v1
        with:
          blueprint: true
          homepage: home_page

# After successful deployment:
# - Blueprint HTML: https://username.github.io/repo/blueprint/
# - Blueprint PDF: https://username.github.io/repo/blueprint.pdf
# - API Documentation: https://username.github.io/repo/docs/
```

--------------------------------

### Configure Project URLs

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Configure URLs for the project home page, GitHub repository, and API documentation in the web.tex preamble. These are used for links within the generated documentation.

```latex
% In blueprint/src/web.tex after \usepackage{blueprint}

% Project home page URL (displayed in header)
\home{https://leanprover-community.github.io/sphere-eversion/}
```

```latex
% GitHub repository URL (used for issue links)
\github{https://github.com/leanprover-community/sphere-eversion}
```

```latex
% API documentation URL (used for Lean declaration links)
\dochome{https://leanprover-community.github.io/sphere-eversion/docs}
```

--------------------------------

### Mark as Mathlib: \mathlibok

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \mathlibok to indicate that a result already exists in Mathlib, meaning no custom formalization is required. This is typically used in theorem environments.

```latex
\begin{theorem}[Fundamental Theorem of Calculus]
  \label{thm:ftc}
  \lean{intervalIntegral.integral_eq_sub_of_hasDerivAt}
  \mathlibok  % Already in Mathlib, no custom formalization needed
  \uses{def:integral, def:derivative}
  If $F' = f$ on $[a,b]$, then $\int_a^b f(x)\,dx = F(b) - F(a)$.
\end{theorem}
```

--------------------------------

### Local blueprint management commands

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Commands for building, checking, and serving blueprints locally. Ensure the project is built with lake before running checkdecls.

```bash
leanblueprint pdf
```

```bash
leanblueprint web
```

```bash
leanblueprint checkdecls
```

```bash
leanblueprint all
```

```bash
leanblueprint serve
```

--------------------------------

### Declare Dependencies: \uses

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \uses to declare dependencies on other labeled items for dependency graph generation. Apply it in theorem statements for statement-level dependencies or in proofs for proof-level dependencies.

```latex
\begin{lemma}
  \label{lem:helper}
  \lean{helper_lemma}
  \leanok
  A technical helper lemma.
\end{lemma}
```

```latex
\begin{theorem}
  \label{thm:main}
  \lean{main_theorem}
  \uses{def:key_definition}  % Needed to state the theorem
  The main result of the paper.
\end{theorem}
```

```latex
\begin{proof}
  \uses{lem:helper, thm:auxiliary}  % Needed for the proof
  Apply the helper lemma and auxiliary theorem.
\end{proof}
```

--------------------------------

### Verify Lean Declarations

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Check that all referenced Lean declarations exist in the project.

```bash
# First, build your Lean project
lake build

# Then check that all \lean{...} declarations exist
leanblueprint checkdecls

# Example output for missing declarations:
# Error: Declaration 'MyProject.nonexistent_lemma' not found
# Error: Declaration 'MyProject.missing_def' not found

# On success (all declarations found):
# All declarations verified successfully
```

--------------------------------

### Configuring Dependency Graph Environments

Source: https://github.com/patrickmassot/leanblueprint/blob/master/README.md

Customize the list of environments tracked by the dependency graph by passing the thms option to the blueprint package.

```latex
\usepackage[thms=dfn+lem+prop+thm+cor]{blueprint}
```

--------------------------------

### Mark as Not Ready: \notready

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \notready to mark an environment as not ready for formalization, indicating that blueprint work is still needed before Lean implementation can begin.

```latex
\begin{conjecture}
  \label{conj:open_problem}
  \notready  % Blueprint work still needed
  \uses{def:zeta_function}
  The Riemann zeta function has all non-trivial zeros on the critical line.
\end{conjecture}
```

--------------------------------

### Specify Proof Target: \proves

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \proves to specify which theorem a proof block is proving, especially when the proof does not immediately follow its statement. The argument is the label of the theorem.

```latex
% In the main text
\begin{theorem}
  \label{thm:deferred}
  \lean{deferred_theorem}
  A theorem whose proof appears later.
\end{theorem}

% Later in the document
\begin{proof}
  \proves{thm:deferred}  % Links this proof to the theorem
  \leanok
  \uses{lem:key_step}
  The deferred proof of the theorem.
\end{proof}
```

--------------------------------

### Mark Formalization Status: \leanok

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \leanok to indicate that a definition, theorem statement, or proof is fully formalized in Lean. Place it inside theorem environments for statements or proof environments for proofs.

```latex
\begin{theorem}[Sphere Eversion]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok  % Statement is formalized
  There is a homotopy of immersions of $\mathbb{S}^2$ into $\mathbb{R}^3$
  from the inclusion map to the antipodal map.
\end{theorem}
```

```latex
\begin{proof}
  \leanok  % Proof is also formalized
  \uses{thm:open_ample, lem:open_ample_immersion}
  This follows from the h-principle for open ample relations
  applied to the space of immersions.
\end{proof}
```

--------------------------------

### Link Theorem to Lean Declaration: \lean

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \lean to link a LaTeX theorem or definition to its corresponding Lean declaration name. Multiple declarations can be specified as a comma-separated list.

```latex
\begin{definition}
  \label{def:immersion}
  \lean{Immersion, IsImmersion}
  A smooth map $f : M \to N$ between manifolds is an \emph{immersion}
  if its differential is injective at every point.
\end{definition}
```

```latex
\begin{theorem}[Whitney Embedding]
  \label{thm:whitney}
  \lean{whitney_embedding_theorem}
  \leanok
  Every smooth $n$-dimensional manifold can be embedded in $\mathbb{R}^{2n}$.
\end{theorem}
```

--------------------------------

### Link to Discussion: \discussion

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use \discussion to link to a GitHub issue for discussions regarding the formalization approach of a specific result. The argument is the issue number.

```latex
\begin{theorem}
  \label{thm:controversial_approach}
  \lean{controversial_theorem}
  \discussion{42}  % Links to GitHub issue #42
  \uses{def:complex_construction}
  A theorem whose formalization approach is being discussed.
\end{theorem}
```

--------------------------------

### Configure LaTeX Dependency Graph Colors

Source: https://context7.com/patrickmassot/leanblueprint/llms.txt

Use the \graphcolor macro in the LaTeX preamble to define custom colors for dependency graph nodes.

```latex
% In web.tex preamble
% \graphcolor{node_type}{color}{legend_description}

% Default color scheme:
% stated (border) - green: statement is formalized
% can_state (border) - blue: ready to formalize statement
% not_ready (border) - orange: needs blueprint work
% proved (fill) - light green: proof is formalized
% can_prove (fill) - light blue: ready to formalize proof
% defined (fill) - light green: definition is formalized
% fully_proved (fill) - dark green: fully formalized with all ancestors
% mathlib (border) - dark green: in Mathlib

% Custom colors example
\graphcolor{stated}{#2E8B57}{Sea Green}
\graphcolor{proved}{#98FB98}{Pale Green}
\graphcolor{fully_proved}{#006400}{Dark Green}
\graphcolor{not_ready}{#FF6347}{Tomato}
```

--------------------------------

### Configure MathJax Equation Numbering

Source: https://github.com/patrickmassot/leanblueprint/blob/master/leanblueprint/jekyll_templates/_include/mathjax.html

This snippet configures MathJax to automatically number equations using the AMS style. Ensure MathJax is included on the page for this to take effect.

```javascript
{% if page.usemathjax %} MathJax.Hub.Config({ TeX: { equationNumbers: { autoNumber: "AMS" <!-- Automatically number equations using AMS style --> } } }); {% endif %}
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.