CICM 2026 AI4Math Workshop 集中展示 LLM 辅助数学、MCP 接入证明助手、Lean benchmark 与自动猜想—反例—证明闭环

CICM 2026 的 AI4Math Workshop 于 9 月 25 日举行，议程覆盖机器学习调优的自动定理证明、flexiformal LLM-assisted mathematics、Wolfram 纯数学语义表示、PIDE MCP 连接 AI agents 与 Isabelle、10 个可扩展组合数学挑战的 Lean benchmark，以及 AutoGraphForge 的猜想生成—反例搜索—Lean proving 闭环。该 workshop 明确定位于连接 formalization、ATP、数学知识管理与 machine learning for mathematical reasoning 社区。