Harmonic

Aristotle API

Programmatic access to Aristotle, Harmonic's formal reasoning agent. Over HTTPS with an API key, submit Lean 4 proofs with `sorry` placeholders, natural-language math problems, or LaTeX papers; Aristotle fills sorries, formalizes documents into Lean 4, and returns only formally verified results. The API is asynchronous — submit a job and poll/download the result — and is driven primarily through the official aristotlelib Python SDK and `aristotle` CLI.

GitHub

Other Resources

🔗
SignUp
https://aristotle.harmonic.fun/auth/login?screen_hint=signup
🔗
Login
https://aristotle.harmonic.fun/auth/login
🔗
APIsJSON
https://raw.githubusercontent.com/api-evangelist/harmonic/refs/heads/main/apis.yml

API entry from apis.yml

apis.yml Raw ↑ 
name: Aristotle API
description: Programmatic access to Aristotle, Harmonic's formal reasoning agent. Over HTTPS with an API
  key, submit Lean 4 proofs with `sorry` placeholders, natural-language math problems, or LaTeX papers;
  Aristotle fills sorries, formalizes documents into Lean 4, and returns only formally verified results.
  The API is asynchronous — submit a job and poll/download the result — and is driven primarily through
  the official aristotlelib Python SDK and `aristotle` CLI.
humanURL: https://aristotle.harmonic.fun
baseURL: https://aristotle.harmonic.fun
tags:
- Formal Verification
- Theorem Proving
- Lean
- Mathematics
properties:
- type: SignUp
  url: https://aristotle.harmonic.fun/auth/login?screen_hint=signup
- type: Login
  url: https://aristotle.harmonic.fun/auth/login