Map / Core AI / Frontier Labs / Harmonic

Harmonic

Mathematical superintelligence lab behind the Aristotle proof agent

OrganizationAI for Science Labs

Products by Harmonic

AristotleAI agent that proves maths and code correct with Lean proofsCoding Agents

People mark and rate products, not organizations. Open a product to say you use it.

About

Harmonic is an AI lab working toward what it calls mathematical superintelligence: models whose answers come with machine-checked proofs in the Lean language. Its model and agent, Aristotle, reached gold-medal level at the 2025 International Mathematical Olympiad and is offered as a web app and Python SDK for formal maths and software verification. It was co-founded by Tudor Achim and Vlad Tenev.