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

Work with this as data

Every API here is available over the APIs.io API and to AI agents over MCP.

MCP server

One button, every client — Claude, Cursor, VS Code and the rest.

https://apis.io/mcp

Tools for apis

7 MCP tools reach this
  • find_apisBrowse and filter every API in the catalog.
  • get_api_artifactsOne API's artifacts, grouped by type.
  • get_openapiThe primary OpenAPI for this API.
  • find_similar_apisAPIs that look like this one.
  • apis_io_searchSTART HERE — APIs, providers and tags for one query, each with its total.
  • resolveTurn a domain, URL or GitHub org into the provider it belongs to.
  • find_cohortsEvery scored population of providers in the catalog.
All 92 tools →

Call it yourself

curl for this page
This API 
curl "https://apis.io/api/v1/apis/aristotle-api"
All apis 
curl "https://apis.io/api/v1/apis?limit=25"

Discovery needs no key. Ratings and market analysis are Pro.

Get an API key

Free tier, no email required.

GitHub Google LinkedIn

A second provider on the same verified email joins the account you already have.

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