Keep pulling the thread on Vlad Tenev & Tudor Akim.
Harmonic's AI system, Aristotle, achieved gold medal level performance at the 2025 International Mathematical Olympiad.
OpenAI and Google DeepMind also achieved gold medal level performance at the 2025 International Mathematical Olympiad using scaled chain-of-thought reasoning.
Formal proof systems like Lean obviate the need for manual human verification and traditional peer review in mathematics, as proofs can be automatically checked for correctness by the system's kernel.
The Aristotle system is capable of building new mathematical theories and structures on the fly, which may not exist in the Mathlib repository, and incorporating them into its proving process.
Tudor Akim predicts that the formal reasoning techniques used in Aristotle for mathematics will be applied to software verification to create a future with bug-free software.
Vlad Tenev predicts that the future of software development will be dominated by formal methods, with AI-generated code written in verifiable languages rather than languages optimized for human readability like Python and Java.
Users of Harmonic's public API have successfully solved Erdos problems that had remained unsolved for 30 to 40 years.
Tudor Akim predicts that by 2030, systems like Aristotle will produce multiple, competing, self-consistent theoretical explanations for all observable physical phenomena, such as unifying quantum mechanics and general relativity.
Harmonic is an AI research lab co-founded by Vlad Tenev and Tudor Akim with the goal of building mathematical superintelligence.
Harmonic's Aristotle system generates candidate proofs in the Lean programming language, which serves as a proof-checking assistant.
The Aristotle AI system's architecture includes a large transformer model that uses a Monte Carlo tree search strategy to discover valid reasoning paths.
The Aristotle AI system incorporates a specialized geometry module modeled on DeepMind's AlphaGeometry.