传统上，数学研究由少数专家进行，难以大规模组织。证明助手语言如Lean提供了解决方案，允许专业数学家、公众和AI工具共同参与复杂项目。通过模块化分解，可以实现大规模协作。目前主要是人类参与，但也有自动化工具的尝试。项目如“Polymath”展示了这种协作的潜力。本文提出试点项目，探索简单代数理论的等式公理，利用证明助手和众包方法扩展研究规模。