牛透社 11 月 26 日消息，专注于形式化数学推理的人工智能初创公司 Harmonic AI 宣布完成 B 轮融资，融资金额达 1.2 亿美元，由 Ribbit Capital Management 领投，Sequoia Capital Operations、Intel Capital 与 Goldman Sachs 等跟投。

该公司于2023年创立，其主要产品是Aristotle，一个专注于形式数学推理的人工智能引擎。该引擎使用精益四证明助手，该证明助手允许用户以计算机可检查正确性的方式编写数学定义、定理和证明，将自然语言数学问题转化为形式可验证的证明。