数学家使用计算机进行数值计算或者处理复杂方程已有很长时间。通过让计算机进行大量重复运算，他们已经证明了一些重要结论。最著名的例子便是上世纪70年代证明四色定理。然而，一种称为“证明助手”的系统功能更为深入。用户基于系统已知的简单对象，输入命题来使系统理解数学概念的定义。输入的命题可以只涉及已知对象，证明助手则会基于它现有的知识来判断该命题是“明显”正确或错误。
如果证明助手的回答是不“明显”，用户则需要输入更多的信息来训练它。证明助手借此迫使用户更加严密地展开他们的论证逻辑，并填补数学家们有意无意省略的一些较简单步骤。一旦研究人员完成了前期繁重的训练工作，使证明助手理解了一系列数学概念，系统就会生成一个计算机代码库。其他研究人员可以以此为基础进行研究，并定义更高级的数学对象。由此，证明助手就能够帮助检验那些耗时费力，甚至是人力所不可及的数学证明。
证明助手一直都不乏拥护者，但这是它首次在领域前沿发挥重要作用，帝国理工学院的数学家Kevin Buzzard说。他参与检验了Scholze和Clausen的研究结果。“之前遗留下来的一个重要问题是：证明助手能否处理复杂的数学问题？”Buzzard说。“我们证明了它们可以。”而且这一切来得太快，超乎任何人的想象。2020年12月，Scholze向证明助手领域的专家们寻求帮助。
德国弗赖堡大学的数学家Johan Commelin带领一队志愿者开始着手解决这一难题。五个多月后的2021年6月5日，Scholze就在Buzzard的博客中宣布，实验主体部分已经成功。“这简直不可思议。交互式证明助手现在已经达到了如此的高度：它能在合理时间内逻辑完备地验证复杂的原创研究。”Scholze写道。
Scholze和Clausen指出，凝聚态数学的关键在于重新定义现代数学的基石之一——拓扑的概念。数学家们研究的很多对象都具有拓扑。拓扑是对象的一种结构，它决定对象的哪些部分相连，哪些不是。拓扑提供了形状的信息，但是比起我们所熟悉的经典几何，拓扑更具延展性：在拓扑中，任意不分割对象的变换都是允许的。比如，一个三角形在拓扑上等价于其他任意三角形，甚至等价于圆形，但是无法等价于一条直线。