Jesse Han

Jesse Han is the co-founder and chief executive of Math, Inc., where he develops AI systems that turn advanced mathematics into machine-checkable proofs. A mathematician, former OpenAI researcher, and founder of Morph Labs, he has pursued a distinctive combination of formal mathematical verification, automated reasoning, and computing infrastructure for autonomous agents.

Han earned his doctorate in mathematics at the University of Pittsburgh under Thomas Hales. With Floris van Doorn, he produced a formal Lean proof of the independence of the continuum hypothesis, translating a foundational result about the limits of conventional mathematical axioms into a computer-verifiable artifact.

At OpenAI, Han worked on neural theorem proving, pairing language-model-generated mathematical steps with proof assistants that check their validity. He co-developed proof artifact co-training, which extracts training signals from the internal structure of existing formal proofs; in reported Lean experiments, the approach increased theorem-proving performance from approximately 32% to 48%. He also co-created miniF2F, a benchmark of Olympiad-level mathematical problems designed to evaluate automated reasoning across multiple proof systems.

Han subsequently co-founded Multi AI and founded Morph Labs. In 2023, he introduced Morph Prover, an openly released conversational assistant for Lean, while acknowledging practical limitations including fabricated lemmas and confusion between Lean versions. Morph later developed agent-native cloud infrastructure through Infinibranch, which lets computational environments be snapshotted, copied, restored, and explored in parallel.

• Verification as a condition of trust. Han pairs flexible AI-generated reasoning with external systems that can independently check whether an answer is correct. In mathematics, Lean provides that standard; his broader ambition is verified superintelligence whose outputs remain computationally inspectable.

• Reasoning-time branching. Han’s agent-infrastructure work uses identical copies of computational environments to let subagents investigate competing solutions simultaneously. A chess example illustrated how independently explored continuations can be evaluated by an external verifier and recombined into a stronger decision.

• Gauss and large-scale autoformalization. Math, Inc.’s Gauss converts sophisticated mathematical arguments into verified Lean code, including a formalization of the strong prime number theorem. It also contributed to verifying sphere-packing results in dimensions eight and twenty-four, building on mathematicians’ existing blueprints, code, and research.

• Open tools and stricter evaluation. OpenGauss provides an open-source autoformalization harness for interactive use, autonomous execution, and coordinated subagents. FormalQualBench extends Han’s interest in rigorous evaluation by testing whether formal proofs establish their intended claims without unauthorized axioms or specification loopholes.