Harmonic 团队Aristotle 在IMO上实现金牌级别表现

hbghlyj

在 2025 年 IMO 上，Aristotle 实现了与金牌获奖者同等的解题能力，通过 Lean 4 证明助手验证，且无需人工校验，这些形式化证明现已公开托管于 GitHub。
Aristotle iOS 应用 Beta 版上线，支持自然语言与拍照双模式，并开放内测报名。用户在应用中提问时，不仅可获得英文解答，还能同步看到对应的 Lean 4 代码，支持拍照提问与多题并行处理。