MSc Thesis
Towards a Formalisation of the Kakeya Conjecture in ℝ²
Towards a Formalisation of the Kakeya Conjecture in ℝ²
Imperial College London, 2024–2025
Supervised by Dr Bhavik Mehta.
The central aim of this project is the formalisation of the Kakeya conjecture in the plane within the Lean theorem prover. While the conjecture is trivial in one dimension and remains largely open in higher dimensions, the two-dimensional case was resolved by Davies (1971), who proved that every Besicovitch set in ℝ² has full Hausdorff dimension. This project focused on formalising the existence of a Besicovitch set in ℝ².