I'm not a mathematician and I'm generally unqualified to comment on any of this but I'll have a stab anyway. The TLDR is that Peter Scholze, one of modern math

I'm not a mathematician and I'm generally unqualified to comment on any of this but I'll have a stab anyway. The TLDR is that Peter Scholze, one of modern mathematics' most accomplished theory builders, has a concept called a 'condensed set' that he thinks can act as a drop-in replacement for topological spaces in most of mathematics. Topological spaces are perhaps one of the least restrictive models of 'space' is in mathematics. Peter thinks his definition will allow mathematicians to bring algebraic techniques to bear on problems that were previously not amenable to such methods. The problem is that everything rests on one theorem, whose proof is difficult. Because the proof is so foundational, he'd like to get it checked by computer instead of relying on the opinion of a handful of mathematicians, who may be sloppy in their checking.