Peter Scholze proposes to formalize the proof of a major result in the Clausen–Scholze approach to rigid analytic geometry via condensed sets. This theory, a version of which was also discovered independently by Barwick and Haine and called pyknotic sets, has two localizations, giving the theory of solid and liquid condensed sets, aimed at the study of \(p\)-adic analytic geometry and real analytic geometry, respectively. A good place to start learning about all of this is with the videos from the recent Copenhagen masterclass.

The problem specifically is to formalize (for example in Lean) the proof that there are no higher Ext groups between certain objects relevant to the liquid theory. More like a liquid Ext experiment.

I found out about this via a post at the n-category café.