在通用代数中探索协作与机器辅助新方法的试点项目

传统上，数学研究由少数专家进行，难以大规模组织。

证明助手语言如Lean提供了解决方案，允许专业数学家、公众和AI工具共同参与复杂项目。

通过模块化分解，可以实现大规模协作，当前主要是人类参与，但也有自动化工具的尝试。

项目如“Polymath”展示了这种协作的潜力，但未使用证明助手，限制了规模。

希望利用现代工具探索多个数学问题，而不是仅关注一两个问题。

提出一个试点项目，探索简单代数理论的等式公理，利用证明助手和众包方法扩展研究规模。

项目关注于对magmas的简单等式理论进行中等规模的探索。

希望扩展Hasse图，覆盖更多的等式，探索其结构和相互关系。

计划通过众包的方式收集证明和反例，减少人类审核的工作量。

希望整合图形可视化软件，展示部分已知的偏序集结构。