面向AI的拉马努金挑战赛

要点

• 挑战赛发布一组关于数学常数的待证明或已证明的公式，用于测试AI的数学推理能力。
• 提交截止日期为2026年8月1日，优先接受形式化证明（如Lean、Rocq等），其次为基于CAS的推导或人类可读证明。
• 所有提交需附有可重现的代码和文档，且不能使用2026年7月1日之后才公开的工具或隐藏的远程服务。