# Aristotle API

**Canonical:** https://apis.io/apis/harmonic/aristotle-api/  
**Provider:** Harmonic — https://apis.io/providers/harmonic/  
**Base URL:** https://aristotle.harmonic.fun  
**Documentation:** https://aristotle.harmonic.fun

Aristotle API is published by [Harmonic](https://apis.io/providers/harmonic/) on the [APIs.io](https://apis.io/) network. Tagged areas include Formal Verification, Theorem Proving, Lean, and Mathematics.

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.

## Machine-readable artifacts (3)

- **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

## Tags

Formal Verification, Theorem Proving, Lean, Mathematics

---

Profiled by [API Evangelist](https://apievangelist.com) and published on [APIs.io](https://apis.io/apis/harmonic/aristotle-api/). The API's provider profile, Kin Score and agent-readiness rating are at https://apis.io/providers/harmonic/.