Building an AI Mathematician with Carina Hong - The TWIML AI Podcast (formerly This Week in Machine Learning & Artificial Intelligence) Recap

Podcast: The TWIML AI Podcast (formerly This Week in Machine Learning & Artificial Intelligence)

Published: 2025-11-04

Duration: 56 min

Summary

In this episode, Karina Hong discusses her journey in mathematics and how her company Axiom aims to merge AI with mathematical reasoning. She highlights the importance of creating programming languages for mathematics to unlock new capabilities and markets.

What Happened

In this episode, host Sam Charrington welcomes Karina Hong, the founder and CEO of Axiom, to explore the intersection of AI and mathematics. Karina shares her lifelong passion for math, which began with Olympiad training, and her rigorous journey through research mathematics, particularly in number theory and combinatorics. She reflects on the challenges of research, where progress can often take months, and emphasizes the need for intuition in mathematical problem-solving. This sets the stage for her vision of an AI mathematician, which could potentially streamline the reasoning process in mathematics.

Karina outlines three key reasons she believes the timing is right for advancements in AI-driven mathematics. First, she discusses the improvements in AI models, particularly large language models (LLMs), that excel in reasoning and coding. Second, she highlights the growing popularity of formal programming languages like Lean, which help mathematicians verify proofs more efficiently. Lastly, she introduces the concept of code generation techniques, which, although often overlooked in the context of mathematics, could revolutionize how mathematical proofs are constructed and verified. By bridging these areas, Axiom aims to enhance mathematical productivity and open new markets.

Key Insights

Key Questions Answered

What is Axiom's approach to mathematical reasoning?

Axiom aims to build an AI mathematician by integrating AI, programming languages, and mathematics. Karina Hong believes that the timing is ripe due to advancements in AI models, the rise of formal languages like Lean, and the potential of code generation techniques. These elements together could unlock new capabilities in how mathematics is understood and applied.

How is Lean changing the landscape for mathematicians?

Lean allows mathematicians to write proofs in a way similar to computer programs. It ensures that each step in a proof follows logically from the previous one, providing immediate feedback on errors. This shifts the traditional pen-and-paper approach of mathematical reasoning into a more structured and verifiable digital format, enhancing the rigor and efficiency of mathematical work.

What is the significance of code generation in mathematics?

Karina mentions that code generation techniques have been largely overlooked in their application to mathematics. By leveraging these techniques, Axiom believes it can achieve significant performance gains in mathematical reasoning. This is particularly important given the vast disparity in available data for programming versus mathematical proofs.

Why is now a crucial time for investment in math and AI?

Karina identifies three converging factors: the advancements in AI reasoning capabilities, the growing adoption of formal programming languages among mathematicians, and the untapped potential of code generation techniques. Together, these trends suggest a ripe opportunity for innovation and new market creation in the field of mathematical reasoning.

What challenges do mathematicians face in research?

Karina describes the often arduous life of a research mathematician, where one can be stuck on a problem for months without progress. This highlights the need for tools that can streamline the verification of mathematical intuitions, allowing mathematicians to focus more on creativity and less on tedious verification, which could be addressed through AI advancements.