Fermat's Last Theorem (FLT) Project

When authoring in Verso, start by mastering these three fundamental patterns:

1. #doc (Manual) "Title" =>: Starts a document module.
2. {include 0 Some.Module}: Includes a chapter module into the top-level Blueprint file.
3. :::definition "label_1": Starts a Blueprint block.

Blueprint nodes (statements, groups, authors, etc.) are identified by unique labels chosen by the author. These labels are stable identifiers used for:

• Dependency references: Using {uses "label"}[] to create a dependency edge in the graph.
• Link-only references: Using {bpref "label"}[] to link to a node without registering a formal dependency.
• Code attachment: Labeling inline lean or rust blocks to attach them to a Blueprint node.
• Metadata: Used in summary pages, graphs, and exported metadata.

Tip: Choose labels early and treat them as stable project identifiers. If a role like {uses "label"}[] has an empty payload, Blueprint can automatically generate visible text (e.g., Theorem N).

This module proves the dimension theorem for Noetherian local rings. It establishes that the Krull dimension of a ring $R$ is equal to both the growth degree of its Hilbert-Samuel function and the minimum number of generators of an ideal whose radical is the maximal ideal.

The core theorem is expressed as the cycle: dim R ≤ growthDeg R ≤ minGenPrimary R ≤ dim R.

Key definitions used:

• growthDeg R: The least exponent bounding the Hilbert-Samuel function $n \mapsto \text{length}(R / \mathfrak{m}^n)$. Note that this is treated as a formal growth order rather than a constructed polynomial.
• minGenPrimary R: The least number of generators of an ideal whose radical is the maximal ideal.
• ringKrullDim R: The Krull dimension of the ring.

ringKrullDim R = (growthDeg R : WithBot ℕ∞)
ringKrullDim R = (minGenPrimary R : WithBot ℕ∞)

The blueprint software, developed by Patrick Massot, is a framework used to enable collaboration on large-scale formalization projects. It provides tools for:

• Dependency Management: Creating a blueprint graph that visualizes the progress and logical dependencies of a proof.
• Mathematical Roadmapping: Providing a structured way to write mathematical proofs (often in LaTeX) that serve as a roadmap for formalization in an ITP like Lean.
• Collaboration: Facilitating the transition of mathematical ideas from paper to code by allowing experts to state results clearly for others to formalize.

A Blueprint project consists of three primary components:

1. Chapter Modules: One or more Lean files containing the mathematical content.
2. Blueprint Top-level File: An assembly file (often named Contents.lean in older examples) that organizes the document and includes chapters.
3. Generator Entry Point: A file (e.g., ProjectTemplateMain.lean) that renders the site.

Key files in a standard template include lakefile.lean for package configuration and the generator entry point.

A Blueprint project is composed of three primary components:

1. Chapter modules: Lean files containing the mathematical content and Blueprint blocks.
2. Top-level Blueprint file: An assembly file (often named Contents.lean, though the name is arbitrary) that imports chapters and configures global pages.
3. Generator entry point: A file that handles the rendering of the site.

This structure allows you to separate mathematical content from the document assembly and the final rendering logic.

To verify that the formalization is complete and does not rely on unproven assumptions (using sorry), use the lake build command. You can then inspect the axioms used by the theorem to ensure it only relies on standard Lean axioms.

Run the following commands:

# Compile the package
lake build FLT.Slop.DimensionTheorem

# Check the axioms used by the theorem
#print axioms DimensionTheorem.dimension_theorem

A successful verification should report only the three standard axioms: [propext, Classical.choice, Quot.sound].

Blueprint chapters use specific block forms to define mathematical objects. These blocks can be nested or linked via parent attributes.

Core Block Forms:

• :::definition "label"
• :::lemma_ "label"
• :::theorem "label"
• :::corollary "label"
• :::proof "label" (Attaches to the preceding statement with the same label)
• :::group "label" (Used for grouping related statements)
• :::author "id" (name := "Name") (Assigns authorship)

Example usage:

:::definition "addition_spec" (parent := "addition_core")
We write $`a + b` for the result of adding $`b` to $`a`.
:::

:::theorem "addition_right_identity" (parent := "addition_core") (owner := "project_author")
For every natural number $`n`, adding zero on the right leaves it unchanged: $`n + 0 = n`.
:::

:::proof "addition_right_identity"
Induct on $`n`.
:::

The project is open-source and relies on crowd-sourcing mathematical expertise. To participate:

1. Explore the codebase: The formalization work is hosted on GitHub at https://github.com/ImperialCollegeLondon/FLT.
2. Review the roadmap: Use the blueprint (an in-progress LaTeX write-up) and the blueprint graph (a dependency graph showing current progress) to understand the mathematical route being taken.
3. Collaborate via Zulip: The primary research forum for real-time collaboration between mathematicians and computer scientists is the FLT stream on Lean Zulip. This is the recommended place to make yourself known if you wish to contribute code or mathematical proofs.