2025年7月，美国初创公司Harmonic推出面向IOS和Android的聊天机器人测试版，其AI模型Aristotle以“零幻觉”数学推理能力引发关注。Aristotle在第66届国际数学奥林匹克(IMO2025)中斩获金牌，并在MiniF2F测试集中取得90%的成功率，领先于OpenAI、谷歌等巨头。Harmonic由Robinhood创始人Vlad Tenev和AI专家Tudor Achim联合创立，成立两年估值接近9亿美元，已获红杉资本、凯鹏华盈等顶级机构投资。Aristotle基于Lean形式化验证技术，通过严格逻辑约束解决AI幻觉问题，适用于金融建模、科学推理等高精度领域。尽管面临DeepSeek、谷歌AlphaProof等强劲对手，Harmonic凭借独特技术路线和资本支持，成为AI数学推理领域的新兴力量。