AI4Math Radar｜用 AIHOT 做了一个 AI for Mathematics 研究雷达

[Charlie-Wang-03]

🧭 AI4Math Radar｜用 AIHOT 做了一个 AI for Mathematics 研究雷达

最近拿 AIHOT 做了一个数学方向的版本，叫 AI4Math Radar。

一开始想得很简单。把信源换成 AI for Mathematics，把筛选标准改一遍，再跑起来就行。

真做下去以后，我发现最麻烦的地方其实是 怎么判断一条消息到底算不算 AI4Math，以及能把它说到什么程度。

比如一篇论文说模型“解决了一个开放问题”，我还得继续往下看。

• 是模型自己声称做出来了，还是作者检查过？
• 有没有领域专家复核？
• 有没有 Lean、Coq 这类机器验证？
• 形式证明通过了，形式化的命题是不是原来那个问题？
• 同一件事几天后出了论文、补了验证、被媒体重新报道，还要不要再记一条？

这些问题后来慢慢变成了这个项目真正花时间的地方。

🔎 现在主要看什么

目前 AI4Math Radar 主要追踪这些方向：

• 数学推理模型
• 自动定理证明与 proof search
• 形式化数学与 autoformalization
• AI 辅助数学发现
• benchmark、数据集与评测
• AI4Math 研究工具和重要生态进展

我也把历史事件从 2022 年开始往回补了一遍。

补历史时一个很明显的感受是，AI4Math 这几年变化非常快。

2022 年大家还在研究怎么让语言模型和 theorem prover 配合，到了 2024 年已经能做到 IMO medal level。2025 到 2026 年以后，AI 开始越来越频繁地碰真正的 research mathematics。

🛠️ 目前怎么运行

我保留了 AIHOT 的不少基础设施和思路，但现在选择了一套比较轻的运行方式：

公开资料
↓
ChatGPT 检索、去重和证据审查
↓
Git 记录
↓
CI 确定性校验
↓
GitHub Pages 发布

现在这套方案已经比较稳定，运行成本也很低。

项目最近刚发了第一个版本 v0.1.0。我也把日常维护里反复踩过的坑整理成了一套 editorial contract，包括：

• 一件事到底应该记哪一天
• 哪些报道算重复
• 什么情况值得单独记成后续事件
• 机器验证到底能说明到哪一步
• 为什么一个时间段完全可以 0 条收录

我更希望这个项目保持“小而准”，而不是为了每天都有内容硬塞新闻。

🚀 下一步想做什么

现在的 ChatGPT + GitHub + GitHub Pages 对我来说已经够用，但我不准备让项目一直停在这里。

如果后面能遇到同样对 AI4Math 感兴趣、愿意一起折腾的朋友，我希望继续把它做成一个真正持续运行的网站。

想继续补的东西包括：

• 更完整的信源采集
• 持续更新
• 事件归组
• 检索与订阅
• 更清楚的数学证据等级
• 更自然地展示“模型生成、专家复核、机器验证、独立确认”等状态

这部分我很希望和真正关心 AI4Math 的人一起做。

如果你在做 数学、形式化证明、AI Agent、网站工程，或者只是长期在跟这个领域，都欢迎交流。

🌱 和 AIHOT 的关系

这个项目是基于 AIHOT 开源框架做出来的。感谢卡兹克把整套东西开源出来，也正因为有这个框架，我才没有从零重新搭采集、筛选和发布系统。

AI4Math Radar 是我独立维护的项目，不是 AIHOT 官方项目。

🔗 项目链接

GitHub
https://github.com/Charlie-Wang-03/ai4math-radar

在线版
https://charlie-wang-03.github.io/ai4math-radar/

v0.1.0 Release
https://github.com/Charlie-Wang-03/ai4math-radar/releases/tag/v0.1.0

如果这里也有人在做 AI4Math、形式化数学，或者拿 AIHOT 改过别的垂直领域，欢迎聊聊。

也欢迎对这个项目下一步真正跑成一个长期网站感兴趣的朋友，一起做。

[KKKKhazix]

谢谢分享，写得很认真。“模型声称 / 作者核对 / 专家复核 / 机器验证”这样分级判断能说到什么程度，对别的行业也很有参考价值。