A project by Dominic Plein (@Splience) & Felix Lentze
in the course of a seminar on computer-assisted maths.
YouTube Video
Warning
This is a research project and not stable code. We also don't maintain this code in the long run. It's mainly for educational purposes and for us to learn Lean4. Nevertheless, you might still find it useful to get started with Lean4 in the context of continuous functions.
In this repository, we give an introduction to continuous functions and formalize them in the functional programming language and mathematical proof-solver Lean4. Continuous functions play a crucial role in many math disciplines and are taught at the very beginning of math studies.
In this repo, you find:
-
A LaTeX document that contains manual proofs. All proofs that were formalized in Lean4 are also written out in this document for reference. It's suggested to first comprehend the proof there, then look at the Lean4 code to see how it's formalized.
-
The Lean4 code with different files that correspond to the sections in the LaTeX document:
- Continuous Functions: Here we give the definition of continuous functions.
- Examples: Here we give some examples of continuous functions.
- Algebraic properties: Here we prove that the sum and the product of two continuous functions are continuous again.
- Left- and right-continuity: Here we define left- and right-continuity, and prove that they are equivalent to continuity. We also discuss the Heaviside function.
See this guide for how to install Lean4 on your machine. It guides you through how to install elan, the Lean version manager, which also installs Lake for you, the Lean package manager.
Then run lake exec cache get in the root of this project. Don't run lake update as we want to stick with the specific version of Lean specified pinned via the lake-manifest.json file.
We highly recommend to use Visual Studio Code as your editor as the Lean4 community has developed a great extension for it. It's included as "recommended extension" to this workspace. Use Extensions: Show Recommended Extensions to install it.
We use some style guidelines from the Lean community here and here. However, note that we are beginners in Lean and therefore our style used in the code might disagree with many "official" guidelines.
Our formatting aims at maximizing readability and understanding for beginners. We write out some tactics even if they could be compressed into a "one-liner". We also make use of excessive white space and comments to make the code more accessible and not a "hell of symbols".