In the recent lecture series run jointly from IHÉS and Bonn, Clausen and Scholze have reworked—again—their foundations of geometry to focus attention on not arbitrary condensed sets and solid modules and so on, but the much smaller class of light condensed sets and so on. These are enough to faithfully capture all sequential spaces, for example, which is a very large class of spaces that contains all CW complexes, metric spaces, (fin dim) manifolds etc. Further, the category of light condensed sets is an honest Grothendieck topos, whereas the category of all condensed sets is close to being so, but has instead a generating proper class, not a set.
The proofs in the theory of solid abelian groups and solid modules became as a result much, much nicer, due to the fact that there is a very nice generic object in the category of light condensed abelian groups (free on a null-sequence) that is projective in that category—but not in the category of all condensed abelian groups.
What would be nice to know is if this new formalism sheds any similar light on the construction of the liquid tensor product(s), making the theory and the proofs easier. I've watched I think nearly all the lecture series mentioned above, but I don't recall this arising or being mentioned. What was discussed was a new completeness condition analogous to solid/liquid, called "gaseous", but I don't know if this helps with the liquid theory at all as far as simplifying what the Liquid Tensor Experiment needed to show.
Unlike the previous lecture courses on condensed mathematics, there is no running set of lecture notes, but rather Clausen and Scholze are apparently writing a book on this material. So there's no extra written material to check over.
Best Answer
Good question!
We've been trying to figure this out as we went along, but so far unsuccessfully. Some more precise points:
For many (but definitely not all) applications to geometry over the real numbers, the gaseous real vector spaces work just as well, and their theory is much easier to get off the ground than liquid real vector spaces. (Roughly speaking, complex- or real-analytic spaces are fine with gaseous vector spaces, smooth manifolds not so much. The reason is that tensor products of spaces of holomorphic or real-analytic functions behave correctly under the gaseous tensor product, but tensor products of spaces of $C^\infty$-functions are only correct under the liquid tensor product.) This is the route we've taken in the course.
We believe that there is a way to characterize (light) liquid real vector spaces in a way close to how we characterize solid or gaseous modules, in terms of certain endomorphisms of this free module $P$ on a nullsequence to become isomorphisms. However, in this case we are not able to see any simple way to compute the resulting completion functor.
If one was able to prove that there is a good theory of light liquid real vector spaces, the full result would follow. More precisely, Theorem 9.1 reduces rather formally to the light setting.
Summary: So far, the theory of liquid real vector spaces remains as hard as it previously was.