A Lean 4 project dedicated to formalizing core results from Geometric Measure Theory (GMT), specifically a formalization of Marstrand's Theorem. This repository contributes to the growing ecosystem of mathematics in Lean.
We are supported by the UW Math AI Lab. Click here to learn more about us.
This project aims to:
- Upstream foundational components to
mathlib - Formalize Marstrand's Theorem and add other GMT results
Here is a poster we presented; it is not up to date, but gives a glimpse into our project structure. We will replace this with our paper when it is done.
Wrapping up
Further work:
- Write our paper
- Add more of our content to
mathlib LeanPoolsubmission
| PR | Status | Description |
|---|---|---|
| #32824 | Merged | Prove that the diameter of a Euclidean ball is twice its radius |
| #32851 | Merged | Introduces Theorem exists_accPt_of_noAtoms and lemma discreteTopology_of_noAccPts |
| #42042 | Merged | Caratheodory measurability of measure-zero sets and complement lemmas |
| #TBA | Todo | Add API about densities to mathlib |