Condensed mathematics is a new foundational theory being developed by Clausen-Scholze et al., which aims to replace topological spaces with "condensed sets". This new framework provides a convenient setting for topological algebra where various issues from the classical approaches using point-set topology can be resolved. The condensed world can also handle several aspects of *functional analysis* in an essentially algebraic manner, and the theory of *liquid vector spaces* plays a central role in this context.

Several portions of this theory have now been formalized on a computer using the Lean interactive proof assistant, starting with the *liquid tensor experiment*, which arose as a response to Scholze's 2020 challenge to formally verify the "main theorem of liquid vector spaces". While the liquid tensor experiment was successfully completed in the summer of 2022, work on the formalization of condensed mathematics is ongoing. After an introduction to condensed mathematics and liquid vector spaces, in this talk, I will discuss the liquid tensor experiments and the recent efforts to explain condensed mathematics to a computer.