This is the development repository for formalised condensed mathematics in Lean. The mathematical results are due to Dustin Clausen and Peter Scholze.

The Lean code is contained in the directory LeanCondensed. The subdirectory Mathlib contains code that is ready to be integrated in Mathlib (and has in many cases already been PR-ed), organised in such a way that the file names correspond to the ones in Mathlib. The other subdirectories contain more work-in-progress code. The goal is to get everything into Mathlib eventually.