Let's code math | Lean4 | Theorem prover

Continuous functions play a crucial role in various disciplines in math. We discuss the epsilon-delta criterion and formalize it in the programming language and Theorem prover Lean4. We also prove that the constant function and the "line function" are continuous and finally discuss left- and right-continuity with the example of the Heaviside function Θ. #lean4 #proof #analysis

💡 Feel free to explore our code and a LaTeX document on GitHub:
https://github.com/Splines/lean-continuous

✍ References
- Vladimir A. Zorich - Mathematical Analysis I. Second Edition.
https://link.springer.com/content/pdf/10.1007/978-3-662-48792-1.pdf
- Stephen Abbott - Understanding Analysis. Second Edition.
https://csunibo.github.io/analisi-matematica/libri/real-analysis.pdf

🌟 Acknowledgements & Credits
- Thank you Felix for working through the topics with me.
- Shoutout to the computer-assisted math seminar 2024 organized by Florent S. & Judith L.
- Thank you Marc, Emilian & Nils for reviewing the draft version of this video.
- Background image by vackground.com on Unsplash:
https://unsplash.com/photos/a-white-and-gray-abstract-background-with-curves-vo-M6JACr-k
- Background image by vackground.com on Unsplash:
https://unsplash.com/photos/a-close-up-of-a-blue-and-orange-abstract-background-jEDNGHrrVRw
- Background image (for thumbnail) by Blair Fraser on Unsplash:
https://unsplash.com/photos/night-sky-photo-aI1tDC8PaLM

💻 Tools used
I used PowerPoint to animate everything, OBS to screen-record it and DavinciResolve to edit it and record the audio. Other great tools include Blender and GeoGebra, but they weren't used in this video. I use the great IguanaTex plugin by Jonathan-LeRoux for LaTeX to include LaTeX in PowerPoint (different than the built-in formula editor).

▶ Chapters
00:00 Intro & Outline
01:17 Definition
03:52 Example: Constant function
07:04 Example: Line
12:17 Left- and right-continuity
17:38 Comments
20:00 Outro