# Harmonic — Aristotle API

> Harmonic is a Palo Alto AI lab building Mathematical Superintelligence (MSI). Its product Aristotle is a formal reasoning agent that uses Lean 4 to prove and formally verify graduate- and research-level problems in math and software. The Aristotle API lets developers submit Lean 4 proofs with `sorry` placeholders, plain-English math problems, or LaTeX papers, and returns only formally verified results. Access is via an API key and the official Python SDK/CLI (aristotlelib). This llms.txt was generated by API Evangelist from the catalog; verify current details against Harmonic's own site.

## APIs
- [Aristotle API](https://aristotle.harmonic.fun): Async, API-key-authenticated formal-reasoning API — submit (fill sorries), formalize (document -> Lean 4), list, download.

## Getting started
- [Aristotle app / dashboard](https://aristotle.harmonic.fun): Sign in, then Dashboard -> API Keys to create a key.
- [Sign up](https://aristotle.harmonic.fun/auth/login?screen_hint=signup)
- [Log in](https://aristotle.harmonic.fun/auth/login)

## SDK & CLI
- [aristotlelib on PyPI](https://pypi.org/project/aristotlelib/): Official Python SDK and `aristotle` CLI. Install: `pip install aristotlelib` (Python >= 3.10). Authenticate with `ARISTOTLE_API_KEY` or `--api-key`.

## Repo artifacts
- [Packages / SDKs](packages/harmonic-packages.yml)
- [CLI command surface](cli/harmonic-cli.yml)
- [Authentication profile](authentication/harmonic-authentication.yml)
- [API conventions (async job model)](conventions/harmonic-conventions.yml)
- [Changelog (SDK releases)](changelog/harmonic-changelog.yml)
- [Lifecycle](lifecycle/harmonic-lifecycle.yml)
- [MCP server (community)](mcp/harmonic-mcp.yml)
- [Domain security probe](security/harmonic-domain-security.yml)

## Company
- [Website](https://www.harmonic.fun)
- [News / blog](https://harmonic.fun/news)
- [GitHub organization](https://github.com/harmonic-ai)
- [Terms of Use](https://aristotle.harmonic.fun/terms)
- [Privacy Policy](https://aristotle.harmonic.fun/privacy)