Lean Formalization of PDE Topics

The files in this directory contain formalizations of selected topics of PDE (partial differential equations) into Lean. The ultimate goal of this formalization is to prepare a comprehensive toolbox for formal analysis of PDEs, for both research and education purposes. This formalization may not be fully optimized for efficient Lean compilation, and may have compatibility issues with the latest Lean and mahtlib versions (which evolve very rapidly).

References

"Partial Differential Equations, A First Course", Rustom Choksi, AMS, 2022.

Sections

Basics

Heat

• HeatKernel: The Fundamental Solution/Heat Kernel and Its Properties.
• HeatSolution: The convolution solution of the heat kernel.
• HeatSolutionProperty: Properties of the heat solution, involving the convolution of the heat kernel and the initial condition

Other Resources

• Web page for this project

Building the Project

To build this project after installing Lean and cloning this repository, follow these steps:

% ./build.sh

You can then serve the documentation locally as a webpage by executing python3 serve.py

Updating the Lean/Mathlib version

Because this project uses a deprecated method to conditionally require doc-gen4 in order to update the version of Lean and Mathlib used in the project you need to:

• edit the lakefile.lean to change the require lines for Mathlib and doc-gen4, to pin to the tag corresponding to the next Lean version (it is highly recommended that you update in incremental steps)
• edit the lean-toolchain to change the Lean version to the next version
• run lake update -R -Kenv=dev
• this may have the side effect of setting your lean-toolchain to the latest Lean version; if so, revert it to the intended version

General Lean Resources

This list is largely inherited from, and thus credited to, Professor Tao's Analysis.

• The Lean community
  • Lean4 web playground
  • How to run a project in Lean locally
  • The Lean community Zulip chat
  • Learning Lean4
    • The natural number game
    • Mathematics in Lean - Lean textbook by Jeremy Avigad and Patrick Massot
• Mathlib documentation
  • Mathlib help files
  • LeanFinder - Natural language search engine for Mathlib
  • List of Mathlib tactics
    • Lean tactics cheat sheet
• Lean extensions:
  • Canonical
  • Duper
  • LeanCopilot
• Common Lean pitfalls
• Lean4 questions in Proof Stack Exchange
• The mechanics of proof - introductory Lean textbook by Heather Macbeth
• A broader list of AI and formal mathematics resources.

More resource suggestions welcome!

Acknowledgment

• Professor Terence Tao's Analysis