Harmonic 发布 Aristotle：融合 informal reasoning、Lean proof search 与 geometry solver，达到 IMO 2025 金牌级 formal proving

Harmonic 团队发布 Aristotle，一个将 Lean proof search、自然语言 reasoning / lemma generation / formalization 与专用 geometry solver 组合的 formal theorem-proving system。论文报告其在 2025 IMO 题目上达到 gold-medal-equivalent performance，并强调 test-time scaling 与 formal verification 的组合。