English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Condensed mathematics, developed by Clausen and Scholze over the last fewyears, is a new way of studying the interplay between algebra and geometry. Itreplaces the concept of a topological space by a more sophisticated butbetter-behaved idea, namely that of a condensed set. Central to the theory aresolid abelian groups and liquid vector spaces, analogues of completetopological groups.  N\"obeling's theorem, a surprising result from the 1960s about the structureof 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 onecannot give any nonzero examples of solid abelian groups. We discuss a recentlycompleted formalisation of this result in the Lean theorem prover, and give amore detailed proof than those previously available in the literature. Theproof is somewhat unusual in that it requires induction over ordinals -- atechnique which has not previously been used to a great extent in formalisedmathematics.

Towards solid abelian groups: A formal proof of N\"obeling's theorem