PeopleofSuperintelligence

Researcher

Huajian Xin

Also known as 辛华剑

Huajian Xin is an AI researcher who trains large language models to write formal mathematical proofs in the Lean proof assistant. After studying logic at Sun Yat-sen University, he interned at DeepSeek, where he was first author of DeepSeek-Prover and DeepSeek-Prover-V1.5 in 2024 and appeared among the authors of the DeepSeek-V3 technical report. In 2025, his APE-Bench tested AI agents on proof-engineering tasks drawn from the commit histories of formal math libraries, and he coauthored Seed-Prover, which fully proved 5 of the 6 problems at IMO 2025. He is a PhD student at the University of Edinburgh supervised by Wenda Li and a student researcher on ByteDance's Seed team in London.

Timeline

  1. By 2023

    Logic and LEGO-Prover

    He studies philosophy, with a focus on logic, at Sun Yat-sen University with a minor in mathematics, and counts Xiaodan Liang among his mentors. In 2023, he coauthors LEGO-Prover with Xiaodan Liang and others, which gives language models a growing library of verified lemmas to reuse as skills in theorem proving.

  2. 2024

    DeepSeek-Prover at DeepSeek

    He interns at DeepSeek and leads research on the DeepSeek-Prover series. The first DeepSeek-Prover paper, posted in May 2024 with him as first author, fine-tunes DeepSeekMath 7B on 8 million synthetic Lean 4 statements with proofs and reaches 46.3% on the miniF2F test with 64 samples.

  3. June 2024

    A TechTalks interview on Lean

    In a June 2024 TechTalks interview, he says the main motivation behind DeepSeek-Prover is to advance formal mathematics. He calls proof languages such as Lean the future of mathematics and describes how DeepSeek-Prover turns existing math problems into verifiable Lean 4 proofs.

  4. August 2024

    DeepSeek-Prover-V1.5 and RMaxTS

    In August 2024, he is first author of DeepSeek-Prover-V1.5, an open-source Lean 4 prover refined through reinforcement learning from proof assistant feedback. With RMaxTS, a Monte-Carlo tree search variant, it reaches 63.5% on the miniF2F test set and 25.3% on ProofNet.

  5. December 2024–April 2025

    DeepSeek-V3 and Prover-V2

    He appears among the authors of the DeepSeek-V3 technical report in December 2024, which describes a mixture-of-experts language model with 671B total parameters. In April 2025, he coauthors DeepSeek-Prover-V2, whose 671B model reaches 88.9% on the MiniF2F test and solves 49 of 658 PutnamBench problems.

  6. 2025

    APE-Bench at Edinburgh

    By March 2025, he is a PhD student at the University of Edinburgh under Wenda Li and an intern on ByteDance's Doubao/Seed team. In April 2025, he is first author of APE-Bench with Luming Li, Xiaoran Jin, Jacques Fleuriot and Wenda Li, a benchmark that extracts proof-engineering tasks from real library commit histories.

  7. July 2025

    Seed-Prover at IMO 2025

    In July 2025, he coauthors Seed-Prover, a lemma-style whole-proof reasoning model for Lean built by ByteDance's Seed team. Paired with the Seed-Geometry engine, it fully proves 5 of the 6 problems at IMO 2025, a silver-medal-level result.

  8. As of October 2026

    Student researcher at ByteDance Seed

    He is a PhD student in artificial intelligence at the University of Edinburgh, supervised by Wenda Li, and a student researcher on ByteDance's Seed team in London. In December 2025, he coauthors Seed-Prover 1.5, which solves 11 of the 12 Putnam 2025 problems within 9 hours.

  1. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI from 1961 to 2025, with a year-by-year chart.
  2. The United States employs an estimated 53% of people in our data with a known employment countryOur estimates of where AI careers are concentrated now and how countries’ shares of dated positions changed over time.
  3. 46% of living people in our data with known birth and employment countries work outside their birth countryOur estimate of cross-border careers in AI, from country of birth and the country of each current organization.
  4. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionOur estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.

Sources and credits

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

  1. Huajian Xin's Blog – Updates on my research xinhuajian.wordpress.com. Checked 19 October 2026.
  2. [2310.00656] LEGO-Prover: Neural Theorem Proving with Growing Libraries arxiv.org. Checked 19 October 2026.
  3. 【BAYES COFFEE HOUSE TECH TALK SERIES】Leveraging Large Language Models for Formal Mathematical Theorem Proving: Data Synthesis and Chain-of-Thought Annotation in the DeepSeek-Prover Series blogs.ed.ac.uk. Checked 19 October 2026.
  4. [2405.14333] DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data arxiv.org. Checked 19 October 2026.
  5. Bootstrapping LLMs for theorem-proving with synthetic data bdtechtalks.substack.com. Checked 19 October 2026.
  6. [2408.08152] DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search arxiv.org. Checked 19 October 2026.
  7. [2412.19437] DeepSeek-V3 Technical Report arxiv.org. Checked 19 October 2026.
  8. [2504.21801] DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition arxiv.org. Checked 19 October 2026.
  9. [2504.19110] APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries arxiv.org. Checked 19 October 2026.
  10. [2507.23726] Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving arxiv.org. Checked 19 October 2026.
  11. [2512.17260] Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience arxiv.org. Checked 19 October 2026.