Aristotle

Aristotle is a mathematical reasoning system developed by Harmonic, an American AI startup co-founded by Vlad Tenev and Tudor Achim, designed to produce formally verified mathematical proofs by combining a large language model with the Lean 4 proof assistant. The system pairs an informal-reasoning component, a Lean proof search system, and a dedicated geometry solver, then verifies every solution against Lean before returning an answer to the user. Harmonic announced that Aristotle reached gold medal level performance on the 2025 International Mathematical Olympiad with formally verified solutions to five of six problems, a result the company has framed as a first for any AI system.

At a glance

• Lab: Harmonic
• Released: Public beta announced July 28, 2025, alongside the IMO 2025 result. Technical paper posted October 2025 on arXiv.
• Modality: Text input and output, specialized for mathematical reasoning and formal proof generation.
• Open weights: No. Aristotle is a closed commercial system. Harmonic published Lean proof artifacts for the IMO 2025 problems in a public GitHub repository under harmonic-ai/IMO2025, but the underlying model weights are not released.
• Context window: Not separately disclosed; the system handles full Olympiad problem statements and the surrounding proof search context.
• Pricing: Not publicly disclosed for the consumer chatbot tier or the API. The consumer Aristotle app is available on iOS, Android, and the web, with enterprise API access introduced through harmonic.fun/aristotle.
• Distribution channels: Aristotle web app, iOS and Android consumer apps, and an enterprise API.

Origins

Harmonic was founded in 2023 by Vlad Tenev (co-founder of Robinhood) and Tudor Achim, with Achim taking the chief executive role. The company's research thesis was that the dominant limitation of contemporary language model AI in technical work was the inability to produce verifiable reasoning, and that the correct way to close that gap was a model that returned only outputs which could be machine checked against a formal proof system. The Aristotle research program was the operational expression of that thesis.

The model architecture combines three parts. The first is an informal reasoning system based on a large language model that drafts candidate proofs and lemmas in natural language. The second is a Lean proof search component that translates those drafts into formal Lean 4 statements and attempts to close the proof through search. The third is a dedicated geometry solver that handles the structurally distinct geometry problems characteristic of high level Olympiad mathematics. Each Aristotle answer is verified by Lean before it is returned, and the verification step is algorithmic rather than learned, so a proof either type checks or it does not.

The 2025 International Mathematical Olympiad result was the principal capability disclosure for the model. Harmonic announced on July 28, 2025 that Aristotle had produced formally verified Lean 4 solutions for five of the six 2025 IMO problems, with the company publishing the Lean statement files and proofs for problems one through five in a public GitHub repository. The IMO is the principal high school level mathematics competition globally and produces problems intentionally designed to be unfamiliar and to require novel reasoning, so the IMO benchmark has been treated by mathematicians and by industry coverage as a high signal capability test for any reasoning system.

The technical paper, "Aristotle: IMO-level Automated Theorem Proving," was posted to arXiv in October 2025 (arxiv.org/abs/2510.01346) and provides the architectural detail and the IMO 2025 result writeup. The paper accompanies the company's broader November 2025 Series C funding announcement, which closed at a $1.45 billion post money valuation and has been characterized in industry coverage as institutional confirmation of Aristotle's capability standing.

Capabilities

Aristotle is built specifically for problems that admit a formally verifiable answer. The model's distinguishing capability is the production of Lean 4 proofs that compile and verify without human intervention, rather than natural language reasoning traces of the kind produced by general purpose chain of thought models. The verification guarantee is structural: if a proof passes Lean, the result is correct in the formal sense that Lean enforces.

The architecture separates informal and formal reasoning. The informal reasoning component drafts proof outlines and candidate lemmas in natural language, drawing on a large language model trained on mathematical content. The proof search component then attempts to formalize the draft in Lean 4, with iterative refinement when the formal step fails. The geometry solver is invoked when the problem class warrants it, and Olympiad geometry problems represent a substantial share of the IMO surface where dedicated solvers have a long tradition in automated theorem proving research.

The system targets high difficulty mathematics rather than the broad capability surface of general purpose models. Aristotle does not write code, hold open ended dialogue, or perform retrieval. The product positioning is that mathematics itself, treated as the verifiable kernel of technical reasoning, is the right domain for a first generation formally verified AI system, and that adjacent verification heavy domains (software verification, hardware verification) are natural successor targets.

Benchmarks and standing

The principal disclosed benchmark is the 2025 International Mathematical Olympiad. Aristotle produced formally verified Lean 4 solutions for five of six problems, a result Harmonic and industry coverage have characterized as gold medal level performance. The verification is the structural innovation: other AI systems have reported high scoring natural language solutions on Olympiad problems, but the Aristotle result is distinguished by the machine checkable Lean proofs that accompany the solutions.

Standard horizontal foundation model benchmarks (Artificial Analysis Intelligence Index, LMArena, GPQA Diamond, SWE-bench Verified, AIME) do not directly apply to Aristotle's architecture, which treats output validity as a verification problem rather than a sampled completion. The closest comparison points are AlphaProof and AlphaGeometry from Google DeepMind, the Lean proof generation work in academic theorem proving research, and the AI for math programs at frontier labs that have published Olympiad results in natural language form.

