用途：面向形式化验证与定理证明，用于补全 Lean4 证明中的 sorry 空洞，并对错误命题自动生成反例。
主要能力：支持英文描述或 Lean4 代码两种输入；可结合项目定理、lake 依赖与 Mathlib 使用；提供 PROVIDED SOLUTION 注释标签标记解答区域。资料给出的基准成绩为 MiniF2F 90%、VERINA 96.8%。
使用方式：API 端点为 aristotle.harmonic.fun，采用 Auth0 认证，需在 harmonic.fun 注册登录。典型用法是在定理的 by 块中保留 sorry，由 Aristotle 填充；也可用注释写入英文命题描述。
适用场景：Lean4 形式化证明补全、反例搜索、与现有 Lean 项目集成。
限制：资料未提供具体收费、价格、调用配额、速率限制及完整安装命令；实际可用性依赖 Harmonic 账号与 API 访问权限。