Carina Hong: AI for Math, Lean, Proofs from The Book

Duration: 263 min · ▶ Watch on YouTube

Guest: Carina Hong 洪乐潼 · Founder and CEO of Axiom

Switch → 中文

Chapters (41)

  • 00:00 · Introduction
    • Introduction of Carina Hong, her background, and her startup Axiom.
  • 02:16 · The Beauty and Definition of Math
    • Carina discusses the ‘struck by lightning’ moments in math and defines math as a structural language.
  • 06:01 · Is Math Discovered or Invented?
    • A discussion on whether math is discovered or invented, using Ramanujan and Hardy as examples.
  • 08:28 · Intuition vs. Brute Force in Math
    • Carina explains her ‘brute-force’ approach to math competitions and discusses DeepMind’s AlphaGeometry.
  • 11:01 · AI’s Role in Mathematics
    • Exploring how AI acts as a brute-force collaborator and the difference between Automated and Interactive Theorem Proving.
  • 14:41 · Growing Up in Guangzhou and Attention Management
    • Carina shares her childhood in Guangzhou and introduces the concepts of bounded vs. free attention.
  • 18:13 · Founder Archetypes
    • Categorizing founders into Visionaries, Executors, and Salesmen, with examples like Mark Zuckerberg and Elon Musk.
  • 23:33 · Navigating MIT and Dealing with Failure
    • Carina recounts her time at MIT, realizing she wasn’t a ‘genius’, and learning to choose her battles.
  • 40:01 · The Pain Addiction of Founders
    • Discussing why founders endure the pain of startups and the psychological traits required to succeed.
  • 50:00 · Leadership and Math Competitions
    • The guest discusses her views on servant leadership and her early experiences building a ‘Lego universe’ in math competitions.
  • 51:37 · Choosing MIT and Undergraduate Studies
    • She explains her strong desire to attend MIT, writing it on scratch paper, and her decision to study math and physics.
  • 54:09 · Academic Honors and Research
    • The guest talks about receiving the Morgan Prize and her undergraduate research in number theory with Professor Ono.
  • 57:45 · Master’s at Oxford and Shift to AI
    • She describes her transition from wet-lab neuroscience (fruit fly experiments) to computational neuroscience and AI during her Master’s at Oxford.
  • 01:01:05 · Law School Interests and Interdisciplinary Thinking
    • The guest discusses her interest in law, debate at the Oxford Union, and how legal textualism intersects with her technical background.
  • 01:06:30 · Founding Axiom and Meeting Her Co-founder
    • She recounts meeting her co-founder Shubho at Verve Coffee and the decision to drop out of her Stanford PhD to start an AI for math company.
  • 01:15:00 · The Landscape of AI for Math
    • The guest analyzes the history and current state of AI applied to formal mathematics, mentioning key figures and milestones.
  • 1:40:00 · The Grueling Fundraising Process
    • The founder describes the repetitive and exhausting nature of early-stage fundraising and facing initial rejections.
  • 1:45:00 · Securing the First Term Sheets
    • The turning point in fundraising when prominent investors like Howard Morgan showed interest, leading to multiple offers.
  • 1:50:00 · The Pressure of High-Stakes Decisions
    • Discussing the intense pressure young founders face, referencing Peter Thiel’s aggressive negotiation with Mark Zuckerberg.
  • 1:55:00 · Seed Round and Team Execution
    • Details of the $64M seed round at a $300M valuation and the team’s rapid execution in building the infrastructure.
  • 2:00:00 · Axiom vs. DeepSeek and OpenAI
    • Explaining why Axiom is a deep-tech company akin to SpaceX, rather than just another model company like DeepSeek.
  • 2:05:00 · Solving IMO Problems and the Math Club
    • The company’s success in solving complex math problems and attracting top mathematicians to their ‘Math Club’.
  • 2:10:00 · Rejecting OpenAI’s Acquisition Attempt
    • The founder recounts how OpenAI attempted to acqui-hire her team and why she chose to stay independent.
  • 2:15:00 · The Future of Human Mathematicians
    • Predicting that AI will handle the computation, while human mathematicians will focus on providing intuition and direction.
  • 2:20:00 · Tackling the Putnam Competition
    • The team’s intense effort to solve the Putnam competition, achieving a near-perfect score under ‘wartime’ conditions.
  • 2:25:00 · Expanding Math into Other Fields
    • Discussing how mathematical formalization can be applied to fields like law and economics.
  • 2:30:00 · Math and Code as Twin Brothers
    • Discussing the Curry-Howard correspondence and how math and code are fundamentally linked.
  • 2:31:33 · The ChatGPT Moment for AI for Math
    • Predicting a breakthrough moment for AI in mathematics, similar to ChatGPT or AlphaGo.
  • 2:33:39 · Technical Paradigms in AI for Math
    • Exploring the ‘Draft, Sketch, and Prove’ paradigm and the use of formal languages like Lean.
  • 2:42:29 · Generalization: Proving, Conjecturing, and Formalization
    • Breaking down the AI for Math landscape into proving theorems, making conjectures, and auto-formalization.
  • 2:52:21 · Coding vs. Math and Software Verification
    • Comparing AI’s capabilities in coding versus math, and highlighting software verification as a key application.
  • 3:02:58 · Commercialization and Market Potential
    • Discussing the commercial viability of formal verification in software and hardware.
  • 3:11:50 · AGI vs. ASI
    • Debating the path to Artificial General Intelligence versus Artificial Super Intelligence.
  • 200:00 · The Lean Data Shortage and Synthetic Data
    • The guest discusses the scarcity of Lean data for formal verification and how AI can be used to generate synthetic data.
  • 204:00 · AI for Science vs. AI for Math
    • A comparison between the slow iteration cycles of AI for Science (wet labs) and the purely digital, fast-paced nature of AI for Math.
  • 208:00 · Ramanujan and Mathematical Intuition
    • The guest shares stories about Ramanujan to illustrate the difference between intuitive mathematical discovery and formal proof.
  • 211:00 · Pre-training vs. Post-training in AI
    • A discussion on whether mathematical intuition is a product of pre-training and how current AI models focus heavily on post-training.
  • 215:00 · Competing with Big Tech
    • The guest explains the competitive landscape involving OpenAI, DeepMind, and Anthropic, and how startups can move faster.
  • 220:00 · Startup Philosophy and Binary Outcomes
    • Reflections on Peter Thiel’s views on monopolies, Elon Musk’s SpaceX, and the binary success/failure nature of ambitious startups.
  • 230:00 · The Desire to Be an Apprentice
    • The guest shares her personal goal of wanting to be an ‘intern’ to continuously learn across various fields like math, physics, and law.
  • 235:00 · Company Culture and Mathematical Heroes
    • A look into the company’s culture, including naming conference rooms after mathematicians like Gauss, Turing, and Lovelace.

Specific Numbers (26)

Time Fact Value Context
00:38 Axiom’s valuation after Series A funding $160 million Mentioned during the introduction of Carina Hong’s startup.
00:46 Age gap between employee and founder 57-year-old professor working for a 24-year-old Highlighting the unique dynamic at Axiom.
08:10 Fields Medal awarded to James Maynard 2022 Mentioned while discussing different proof techniques in mathematics.
10:05 AlphaGeometry’s success rate 81% The percentage of historical IMO geometry problems solved by DeepMind’s AlphaGeometry.
12:23 First Putnam math competition 1927 Referencing the history of the Putnam competition.
12:18 Perfect scores in Putnam history 5 human perfect scores, AI achieved the 6th Discussing the breakthrough of AI in solving complex math competitions.
01:05:06 Kenny Luo started working on Lean 2020 Mentioning when her friend started working on formal verification.
01:06:24 Meeting at Verve Coffee 1000 cups Joking about the number of coffees bought while discussing startup ideas with her co-founder.
01:14:50 Reading group duration 1.5 years The time spent discussing ideas before officially starting the company.
01:26:50 HOList project start 2016 Early efforts in AI for math at Google by Christian Szegedy and Yuhuai Wu.
01:27:15 GPT-f project 2019-2020 OpenAI’s early work on formal math supported by Ilya Sutskever.
01:27:44 AlphaGeometry success 2024 DeepMind’s system solving IMO geometry problems.
1:40:05 Valuation increase 3x The company’s valuation increased three times from the first offer to the final offer.
1:48:30 Seed round valuation $300 million The seed round was raised at a $300 million valuation.
1:49:08 Seed round funding amount $64 million The company raised $64 million in their seed round, exceeding their $50 million target.
1:59:57 DeepSeek Prover performance 11% DeepSeek Prover achieved 11% on a specific benchmark.
2:00:00 Axiom’s performance on benchmark 98.93% Axiom’s system achieved 98.93% on the same benchmark.
2:00:31 Series A valuation $1.6 billion The company reached a $1.6 billion valuation in their Series A round.
2:00:36 Series A funding amount $200 million+ The company raised at least $200 million in their Series A.
2:21:12 Putnam competition score 80/120 The AI achieved a score of 80 out of 120 on the Putnam competition, placing it in the top 5.
2:32:32 DeepMind AlphaGeometry score 28 points Achieved in 2024, marking an AlphaGo-like moment for AI in math.
2:41:15 Draft, Sketch and Prove paper publication 2022 A key paradigm introduced for AI theorem proving.
2:58:06 Donald Knuth’s vision 1980s The era when Donald Knuth proposed literate programming and formalizing code.
3:01:30 Amazon automated reasoning code 260,000 lines The amount of proof code written over 3-5 years to verify a hypervisor component.
202:28 Company Headcount Growth 15 to 30 The company grew from 15 employees in December to 30 employees currently.
202:37 Competitor Headcount 50 to 75 The guest estimates their main competitor has between 50 and 75 employees.

Research Claims & Predictions (13)

  • [11:01] AI in math can be divided into intuitive/smart AI and brute-force AI.
    • evidence: Based on the current development of AI models that either mimic human intuition or rely on massive computational power.
  • [13:31] Interactive Theorem Proving (ITP) is the future of human-AI collaboration in math.
    • evidence: AI is transitioning from just solving problems automatically (ATP) to working alongside humans to prove theorems interactively.
  • [01:04:30] AI can be used to interpret legal texts and the Constitution.
    • evidence: Applying LLMs to historical documents to understand original public meaning, treating it as a structured data problem.
  • [01:06:00] Formal verification (Lean) can transform math into code.
    • evidence: Treating math problems as coding problems allows AI to tackle them more effectively, moving from natural language to formal logic.
  • [01:20:00] Scaling alone might not be enough for AI in math.
    • evidence: Contrasting with speech or vision, math might require new architectures or data generation strategies beyond just scaling compute.
  • [2:24:50] AI will transition society from ‘math-poor’ to ‘math-rich’.
    • evidence: As AI solves complex mathematical problems exponentially faster, the supply of mathematical proofs and discoveries will explode.
  • [2:25:55] The role of human mathematicians will shift towards providing intuition.
    • evidence: Instead of doing the manual calculation and proof-writing, humans will direct the AI on which problems are important and provide the high-level intuition.
  • [2:31:33] AI for Math will have a ChatGPT moment.
    • evidence: Driven by the integration of formal verification and large language models.
  • [2:46:02] Auto-formalization is a major bottleneck.
    • evidence: Translating natural language math into formal code (like Lean) is currently harder than proving the theorems.
  • [2:52:21] Software verification is the first major commercial market for AI for Math.
    • evidence: The ability to formally verify code will revolutionize software engineering before general math AI is achieved.
  • [3:11:50] ASI (Artificial Super Intelligence) will precede AGI.
    • evidence: AI will achieve superhuman performance in specialized domains (like math or verification) before becoming generally intelligent across all human tasks.
  • [201:30] AI can effectively generate synthetic data for Lean.
    • evidence: By using AI to synthesize data, companies can overcome the bottleneck of scarce human-written formal proofs.
  • [211:40] Mathematical intuition may be a result of pre-training.
    • evidence: The guest hypothesizes that Ramanujan’s ‘intuition’ was essentially a highly optimized pre-trained state, whereas current AI math efforts are focused on post-training.

Key Concepts (17)

  • [04:36] Math as a structural language
    • Math is a civilization system built upon axioms that humanity agrees are true, upon which complex structures are built.
  • [14:05] Automated Theorem Proving (ATP)
    • Using computers to automatically prove mathematical theorems based on predefined rules.
  • [14:08] Interactive Theorem Proving (ITP)
    • A collaborative process where humans and computers work together to prove theorems, with AI acting as an assistant.
  • [15:55] Bounded vs. Free Attention
    • Bounded attention is focusing strictly on required tasks (like answering emails), while free attention allows the mind to wander and generate creative, strategic thoughts.
  • [01:02:50] Originalism / Textualism
    • Legal philosophies focusing on the original public meaning or the strict text of the Constitution, which she relates to structured data analysis.
  • [01:05:08] Formal Verification (Lean)
    • Using programming languages to write and verify mathematical proofs with absolute certainty, turning math into code.
  • [01:06:09] Math as Code
    • The idea that formalizing math turns it into a software engineering problem, making it amenable to AI tools.
  • [2:02:12] Formalization (形式化)
    • The process of translating mathematical problems and proofs into a strict, machine-readable language (like Lean) so that computers can verify their correctness.
  • [2:03:17] Program Synthesis
    • The automatic generation of computer programs to solve specific problems, used by Axiom to bridge the gap between natural language math and formal code.
  • [2:23:52] Axiom (公理)
    • A self-evident truth in mathematics that requires no proof, chosen as the name of the company to reflect its foundational goals.
  • [2:30:30] Curry-Howard Correspondence
    • The direct relationship between computer programs and mathematical proofs.
  • [2:41:15] Draft, Sketch, and Prove
    • A paradigm where an informal proof is drafted, formalized into a sketch, and then rigorously proven using an AI prover.
  • [2:46:02] Auto-formalization
    • The process of automatically translating natural language mathematics into a formal, machine-verifiable language like Lean.
  • [2:52:21] Formal Verification
    • The act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property.
  • [200:26] Lean
    • A formal proof verification language used to mathematically prove that code or theorems are correct.
  • [201:34] Synthetic Data Generation
    • Using AI models to create artificial data (in this case, formal math proofs) to train other models when human data is scarce.
  • [211:45] Pre-training vs. Post-training
    • Pre-training is the initial phase of training an AI on vast amounts of raw data to build intuition, while post-training refines it for specific tasks like formal verification.

People Mentioned (35)

  • Carl Friedrich Gauss — Mentioned regarding the ‘struck by lightning’ moment of sudden mathematical insight.
  • Srinivasa Ramanujan — Used as an example of a mathematician with unexplainable, alien-like intuition.
  • G. H. Hardy & J. E. Littlewood — Mathematicians who worked to formally prove Ramanujan’s intuitive findings.
  • Yitang Zhang — Mentioned for his famous proof regarding bounded gaps between primes.
  • James Maynard — Mentioned for his 2022 Fields Medal and proof techniques.
  • Henry Cohn — MIT professor who gave Carina a sphere packing problem.
  • Evan Chen — IMO coach whose complex geometry diagram was solved by AI.
  • Mark Zuckerberg — Used as a prime example of an ‘executor’ type founder.
  • Elon Musk — Used as an example of a ‘visionary’ type founder.
  • Sam Altman — Used as an example of a ‘salesman’ type founder.
  • Mike Schroepfer (Schrep) — Mentioned as a visionary CTO at Facebook who complemented Zuckerberg.
  • Sheryl Sandberg — Mentioned as a strong executor who helped scale Facebook.
  • Prof. Ono — The guest’s undergraduate research advisor in number theory.
  • Kenny Luo — A friend from MIT who introduced her to Lean and formal verification.
  • Shubho — The guest’s co-founder at Axiom.
  • Tudor — CEO of a competing AI for math company.
  • Christian Szegedy — Pioneer in AI for math, worked on HOList.
  • Yuhuai (Tony) Wu — Researcher who worked on AI for math at Google and later founded xAI.
  • Ilya Sutskever — Supported early AI for math efforts at OpenAI.
  • Howard Morgan — Investor who showed early belief in the company, boosting the founder’s confidence.
  • Jim Simons — Legendary mathematician and founder of Renaissance Technologies, mentioned as a connection.
  • Peter Thiel — Investor known for aggressive negotiation tactics, referenced in the Zuckerberg story.
  • Matt Murphy — Partner at Menlo Ventures who led the investment in Axiom.
  • Ken Ribet — Prominent math professor who interacted with the Axiom team regarding math proofs.
  • Francois Chollet — AI researcher who joined the Axiom team, known for his work on ARC.
  • David Silver — Co-author of a paper on learning from experience.
  • Richard Sutton — Co-author of a paper on learning from experience.
  • Terence Tao — Renowned mathematician involved in formalizing mathematics.
  • Kevin Buzzard — Mathematician advocating for the use of Lean in formalizing math.
  • Donald Knuth — Computer scientist who envisioned formalizing code in the 1980s.

Companies Mentioned (20)

Facebook (Meta) · Axiom · Google DeepMind · MIT · Oxford University · Stanford University · Meta · Baidu · Anthropic · OpenAI · B Capital · First Round Capital · Facebook · Menlo Ventures · DeepSeek · SpaceX · DeepMind · Amazon · Cadence · Essential AI

Notable Quotes (13)

Math is a bit like humanity deciding to create a civilization system, and within this system, we build upon axioms we agree are true. — Carina Hong @ 04:43

I am a brute-force player. If you give me a geometry problem, I will just use complex numbers to forcefully calculate it. — Carina Hong @ 08:45

Free attention is what separates an average founder from a highly strategic and decisive one. — Carina Hong @ 16:42

Everything we think is impossible is possible. — Axiom Founder @ 01:07:16

I think the risk of the technology is not as high as I initially thought. — Axiom Founder @ 01:14:26

我们这顿饭不吃完，你不签，我这个东西我现在撕掉。 — Peter Thiel (quoted by guest) @ 1:50:38

不要再去精确的搞这些东西了，现在是战争状态，能怎么快捷的去做就怎么快捷的去做。 — Axiom Founder @ 2:20:51

Math is code and code is math. — Guest @ 2:30:26

Anything you can define, you can prove. — Guest @ 2:52:26

I don’t really like the term AGI. I think we are building ASI (Artificial Super Intelligence). — Guest @ 3:14:15

Ramanujan’s kind of natural, intuitive state might actually be a product of pre-training. — Guest @ 211:41

Monopoly leads to stagnation, competition leads to mediocrity. — Guest @ 220:05

I am currently a disciple of the ‘Don’t Die’ movement. — Guest @ 249:48

Career Arc & Personal Stories (11)

  • [14:52] Carina grew up in Guangzhou, enjoying the local food and spending her walks to school thinking about math problems.
  • [23:33] During her math competition days, she realized she wasn’t a natural ‘genius’ at geometry, so she developed a brute-force method using complex numbers to solve problems.
  • [34:00] At MIT, she was surrounded by brilliant peers and realized she couldn’t compete on pure genius alone, leading her to find her own unique path and drop out of classes where she felt she couldn’t win.
  • [51:37] She was obsessed with attending MIT, writing the letters on her scratch paper during exams to motivate herself.
  • [57:45] Realized during her Master’s at Oxford that she preferred computational AI over wet-lab neuroscience experiments with fruit flies.
  • [01:06:30] Spent a year and a half discussing ideas with her future co-founder at Verve Coffee before deciding to drop out of her Stanford PhD and start Axiom.
  • [1:40:00] The founder shares the grueling experience of early fundraising, facing numerous rejections, and having to repeat the same pitch while balancing her studies and exams.
  • [1:51:51] She recounts a ziplining event with other female founders where she had to overcome her fear and take a leap of faith, comparing it to the entrepreneurial journey of making high-stakes decisions with incomplete information.
  • [2:09:14] OpenAI reached out to acquire her team. Despite the prestige, she declined the offer because she wanted to build her own vision and felt that joining a larger company would compromise her goals.
  • [2:49:38] The guest shares a personal anecdote about studying algebraic geometry during the pandemic and learning the term ‘germ’ (which means bacteria in everyday English but has a specific mathematical meaning), illustrating the gap between natural language and mathematical terminology.
  • [230:00] The guest shares that her ultimate dream isn’t necessarily to be a CEO forever, but to be an ‘intern’ or apprentice. She loves the idea of jumping into new fields—like computational neuroscience, physics, or law—and learning from the ground up.

