PeopleofSuperintelligence

Researcher

Bhavik Mehta

Bhavik Mehta is a mathematician whose work spans Lean formalization and AI theorem proving. He began formalizing mathematics in Lean in 2019 and coauthored work on Hall’s Marriage Theorem, Szemerédi’s Regularity Lemma, and an exponential Ramsey bound. In 2025, he coauthored a Nature paper presenting Google DeepMind’s AlphaProof, a reinforcement-learning agent that learns to find formal proofs. In 2026, he coauthored a paper reporting formal verification of the dimension-eight sphere-packing result, with the final stages completed by Math, Inc.’s Gauss model. As of October 2026, he is a Chapman Fellow in Mathematics at Imperial College London and a Mathlib maintainer.

Works
3
Citations
10
h-index
2

Publication numbers from OpenAlex, as of 18 October 2026.

Timeline

  1. Since 2019

    Beginning formalization in Lean

    He begins formalizing mathematics in Lean in 2019.

  2. 2021

    Hall’s Marriage Theorem

    He coauthors a Lean formalization of Hall’s Marriage Theorem for the mathlib library in 2021.

  3. 2022

    Szemerédi’s Regularity Lemma

    With Yaël Dillies, he formalizes a strong version of Szemerédi’s Regularity Lemma in Lean in 2022 and applies it to Roth’s theorem.

  4. 2023

    A formal Ramsey bound

    He formalizes an exponential improvement to a Ramsey-number upper bound in Lean in 2023, before referees finish checking the result.

  5. 2025

    Working on AlphaProof

    In 2025, he is a research fellow at Imperial College London, where he works with Kevin Buzzard, and holds a mathematics PhD from Cambridge supervised by Timothy Gowers. He coauthors the Nature paper presenting Google DeepMind’s AlphaProof, a reinforcement-learning agent that learns to find formal proofs.

  6. 2026

    Formalizing sphere packing

    He is among the coauthors of a 2026 paper reporting the formal verification of the dimension-eight sphere-packing result; Math, Inc.’s Gauss model completes the final verification stages.

  7. As of October 2026

    Chapman Fellow at Imperial

    As of October 2026, he is a Chapman Fellow in Mathematics at Imperial College London and a Mathlib maintainer.

Career

  1. Since 2025Imperial College LondonResearch Fellow

Education

  1. University of CambridgePhD

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. Formalising Szemerédi’s Regularity Lemma in Lean2021 · 5 citations
  2. Formalising the Kruskal-Katona Theorem in Lean2022 · Lecture notes in computer science · 3 citations
  3. Formalising Sharkovsky’s Theorem (Proof Pearl)2023 · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) · 2 citations

From OpenAlex, as of 18 October 2026.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes Imperial College London. Our estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.
  2. The company share of AI researchers’ top papers rose from 3% to 32%Includes Imperial College London. We estimate where leading AI researchers worked when their most-cited papers appeared. The company share rose from 3% in 1975–1979 to 32% in 2020–2024.
  3. Google has the highest combined h-index among AI organizationsIncludes Imperial College London. Our estimates of combined and median h-index at AI organizations, using current affiliations and OpenAlex records.
  4. Stanford University trained or employed 27 of the 111 AI major-prize winners, more than any other universityIncludes Imperial College London. Stanford University trained or employed 27 of the 111 AI major-prize winners, more than any other university. We compare doctorate and employment links for major-prize and best-paper winners.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Bhavik Mehta yet. Send us a free-licensed photo.

  1. Mathlib maintainers leanprover-community.github.io. Checked 18 October 2026.
  2. Formalizing Hall's Marriage Theorem in Lean arxiv.org. Checked 18 October 2026.
  3. Formalising Szemerédi’s Regularity Lemma in Lean drops.dagstuhl.de. Checked 18 October 2026.
  4. Formalising (part of) the Diagonal Ramsey Paper cst.cam.ac.uk. Checked 18 October 2026.
  5. Co-piloting proofs lims.ac.uk. Checked 18 October 2026.
  6. Olympiad-level formal mathematical reasoning with reinforcement learning nature.com. Checked 18 October 2026.
  7. A Milestone in Formalization: The Sphere Packing Problem in Dimension 8 arxiv.org. Checked 18 October 2026.
  8. b-mehta (Bhavik Mehta) · GitHub github.com. Checked 18 October 2026.