Industry coverage has consistently characterized the IMO 2025 result as a substantial capability disclosure for the formal mathematics AI segment, while noting that translation from Olympiad style problems to applied verification deployment is a separate commercial question. Benchmark leadership in formal mathematics is a different shape than benchmark leadership in general purpose language modeling, since formal verification produces a binary correctness signal rather than a continuous score.

Access and pricing

Aristotle is accessible through three surfaces. The Aristotle consumer chatbot is available as a beta on the web at aristotle.harmonic.fun, as iOS and Android apps, and through an enterprise API. The consumer surfaces are positioned as hallucination free tools for math students and researchers. The enterprise API is positioned for institutions that want Olympiad grade mathematical reasoning embedded in research, education, or verification workflows.

Per token pricing for the API has not been publicly disclosed in the company's announcements. Consumer subscription tiers and enterprise contract terms are negotiated through the Harmonic website. Lean proof artifacts for the IMO 2025 problems are published in the public harmonic-ai/IMO2025 repository on GitHub for verification and research reproduction.

The model itself is closed weights. Harmonic has framed the product strategy around mathematical superintelligence as a commercial offering rather than as an open weights research release.

Comparison

Direct competitors and adjacent reasoning systems:

• AlphaProof and AlphaGeometry (Google DeepMind). The closest research peer. AlphaProof and AlphaGeometry reached silver medal level on the 2024 IMO and were the first AI systems to reach Olympiad medal levels on natural language problem statements. The DeepMind systems use a similar combination of formal verification (Lean) and dedicated geometry reasoning, but they are research systems rather than commercial products with consumer or enterprise access. Aristotle's distinctive position is the productized commercial form factor.
• AxiomProver (Axiom Math). The principal commercial peer in formal mathematics AI. Axiom Math has emphasized Putnam results and an autonomous proof of an open number theory conjecture, with technical positioning around its Lean substrate and academic mathematics research credibility. The two companies are widely characterized as the leading formal mathematics AI insurgents of the 2023 to 2026 cohort.
• General purpose reasoning models from frontier labs. Models such as o1, o3, and successor systems from OpenAI, Claude reasoning variants from Anthropic, Gemini Deep Think from Google DeepMind, and DeepSeek R1 produce natural language chain of thought solutions on math benchmarks. These models score well on AIME and adjacent competition benchmarks but do not produce Lean verifiable proofs. The trade off is breadth of capability against verification guarantees.
• Academic Lean proof generation research. A long line of academic work in automated theorem proving, including Coq and Lean research at Carnegie Mellon, MIT CSAIL, Stanford, and elsewhere, supplies the substrate of theorem proving methods on which Aristotle and AlphaProof both build.

Aristotle's distinctive position among May 2026 formally verified mathematical AI systems is the combination of Olympiad level capability evidence, productized consumer and enterprise distribution, and the Tenev co founder profile that has anchored institutional investor visibility for the lab.

Outlook

Open questions for Aristotle and Harmonic over the next 6 to 18 months:

• Beyond IMO. The IMO result established gold medal level capability on a single year's problems. The pace of subsequent capability disclosures, including unsolved conjecture progress, Putnam coverage, and broader research mathematics applications, will signal whether Aristotle generalizes beyond the prepared training distribution.
• Applied verification deployment. Harmonic has stated software and hardware verification as adjacent target domains. The translation from competition mathematics to commercial verification customers is the principal commercial test for the model line.
• Pricing transparency and developer access. The lack of publicly disclosed API pricing limits independent capability and cost benchmarking. As enterprise rollout proceeds, pricing transparency will affect comparison with general purpose reasoning models on cost per verified proof.
• Research output cadence. The October 2025 Aristotle paper documented the IMO result. Whether successor releases continue at a research publication cadence will affect the model's standing in the academic theorem proving community.
• Competitive dynamics with AlphaProof and AxiomProver. The two principal peer programs operate at different commercial scales and with different research framings. Comparative results disclosure on shared benchmarks (Putnam, IMO, AIME, FrontierMath) will shape the segment's evolution.

Sources

• Aristotle: IMO-level Automated Theorem Proving (arXiv). Technical paper from the Harmonic team covering architecture, Lean integration, and IMO 2025 results.
• Harmonic Announces IMO Gold Medal-Level Performance (Business Wire). July 2025 announcement of the Aristotle app and IMO result.
• GitHub: harmonic-ai/IMO2025. Public repository with Lean statement files and proofs for the IMO 2025 problems.
• Aristotle API site. Product and API access page.
• TechCrunch: Harmonic launches an AI chatbot app. Coverage of the consumer app launch.
• Business Wire: Harmonic builds momentum towards mathematical superintelligence with $120 Million Series C. November 2025 Series C announcement.
• Mindplex: Harmonic's AI Aristotle claims solution to historic math puzzle. Coverage of Aristotle capability disclosures.