A major advancement happened this year where a recent paper from a fields medalist on an incredibly abstract topic was formally proved in Lean. The theorem was

A major advancement happened this year where a recent paper from a fields medalist on an incredibly abstract topic was formally proved in Lean. The theorem was that Scholze’s new condensed mathematics was logically consistent with real functional analysis. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm...