How a 20-Person Startup Won Gold at the Math Olympiad—Tying With OpenAI & DeepMind (Tudor Achim, CEO of Harmonic)

Speaker A: Aristotle is the world's first mathematical agent. You can delegate a mathematical reasoning task to Aristotle via the API, and it'll think for a long time and it'll give you an answer. And the really cool thing about it is that it's always correct. You can ask a math LLM a question and it'll give you an answer that looks very, very plausible. The dream of software engineering since day one was to produce programs that had proofs of correctness. And the reason why we don't have that is that for every line of code that you write, you might have to write 20 lines of code to verify it.

But you can imagine if you have an AI system that can specify functionality, formalize it, write proofs of correctness. All of a sudden, I would actually question why would you write any software that's not verified. By 2030, we will have 5 theories unifying quantum mechanics and general relativity, and we won't know which is correct because they all are equally plausible and correct. But we'll have to do higher and higher energy physics experiments to determine which one's right. So just because an AI can create like a logically consistent explanation of something no human has been able to create before doesn't mean that it fully solves every single, like, open problem in the world.

Speaker C: Last July, a 20-person startup won gold at the International Math Olympiad, tying with OpenAI and Google DeepMind in the process. Speaker B: It solved 5 of 6 problems, and unlike its much larger rivals, every proof was formally verified checked step by step. Speaker C: The company is Harmonic, and its CEO is Tudor Akeem, a PhD dropout and serial founder who believes that formal mathematical proof is the necessary infrastructure layer to create truly trustworthy AI. Today, Tudor and I discuss how he started a company with Robinhood CEO Vlad Tenev, why hallucinations may be the key to machine originality, and his extraordinary claim that by 2030, AI will have generated theoretical explanations for essentially everything.