# Harmonic (AI)

> Source: https://aiwiki.ai/wiki/harmonic_aristotle
> Updated: 2026-10-27
> Fact-checked: 2026-10-27
> Categories: AI Companies, AI for Science
> License: CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) - attribute to "AI Wiki (aiwiki.ai)"
> Cite as: AI Wiki. "Harmonic (AI)." aiwiki.ai, 27 Oct 2026. https://aiwiki.ai/wiki/harmonic_aristotle
> From AI Wiki (https://aiwiki.ai), the free encyclopedia of artificial intelligence. Reuse freely with attribution.

**Harmonic** is an American artificial intelligence company building what it calls mathematical [superintelligence](https://aiwiki.ai/wiki/superintelligence) (MSI), a system designed to reason about mathematics and related quantitative fields without producing false statements.[2] Its flagship model, **Aristotle**, generates solutions in the [Lean](https://aiwiki.ai/wiki/lean) proof assistant language and checks them with a formal verifier, so that any output the system presents as proven has been machine-verified down to the axioms.[8] The company was founded in 2023 by Tudor Achim, who serves as chief executive, and Vlad Tenev, the co-founder and chief executive of Robinhood, who serves as executive chairman.[16] Harmonic drew wide attention in July 2025 when it reported that Aristotle had reached gold-medal-level performance on the problems of the 2025 International Mathematical Olympiad, with every submitted solution formally verified in Lean.[1][29] It is based in Palo Alto, California.[30]

Harmonic has raised about $295 million across three rounds, most recently a $120 million Series C in November 2025 at a $1.45 billion post-money valuation, and in January 2026 the company said [Nvidia](https://aiwiki.ai/wiki/nvidia) had joined that round.[17][30][18] In March 2026 the company released Aristotle Agent, which it describes as an autonomous mathematician that turns problems written in English into formal proofs.[20] By October 2026 Aristotle's product site called it "the AI agent that proves software correct," and Harmonic's developer tools targeted the verification of Verilog hardware designs and C code alongside mathematics.[38][39]

Harmonic positions itself within the broader effort to apply [artificial intelligence](https://aiwiki.ai/wiki/artificial_intelligence) to rigorous reasoning. Its central thesis is that the [hallucination](https://aiwiki.ai/wiki/hallucination) problem of [large language models](https://aiwiki.ai/wiki/large_language_model) can be mitigated, and in mathematics eliminated, by requiring outputs to pass a formal check, an approach drawn from [automated theorem proving](https://aiwiki.ai/wiki/automated_theorem_proving) rather than from open-ended text generation.[13][17]

## Founding and leadership

Harmonic was founded in 2023 and announced its mission and first research results publicly on June 10, 2024.[16][25] According to Index Ventures, an early investor, Achim and Tenev formed the company after both became fascinated by the idea of using AI to solve a Millennium Prize problem.[13]

Tudor Achim is co-founder and chief executive. Before Harmonic he co-founded and was chief technology officer of Helm.ai, an autonomous-driving software company.[16] He worked on [machine learning](https://aiwiki.ai/wiki/machine_learning) at Quora and briefly pursued a PhD before leaving to co-found Helm.ai.[14] He holds a bachelor's degree in computer science from [Carnegie Mellon University](https://aiwiki.ai/wiki/cmu) and was a doctoral candidate in computer science at [Stanford University](https://aiwiki.ai/wiki/stanford_university).[16]

Vlad Tenev is co-founder and executive chairman. He is best known as the co-founder and chief executive of the retail brokerage Robinhood Markets, a role he has continued to hold while chairing Harmonic.[16] Tenev holds a bachelor's degree in mathematics from Stanford University and a master's degree in mathematics from UCLA.[16] Press coverage frequently identifies Harmonic through him; TechCrunch's July 2025 headline called it "the Robinhood CEO's AI math startup."[2]

When the Series A closed in September 2024, Sequoia partner Andrew Reed joined the founders on the board of directors and Index Ventures partner Jan Hammer joined as a board observer.[27] Kleiner Perkins partner Ilya Fushman became a board observer with the Series B in July 2025.[28] Harmonic was described as a roughly 20-person company at the time of its 2025 IMO result.[14] In January 2026 it told Axios that it had fewer than 30 employees and planned to grow to between 50 and 75, while spending much of its new funding on computing resources.[18]

## Aristotle and the formal-verification thesis

Aristotle is Harmonic's core system. Rather than emitting only natural-language argument, it works in Lean 4, an open-source proof assistant and functional programming language in which a proof is a program that the Lean kernel either accepts or rejects.[8] Harmonic's claim is that this makes the system hallucination-free within the domains it supports: a proof that compiles is correct by construction. Achim told TechCrunch that Aristotle "is the first product available to people that does reasoning and formally verifies the output," and that "within the domains that Aristotle supports, which are quantitative reasoning domains, we actually do guarantee that there's no hallucinations."[2]

Harmonic's first published result, in June 2024, was an early version of Aristotle evaluated on MiniF2F, a standard benchmark of competition-style problems, which the company re-formalized in Lean 4 and re-split into training, validation and test sets. It reported an 83% success rate when external computer algebra systems were allowed to solve simple subproblems and 63% in pure Lean.[25] A month later it reported 90% on MiniF2F in the first setting, released its corrected version of the benchmark, and added a natural-language interface that autoformalizes problems into Lean.[26]

According to the company's technical report, posted to [arXiv](https://aiwiki.ai/wiki/arxiv) on October 1, 2025 under the title *Aristotle: IMO-level Automated Theorem Proving*, the system combines three components: a Lean proof-[search engine](https://aiwiki.ai/wiki/search_engine); an informal-reasoning module that proposes and then formalizes intermediate lemmas, bridging from natural-language intuition to formal statements; and a dedicated geometry solver for the geometry problems that are awkward to express directly in Lean.[8] The report states that the system reaches state-of-the-art results on automated-theorem-proving benchmarks with favorable scaling.[8] It describes the proof search as a highly parallel Monte Carlo Graph Search guided by a large transformer that serves as both policy and value function, trained with [reinforcement learning](https://aiwiki.ai/wiki/reinforcement_learning) in the style of expert iteration on a large dataset of statements that an in-house autoformalization system converted into Lean. When deployed at scale, Aristotle also uses a form of [test-time training](https://aiwiki.ai/wiki/test_time_training), retraining on its own search traces when a problem remains unsolved.[8] The geometry solver is built on Yuclid, a C++ deduction engine that Harmonic open-sourced under the Apache 2.0 license.[8][43] Separately, the company has described a self-play and synthetic-data approach in which the model generates its own formal problem-and-proof pairs for training.[4][31] This formal approach, related to wider [mathematical reasoning](https://aiwiki.ai/wiki/mathematical_reasoning) research, distinguishes Harmonic from most of the [generative AI](https://aiwiki.ai/wiki/generative_ai) field and aligns it with the [AI-for-science](https://aiwiki.ai/wiki/ai_for_science) goal of verifiable machine-assisted discovery.

## The 2025 International Mathematical Olympiad claim

On July 28, 2025, Harmonic announced in a livestream on X that Aristotle had achieved gold-medal-level performance on the six problems of the 2025 International Mathematical Olympiad.[1][29] The system produced formally verified solutions to five of the six problems.[8] Five correct solutions equal 35 points, which was the gold-medal cutoff that year, and the same score reported by the systems from [Google DeepMind](https://aiwiki.ai/wiki/google_deepmind) and [OpenAI](https://aiwiki.ai/wiki/openai).[10][11][40] None of the AI systems solved Problem 6.[10][11] Harmonic published its formal Lean proofs for Problems 1 to 5 in a public [GitHub](https://aiwiki.ai/wiki/github) repository.[15]

The result came alongside parallel announcements from Google DeepMind, whose Gemini Deep Think model worked in natural language, and OpenAI, whose general-purpose model likewise produced natural-language proofs.[10][11] Several caveats attach to and differentiate these claims:

- Harmonic's result came from a formal test, meaning the problems were translated into a machine-readable format before the system attempted them.[2] The mathematician Emily Riehl, writing in *Scientific American*, noted that for the formal entries from Harmonic and ByteDance the questions had to be written to accommodate the models' language limitations, and that the systems "still needed days to figure it out."[12] By contrast, DeepMind said its model worked end to end in natural language from the official problem statements within the 4.5-hour competition time limit, and that its results were officially graded and certified by IMO coordinators.[40] OpenAI's natural-language solutions were marked by former IMO contestants.[11]
- The IMO's president, Gregor Dolinar, said the organization "cannot validate the methods [used by the AI models], including the amount of compute used or whether there was any human involvement, or whether the results can be reproduced."[12] Harmonic waited until July 28, the end of an informal embargo on AI-company announcements that ran until a week after the competition ended, although OpenAI and DeepMind had announced their results earlier.[11]
- The distinctive strength of Harmonic's claim is the nature of its evidence rather than its timing. Because the solutions are Lean proofs checked by a computer, a third party can in principle re-run the verifier and confirm correctness, which is not possible for a natural-language proof that depends on a human grader. The mathematician Kevin Buzzard, a specialist in formalized mathematics, noted that a formal proof that compiles is by definition a full-marks solution, while also cautioning that Harmonic gave no information about how the answers to the "determine the value" problems were supplied to the system, and that the announcements were not peer reviewed.[11] Buzzard also observed that, with no agreed rules, each company effectively made up its own rules.[11]

Harmonic's headline of "gold-medal-level performance" is therefore an unofficial result whose main advantage over its rivals is independent machine-checkability, offset by its reliance on formalized problem statements and a time budget longer than the competition's.

## Funding and valuation

Harmonic raised roughly $295 million across three rounds in about 14 months, reaching a $1.45 billion post-money valuation and unicorn status in November 2025.[17][30]

| Round | Date | Amount | Valuation | Lead investor(s) |
| --- | --- | --- | --- | --- |
| Series A | September 2024 | $75 million | $325 million post-money | [Sequoia Capital](https://aiwiki.ai/wiki/sequoia_capital) (with [Index Ventures](https://aiwiki.ai/wiki/index_ventures))[6][31] |
| Series B | July 2025 | $100 million | about $875 million | [Kleiner Perkins](https://aiwiki.ai/wiki/kleiner_perkins)[5][28] |
| Series C | November 25, 2025 | $120 million | $1.45 billion post-money | Ribbit Capital[3][30] |
| Total | -- | about $295 million | -- | -- |

The Series A also included Era Funds, GreatPoint Ventures, DST Global partners, Nikesh Arora and Jared Leto.[31] Paradigm participated significantly in the Series B, alongside Ribbit Capital, Sequoia Capital, Index Ventures and Charlie Cheever.[28] Some outlets reported the July 2025 Series B valuation as about $900 million; TechCrunch reported it as $875 million.[2][19]

The Series C, announced on November 25, 2025, was led by Ribbit Capital with participation from [Sequoia Capital](https://aiwiki.ai/wiki/sequoia_capital), [Index Ventures](https://aiwiki.ai/wiki/index_ventures), [Kleiner Perkins](https://aiwiki.ai/wiki/kleiner_perkins) and, as a new investor, the Emerson Collective.[3][30] Reuters described Harmonic as pre-revenue at the time, and Achim said the bulk of the money would go toward the computing power needed to train its models.[17][42] On January 15, 2026, Harmonic told Axios that Nvidia was joining the Series C, and SiliconANGLE reported that Nvidia's venture arm, NVentures, was among the round's investors, alongside Paradigm and Charlie Cheever as well as the investors named above.[18][19] The size of Nvidia's investment was not disclosed, and the roughly $295 million total reported in November 2025 predates it.[17][18]

## Product and access

On July 28, 2025, Harmonic launched a beta of an Aristotle app for iOS, with a waitlist and a gradual rollout; the app showed each answer in English together with the Lean code that verifies it.[29] TechCrunch described the launch as an iOS and Android chatbot app.[2] The company said it planned to release an application programming interface (API) for enterprises and a web app for consumers.[2] Harmonic made Aristotle available to the public through the API in October 2025.[16] In November 2025 it added support for plain-English input alongside native Lean, automated lemma generation and a streamlined terminal interface.[30]

In December 2025 Harmonic reported that the public API version of Aristotle resolved 96.8% of the 189 formal specifications in VERINA, a code-verification benchmark developed by researchers at UC Berkeley and Meta, proving 160 correct and showing 23 to be false.[22] Harmonic has also said that Aristotle shows promise in coding and chip design.[18] As of January 2026 the API was still a free beta, and the company said it was not ready to announce how or when it would charge for Aristotle.[18]

On March 17, 2026, Harmonic released Aristotle Agent, which it called "the world's first autonomous mathematician." The company said the agent can take math problems written in plain English, convert them into formal proofs and work for up to 24 hours without assistance, editing files directly inside Lean projects, and that it was available on the web, through a command-line interface and through the API, free of charge at launch.[20] Harmonic said Aristotle Agent ranked first in formal mathematics on ProofBench, a benchmark developed by [Vals AI](https://aiwiki.ai/wiki/vals_ai), outperforming its closest competitor by 15%; this is a company claim.[20] In April 2026 Harmonic said on X that Aristotle was "now powering formal verification of Solana smart contracts," sharing a post by an outside developer.[41]

By late October 2026 Aristotle's product site described it as "The AI agent that proves software correct," applying "the reasoning that earned IMO gold" to formal verification of software, hardware and mathematics.[39] Version 3.0.0 of `aristotlelib`, Harmonic's command-line tool and Python library for the Aristotle API, was published on October 27, 2026. Its documentation says Aristotle verifies Verilog and C code against properties a user states in English, returning a proof or a counterexample, that each run spends credits from the user's account, and that the service can also be reached through a hosted [Model Context Protocol](https://aiwiki.ai/wiki/model_context_protocol) server.[38]

## Research use and Erdős problems

Mathematicians and hobbyists began using Aristotle on open problems soon after its public release. In late November 2025 Tenev wrote on X that Aristotle had proved Erdős problem #124 in Lean "all by itself" after Boris Alexeev ran it on a beta version of the system.[34] The problem's page on erdosproblems.com records that Aristotle, run by Alexeev, provided and formalized in Lean a simple proof of the first of the problem's two questions.[33] Sébastien Bubeck of OpenAI noted that this was the "easy" version of #124 and that the hard version remained open.[35]

A January 2026 arXiv write-up by Nat Sothanaphan describes the resolution of Erdős problem #728 by a combination of OpenAI's [GPT-5.2](https://aiwiki.ai/wiki/gpt-5.2) Pro and Aristotle, operated by Kevin Barreto, whose final output was a formal proof in Lean. The write-up calls it the first Erdős problem regarded as fully resolved autonomously by an AI system.[32] Later papers report wider use: a March 2026 formalization of an equilibrium result for the Vlasov-Maxwell-Landau system used Aristotle to close 111 lemmas within a workflow that also used Gemini Deep Think and [Claude Code](https://aiwiki.ai/wiki/claude_code),[36] and a July 2026 paper presented solutions to eight problems from the Kourovka Notebook of open questions in group theory, all of which its authors say were autonomously discovered and formally verified in Lean by Aristotle.[37]

## Community programs and benchmarks

In January 2026 Harmonic announced $1 million in sponsorships for mathematicians, split between Principal Investigator Awards for research projects and Rising Mathematician Awards aimed mainly at undergraduates.[23] In February 2026 it made an inaugural $300,000 donation to the Lean Focused Research Organization (Lean FRO), describing Lean's formal verification system as the backbone of its mission.[24]

In July 2026 Harmonic and the American Institute of Mathematics (AIM) announced that they would jointly develop an open benchmark built from problems selected by working mathematicians. According to Axios, the initial set contains more than 50 number theory problems, ranging from generating examples to open research questions, and is meant to measure both whether models produce correct answers and whether they help mathematicians make progress on hard research problems. The two organizations said they would publish the benchmark materials and evaluation criteria.[21]

## Timeline

| Date | Event |
| --- | --- |
| 2023 | Harmonic founded by Tudor Achim and Vlad Tenev[16] |
| June 2024 | Public launch; first MiniF2F results[25] |
| September 2024 | $75 million Series A led by Sequoia Capital[31] |
| July 2025 | $100 million Series B led by Kleiner Perkins[28] |
| July 28, 2025 | IMO 2025 gold-medal-level claim; iOS app beta[29] |
| October 2025 | Aristotle technical report on arXiv; public API[8][16] |
| November 2025 | $120 million Series C led by Ribbit Capital; Erdős #124 claim[30][34] |
| December 2025 | 96.8% on the VERINA code-verification benchmark[22] |
| January 2026 | Nvidia joins Series C; Erdős #728 resolved with GPT-5.2 Pro; $1 million sponsorships[18][32][23] |
| February 2026 | $300,000 donation to Lean FRO[24] |
| March 2026 | Aristotle Agent released[20] |
| July 2026 | Benchmark partnership with the American Institute of Mathematics[21] |
| October 2026 | `aristotlelib` 3.0.0 for verifying Verilog and C code[38] |

## Reception

Harmonic's approach differs from that of most frontier labs, which pursue general-purpose language models and treat reliability as a property to be improved statistically. It stakes its case on formal verification: the claim that, by routing reasoning through Lean, it can offer a machine-checkable guarantee of correctness in mathematics. Mathematicians writing about the 2025 IMO results credited formal proofs with being uniquely trustworthy while criticizing the unofficial and self-defined nature of the AI entries.[11][12] The Erdős #124 announcement drew pushback because the version Aristotle solved was the easier one.[33][35] In an April 2026 interview with The Generalist, Achim predicted that "within 2 or 3 years, AI mathematicians will surpass human mathematicians for any specific mathematical task."[14]

## See also

- [List of neolabs](https://aiwiki.ai/wiki/list_of_neolabs)
- [Neolab](https://aiwiki.ai/wiki/neolab)
- [Axiom Math](https://aiwiki.ai/wiki/axiom_math)
- [AlphaProof](https://aiwiki.ai/wiki/alphaproof)
- [Lean (Theorem Prover)](https://aiwiki.ai/wiki/lean)
- [Mathlib](https://aiwiki.ai/wiki/mathlib)
- [Automated Theorem Proving](https://aiwiki.ai/wiki/automated_theorem_proving)
- [Terence Tao](https://aiwiki.ai/wiki/terence_tao)

## References

[1] [Harmonic Announces IMO Gold Medal-Level Performance & Launch of First Mathematical Superintelligence (MSI) AI App](https://www.businesswire.com/news/home/20250728394917/en/Harmonic-Announces-IMO-Gold-Medal-Level-Performance-Launch-of-First-Mathematical-Superintelligence-MSI-AI-App) - Business Wire, July 28, 2025.
[2] [Harmonic, the Robinhood CEO's AI math startup, launches an AI chatbot app](https://techcrunch.com/2025/07/28/harmonic-the-robinhood-ceos-ai-math-startup-launches-an-ai-chatbot-app/) - TechCrunch, July 28, 2025.
[3] [Harmonic Builds Momentum Towards Mathematical Superintelligence with $120 Million Series C](https://www.businesswire.com/news/home/20251125727962/en/Harmonic-Builds-Momentum-Towards-Mathematical-Superintelligence-with-$120-Million-Series-C) - Business Wire, November 25, 2025.
[4] [Harmonic AI raises $120M at $1.45B valuation to advance mathematical reasoning](https://siliconangle.com/2025/11/25/harmonic-ai-raises-120m-1-45b-valuation-advance-mathematical-reasoning/) - SiliconANGLE, November 25, 2025.
[5] [Harmonic Raises $100 Million Series B to Accelerate Development of Mathematical Superintelligence](https://www.businesswire.com/news/home/20250710118878/en/Harmonic-Raises-$100-Million-Series-B-to-Accelerate-Development-of-Mathematical-Superintelligence) - Business Wire, July 10, 2025.
[6] [Harmonic Announces Series A Funding Round To Accelerate Development of Mathematical Superintelligence](https://www.businesswire.com/news/home/20240923548068/en/Harmonic-Announces-Series-A-Funding-Round-To-Accelerate-Development-of-Mathematical-Superintelligence) - Business Wire, September 23, 2024.
[7] [Harmonic Raises $75M in Series A Funding](https://www.finsmes.com/2024/09/harmonic-raises-75m-in-series-a-funding.html) - FinSMEs, September 2024.
[8] [Aristotle: IMO-level Automated Theorem Proving](https://arxiv.org/abs/2510.01346) - Tudor Achim et al. (Harmonic), arXiv, October 1, 2025.
[9] [Aristotle: IMO-level Automated Theorem Proving (full text)](https://arxiv.org/html/2510.01346v1) - arXiv HTML, October 2025.
[10] [The 2025 IMO Winner's Circle: How Three AI Teams Got Gold in Very Different Ways](https://inferencebysequoia.substack.com/p/the-2025-imo-winners-circle-how-three) - Inference by Sequoia, July 30, 2025.
[11] [AI at IMO 2025: a round-up](https://xenaproject.wordpress.com/2025/08/03/ai-at-imo-2025-a-round-up/) - Kevin Buzzard, Xena Project, August 3, 2025.
[12] [Mathematicians Question AI Performance at International Math Olympiad](https://www.scientificamerican.com/article/mathematicians-question-ai-performance-at-international-math-olympiad/) - Emily Riehl (opinion), Scientific American, August 7, 2025.
[13] [Solving the AI Reasoning Gap: How Harmonic is Building Mathematical Superintelligence](https://www.indexventures.com/perspectives/solving-the-ai-reasoning-gap-how-harmonic-is-building-mathematical-superintelligence/) - Jan Hammer, Index Ventures.
[14] [How a 20-Person Startup Won Gold at the Math Olympiad](https://www.generalist.com/p/how-a-20-person-startup-won-gold) - The Generalist (interview with Tudor Achim), April 14, 2026.
[15] [harmonic-ai/IMO2025 (formal Lean proofs and verification artifacts)](https://github.com/harmonic-ai/IMO2025) - GitHub.
[16] [About Harmonic (founders and milestones)](https://harmonic.fun/about/) - Harmonic company site, accessed October 27, 2026.
[17] [Robinhood CEO's math-focused AI startup Harmonic valued at $1.45 billion in latest fundraising](https://finance.yahoo.com/news/robinhood-ceos-math-focused-ai-192706395.html) - Krystal Hu, Reuters via Yahoo Finance, November 25, 2025.
[18] [Exclusive: Nvidia investing in math AI startup Harmonic](https://www.axios.com/2026/01/15/nvidia-harmonic-ai-math-accuracy) - Ina Fried, Axios, January 15, 2026.
[19] [Nvidia's NVentures backs Harmonic AI in funding round for mathematical superintelligence](https://siliconangle.com/2026/01/15/nvidias-nventures-backs-harmonic-ai-series-c-mathematical-superintelligence/) - Duncan Riley, SiliconANGLE, January 15, 2026.
[20] [Robinhood CEO Vlad Tenev Touts 'Autonomous Mathematician' As Harmonic Unveils Aristotle Agent](https://tech.yahoo.com/ai/articles/robinhood-ceo-vlad-tenev-touts-023106081.html) - Ananya Gairola, Benzinga via Yahoo Tech, March 20, 2026.
[21] [Exclusive: Harmonic launches new AI math benchmark](https://www.axios.com/2026/07/20/harmonic-mathemeticians-ai-benchmarks) - Madison Mills, Axios, July 20, 2026.
[22] [Aristotle Learns to Code, Achieving New State-of-the-Art of 96.8% on Code Verification Benchmark](https://www.harmonic.fun/news/verina-benchmark/) - Harmonic, December 3, 2025.
[23] [Harmonic Announces Mathematician Sponsorships to Accelerate Mathematical Superintelligence](https://www.harmonic.fun/news/mathematician-sponsorships/) - Harmonic, January 22, 2026.
[24] [Powering the Future of MSI with Inaugural $300,000 Donation to Lean FRO](https://www.harmonic.fun/news/lean-fro-donation/) - Harmonic, February 11, 2026.
[25] [Introducing Harmonic: Our Mission and First Results](https://www.harmonic.fun/news/intro-harmonic/) - Harmonic, June 10, 2024.
[26] [One month in - A new SOTA on MiniF2F and more](https://www.harmonic.fun/news/minif2f/) - Harmonic, July 9, 2024.
[27] [Harmonic Closes Series A Funding Round](https://www.harmonic.fun/news/series-a/) - Harmonic, September 23, 2024.
[28] [Harmonic Announces Series B Funding](https://www.harmonic.fun/news/series-b/) - Harmonic, July 9, 2025.
[29] [Aristotle Achieves Gold Medal-Level Performance at the International Mathematical Olympiad, iOS App Beta Launch](https://www.harmonic.fun/news/imo-ios/) - Harmonic, July 28, 2025.
[30] [Harmonic Builds Momentum Towards Mathematical Superintelligence with $120 Million Series C](https://finance.yahoo.com/news/harmonic-builds-momentum-towards-mathematical-213000511.html) - Business Wire via Yahoo Finance, November 25, 2025.
[31] [Harmonic Announces Series A Funding Round To Accelerate Development of Mathematical Superintelligence](https://www.silicon.co.uk/press-release/harmonic-announces-series-a-funding-round-to-accelerate-development-of-mathematical-superintelligence) - Business Wire via Silicon UK, September 23, 2024.
[32] [Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof](https://arxiv.org/abs/2601.07421) - Nat Sothanaphan, arXiv, January 12, 2026.
[33] [Erdős Problem #124](https://www.erdosproblems.com/124) - Thomas Bloom, erdosproblems.com, last edited December 1, 2025.
[34] [Post announcing Aristotle's proof of Erdős Problem #124](https://x.com/vladtenev/status/1994922827208663383) - Vlad Tenev on X, November 30, 2025.
[35] [Post on the "easy" version of Erdős Problem #124](https://x.com/SebastienBubeck/status/1995159227170701753) - Sébastien Bubeck on X, November 30, 2025.
[36] [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://arxiv.org/abs/2603.15929) - Vasily Ilin, arXiv, March 16, 2026.
[37] [On Some Problems from the Kourovka Notebook](https://arxiv.org/abs/2607.17477) - Wouter van Doorn, Elias Judin, Pietro Monticone and Daniel Morrison, arXiv, July 20, 2026.
[38] [aristotlelib (Aristotle SDK and command-line tool)](https://pypi.org/project/aristotlelib/) - Harmonic, Python Package Index, version 3.0.0, October 27, 2026.
[39] [Aristotle: The AI agent that proves software correct](https://aristotle.harmonic.fun/) - Harmonic, accessed October 27, 2026.
[40] [Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad](https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/) - Google DeepMind, July 21, 2025.
[41] [Post: "Aristotle now powering formal verification of Solana smart contracts"](https://x.com/HarmonicMath/status/2041938768735957100) - Harmonic on X, April 8, 2026.
[42] [Announcing Our Series C Funding As We Build Momentum Towards Mathematical Superintelligence (MSI)](https://www.harmonic.fun/news/series-c/) - Harmonic, November 25, 2025.
[43] [How Aristotle Achieved its IMO Gold Medal-Level Performance](https://www.harmonic.fun/news/imo-gold/) - Harmonic, October 2, 2025.