Recent progress in artificial intelligence (AI) is unlocking transformative capabilities for mathematics. There is great hope that AI will help solve major open problems and autonomously discover new mathematical concepts. In this essay, we further consider how AI may open a grand perspective on mathematics by forging a new route, complementary to mathematical\textbf{ logic,} to understanding the global structure of formal \textbf{proof}\textbf{s}. We begin by providing a sketch of the formal structure of mathematics in terms of universal proof and structural hypergraphs and discuss questions this raises about the foundational structure of mathematics. We then outline the main ingredients and provide a set of criteria to be satisfied for AI models capable of automated mathematical discovery. As we send AI agents to traverse Platonic mathematical worlds, we expect they will teach us about the nature of mathematics: both as a whole, and the small ribbons conducive to human understanding. Perhaps they will shed light on the old question: "Is mathematics discovered or invented?" Can we grok the terrain of these \textbf{Platonic worlds}?

翻译：人工智能（AI）的最新进展正在为数学领域解锁变革性能力。人们寄予厚望，希望AI能帮助解决重大未解难题，并自主发现新的数学概念。本文进一步探讨了AI如何通过开辟一条与数学**逻辑**互补的新路径，为理解形式化**证明**的整体结构打开一个宏大的数学视角。我们首先以通用证明与结构超图为基础，勾勒数学的形式结构，并讨论由此引发的关于数学基础结构的疑问。接着，我们概述了具备自动数学发现能力的AI模型所需的主要要素，并提出一套需满足的准则。当我们派遣AI智能体穿越柏拉图的数学世界时，我们期待它们能揭示数学的本质：既包括数学的整体面貌，也包括那些易于人类理解的小小脉络。或许它们将照亮那个古老的问题：“数学是被发现的，还是被发明的？”我们能否领悟这些**柏拉图世界**的地形？