Jesse Han

Jesse Han, also published as Jesse Michael Han, is the founder of Morph Labs and a researcher in neural theorem proving. His collaborative research developed training methods and benchmarks for language-model theorem provers. At AI Engineer World’s Fair 2025, he presented a complementary infrastructure agenda: give AI agents computing environments they can copy, explore in parallel and evaluate against verification conditions.[2][4][5][3]

In his 2025 keynote, Han asked, “what if we had more empathy for the machine?” His practical answer was to build environments that could keep pace with agents’ reasoning. He described Morph’s Infinibranch as virtualization, storage and networking technology that could snapshot, branch and replicate entire cloud virtual machines in a fraction of a second. Saved environments let agents backtrack or explore alternative actions from a common starting state.[3]

Han illustrated the approach with parallel agents trying different ways to start a server on port 8000. Each began from a prepared snapshot; one attempt failed, another succeeded, and the successful workspace could pass into the next part of the workflow. He called the snapshot chains “Git for compute”: setup steps could mutate an environment, with their resulting states reused much like Docker’s cached layers.[3]

He distinguished ordinary reasoning-time tool use from reasoning-time branching: an agent could replicate its environment during deliberation, delegate exploration to sub-agents and recombine their results. His chess demonstration used a restricted chess engine to evaluate positions—a verifier in that example, rather than a formal proof checker. Han reported that branching found the correct move in less wall-clock time than the earlier run, without supplying numerical timing or a controlled benchmark.[3]

Han framed alignment as fundamentally a language problem, arguing that natural language’s limitations called for a computational language with algorithmic guarantees of correctness. His proposed “verified superintelligence” would use external software and formal verification to inspect and improve its reasoning, then produce algorithmically checkable outputs. This was his research ambition, rather than an alignment solution established by the demonstrations.[3]

At the same keynote, Han announced Christian Szegedy’s appointment as Morph’s chief scientist and identified the demonstrations as running on very early checkpoints of Magi One. He described plans to train that model to use Infinibranch for branching and verified reasoning, forecasting Q1 2026 arrival. He also announced Morph Liquid Metal, describing container support, millisecond branching and planned GPU support with a Q4 2025 forecast. These were the schedules announced in 2025.[3][1]

Before these infrastructure announcements, Han had worked on formal proofs and language-model theorem proving. That earlier research supplies concrete mathematical context for his later proposals about verification.[6][4][5][3]

Han and Floris van Doorn coauthored A Formal Proof of the Independence of the Continuum Hypothesis, published at CPP 2020 and submitted to arXiv in February 2021. Their Lean formalization used Boolean-valued models and forcing arguments for both directions: Cohen forcing for the consistency of the hypothesis’s negation and sigma-closed forcing for its consistency. This was formal-mathematics work, distinct from his subsequent neural theorem-proving research.[6]

With Jason Rute, Yuhuai Wu, Edward W. Ayers and Stanislas Polu, Han coauthored Proof Artifact Co-training for Theorem Proving with Language Models, first submitted in February 2021. PACT addressed scarce training data by extracting self-supervised examples from kernel-level proof terms and co-training on them alongside tactic prediction. The authors reported that their Transformer-driven Lean theorem prover’s success rate rose from 32% to 48% on the paper’s held-out test suite.[4]

Han also coauthored miniF2F with Kunhao Zheng and Stanislas Polu. First submitted in August 2021 and published at ICLR 2022, it provided a shared benchmark for neural theorem proving across formal systems. The paper described a benchmark of 488 formal problem statements from the AIME, AMC, International Mathematical Olympiad and classroom mathematics, targeting Metamath and Lean with partial support for Isabelle and HOL Light.[5]

Han received his University of Pittsburgh PhD in 2023 under Tom Hales, studying large language models’ applications to neural theorem proving. He was a senior research scientist at OpenAI, contributing to GPT-4 and automated theorem proving for mathematical Olympiad problems, before being identified as Morph’s founder and CEO in an April 2024 University of Washington seminar. In that seminar’s abstract, he argued that mathematical research would soon become predominantly AI-assisted and that frameworks such as Lean would help make mathematics legible to both humans and AI reasoning systems at scale.[2]