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.

翻译：凝聚数学是Clausen和Scholze近年来发展的一种研究代数与几何相互作用的新方法。它用更复杂但性质更好的凝聚集概念取代了拓扑空间的概念。该理论的核心是固态阿贝尔群与液态向量空间——它们对应于完备拓扑群。诺贝林定理是20世纪60年代关于从射有限空间到整数连续映射的阿贝尔群结构的惊人结果，该定理是固态阿贝尔群理论的关键要素；若缺少此定理，则无法给出任何非零的固态阿贝尔群实例。我们讨论了该定理在Lean定理证明器中最近完成的形式化工作，并提供了比现有文献更详细的证明。该证明的特殊之处在于需要基于序数进行归纳——这种技术在形式化数学中尚未得到广泛应用。