Hong Letong / 洪乐潼
Hong Letong is the mathematician and Axiom founder interviewed in 137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的. The episode presents her path from Guangzhou math competitions, MIT mathematics and physics, Oxford neuroscience, and Stanford law into AI For Math entrepreneurship.
Technical Position
Hong argues that an AI Mathematician needs more than a model that solves contest problems. The system needs Interactive Theorem Proving, Auto-Formalization, a growing knowledge base, conjecture generation, benchmark construction, and verification tooling around Lean Theorem Prover and Mathlib. She repeatedly frames Axiom as a systems and deep-tech company rather than a pure model company.
Founder View
The source presents Hong as a visionary founder who still prefers the stance of a learner. Her leadership view is bottom-up and service-oriented: the CEO should help the technical team move faster, while human mathematicians continue to supply intuition, question choice, taste, and adversarial benchmark design.
Connections
- Axiom and Axiom Prover — company and prover system she founded and describes.
- Shubo and Ken Ono — cofounder and senior mathematician connected to Axiom’s formation.
- AI For Math, AI Mathematician, Auto-Formalization, and Formal Verification — main technical themes she explains.
- Lean Theorem Prover, Mathlib, and Putnam Competition — formal system, library, and benchmark context in the episode.
- Research Taste, AI Organization Design, and Mathematical Abundance — human and organizational themes in her view of AI-era mathematics.