在通用代数中探索协作与机器辅助新方法的试点项目
原文英文,约2500词,阅读约需9分钟。发表于: 。Traditionally, mathematics research projects are conducted by a small number (typically one to five) of expert mathematicians, each of which are familiar enough with all aspects of the project...
传统上,数学研究由少数专家进行,难以大规模组织。证明助手语言如Lean提供了解决方案,允许专业数学家、公众和AI工具共同参与复杂项目。通过模块化分解,可以实现大规模协作。目前主要是人类参与,但也有自动化工具的尝试。项目如“Polymath”展示了这种协作的潜力。本文提出试点项目,探索简单代数理论的等式公理,利用证明助手和众包方法扩展研究规模。