Condensed mathematics, developed by Clausen and Scholze over the last few years, is a new way of studying the interplay between algebra and geometry. It replaces the concept of a topological space by a more sophisticated but better-behaved idea, namely that of a condensed set. Central to the theory are solid abelian groups and liquid vector spaces, analogues of complete topological groups. N\"obeling's theorem, a surprising result from the 1960s about the structure of the abelian group of continuous maps from a profinite space to the integers, is a crucial ingredient in the theory of solid abelian groups; without it one cannot give any nonzero examples of solid abelian groups. We discuss a recently completed formalisation of this result in the Lean theorem prover, and give a more detailed proof than those previously available in the literature. The proof is somewhat unusual in that it requires induction over ordinals -- a technique which has not previously been used to a great extent in formalised mathematics.

翻译：凝聚态数学（Condensed mathematics）由Clausen和Scholze在过去几年中发展，是一种研究代数与几何之间相互作用的新方法。它用更精密且性质更优良的凝聚集概念取代了拓扑空间的概念。该理论的核心是固态阿贝尔群和液态向量空间，它们是完备拓扑群的类比。Nöbeling定理是1960年代一个关于从投射有限空间到整数的连续映射的阿贝尔群结构的惊人结果，它是固态阿贝尔群理论的关键组成部分；没有它，我们无法给出固态阿贝尔群的任何非零示例。我们讨论了在Lean定理证明器中近期完成的该定理的形式化，并提供了比现有文献更详细的证明。该证明较为独特，因为它需要对序数进行归纳——这一技巧此前在形式化数学中尚未被广泛使用。