This repository contains the source latex code for my bachelor’s thesis project in the Faculty of Mathematics and Computer Science at FernUni.
The project aims to provide an introduction to formal mathematics using Lean, with a focus on the practical application of theorem proving rather than a detailed exposition of the language itself.
The accompanying code examples are available here:
🔗 Intro to Formal Mathematics in Lean
Within this project, I include a formalization of the classical result that the topological sine curve is connected but not path-connected.
The work takes inspiration from Konrad Conrad’s exposition:
📄 “Connected but Not Path Connected”
🔗 https://kconrad.math.uconn.edu/blurbs/topology/connnotpathconn.pdf
The formalized and revisited proof is available as a pull request in Mathlib4: 🔗 mathlib4#25529. The edited and merged version is a stronger result than my original work.