Mathematics Distillation Challenge – Equational Theories
2 months ago
- #AI
- #collaboration
- #mathematics
- 传统数学研究通常由专业数学家组成的小团队针对深奥问题开展工作。
- 一种互补性方法是利用人工智能等现代技术，与广泛群体合作解决具有数学趣味的问题。
- 此类协作的典型案例包括Polymath项目、协作形式化验证项目以及方程理论项目(ETP)。
- ETP项目运用Lean形式化验证系统和自动定理证明器，在泛代数领域解决了超过2200万道真假命题判断题。
- 新启动的项目旨在将ETP成果提炼成简明易懂的'速查手册'。
- 该项目包含一项竞技挑战：设计不超过10KB的速查手册，用于提升廉价AI模型在真假判断题上的表现。
- 挑战赛第一阶段将在包含1200道题目（1000道简单题+200道难题）的公开测试集上评估速查手册效果。
- 前1000名入围者将晋级第二阶段，该阶段将采用更先进的模型并要求提供证明或反例。
- 赛事通过Zulip频道协调组织，提交截止日期为4月20日。
- 未来挑战可能会聚焦其他数学问题类型及协作研究模式。