Tools & Models Discussed (15)

  • AlphaGeometry: An AI model by Google DeepMind that solves complex IMO geometry problems by converting them into symbolic expressions.
  • Lean: A formal proof programming language used by mathematicians for Interactive Theorem Proving.
  • Lean: A formal proof verification system and programming language used to digitize mathematics.
  • HOList: An early environment for machine learning of higher-order logic proofs developed at Google.
  • GPT-f: An automated theorem prover based on generative pre-trained transformers developed at OpenAI.
  • AlphaGeometry: An AI system by DeepMind that solves complex geometry problems at an Olympiad level.
  • Lean: A formal proof verification language used to translate and verify mathematical proofs.
  • DeepSeek Prover: An AI model developed by DeepSeek for mathematical reasoning and proofs.
  • Monte Carlo Tree Search (MCTS): A search algorithm used in AI to explore possible solutions, mentioned as being too computationally expensive for some of their early approaches.
  • Lean: A functional programming language and theorem prover used heavily for formalizing mathematics.
  • Isabelle: An older, established interactive theorem prover.
  • Coq: Another established interactive theorem prover.
  • AlphaGeometry: An AI system by DeepMind that solves complex geometry problems at an Olympiad level.
  • Lean: A theorem prover and programming language used for formal verification of mathematics.
  • Transformer: The underlying neural network architecture mentioned in the context of the ‘Attention Is All You Need’ paper.

Topics

AI for Mathematics · Automated vs Interactive Theorem Proving · Founder Archetypes · Math Competitions and Education · Attention Management · AI for Mathematics · Formal Verification · Startup Founding Journey · Interdisciplinary Research (Math, Law, AI) · Academic Career vs. Entrepreneurship · AI in Mathematics · Startup Fundraising · Formal Verification · Deep Tech Entrepreneurship · Venture Capital Negotiation · AI for Mathematics · Formal Verification · Theorem Proving · Auto-formalization · Lean Programming Language · AGI vs ASI · AI for Mathematics · Formal Verification · Synthetic Data · Startup Strategy · Pre-training vs Post-training

Takeaways

  • AI is transforming mathematics from a purely human endeavor to a collaborative human-AI process through Interactive Theorem Proving.
  • Founders generally fall into three categories: Visionary, Executor, and Salesman. Successful companies require a complementary mix of these traits.
  • Free attention is crucial for creative problem-solving and strategic leadership, distinguishing great founders from average ones.
  • Not all successful mathematicians or researchers rely purely on ‘genius’; brute-force calculation and persistent effort are highly effective strategies.
  • Formal verification languages like Lean are bridging the gap between abstract mathematics and AI.
  • Interdisciplinary thinking, such as applying AI to legal textualism, can spark novel startup ideas.
  • The field of AI for math has evolved rapidly from early experiments in 2016 to Olympiad-level systems in 2024.
  • Founding a deep-tech startup often requires a long period of ideation and building conviction before taking the leap.
  • Fundraising for deep-tech AI startups requires immense resilience and the ability to handle repeated rejections.
  • Having a strong, contrarian vision (like focusing on formalization rather than just LLM scaling) can attract top-tier investors and talent.
  • AI will fundamentally change the field of mathematics, shifting the human role from calculation and manual proof-writing to providing high-level intuition.
  • Young founders must learn to make high-stakes decisions quickly, even with incomplete information.
  • The intersection of AI and mathematics is moving towards formal verification, where proofs are written in code (like Lean) and verified by machines.
  • Auto-formalization (translating human math to code) is currently a bigger bottleneck than the actual theorem proving.
  • The first massive commercial application of ‘AI for Math’ will likely be in software and hardware verification, ensuring code is bug-free.
  • The development of AI is likely to result in Artificial Super Intelligence (ASI) in specific domains before achieving broad Artificial General Intelligence (AGI).
  • AI for Math has a much faster iteration cycle than AI for Science because it doesn’t rely on physical wet labs.
  • The biggest bottleneck in formal verification AI is the lack of human-written Lean data, making synthetic data generation crucial.
  • Startups can compete with Big Tech by moving faster and taking on binary, high-risk bets.
  • Mathematical intuition (like Ramanujan’s) can be thought of as highly optimized pre-training, whereas formal proof generation is a post-training task.