**AI Agent 尝试低成本证明黎曼猜想**

_Watch an AI agent try to prove the Riemann hypothesis on the cheap_

> 该项目展示了一个基于 Lean 4 和 Qwen3.5 2B 模型的 AI Agent，在 CPU 环境下全天候尝试证明黎曼猜想。系统通过 Rust 服务调用 Lean REPL 进行严格验证，仅当预测结果通过 Lean 检查且符合数学事实时才计入进展。Agent 利用多臂老虎机算法选择研究方向，并在 SurrealDB 中存储记忆与推理轨迹，体现了低成本 AI 在复杂数学证明中的探索。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-products
- **发布时间**：2026-09-29 00:48（北京时间）
- **原文**：[打开原文](https://www.zeyaddeeb.com/experiments/proofs)