PeopleofSuperintelligence

Researcher

Julia Markus Himmel

Also known as Markus Himmel, TwoFX

Julia Markus Himmel is a software developer with a background in mathematics who uses Lean to formalize mathematics and verify programs. In 2020, she completed a bachelor's thesis at KIT that extended mathlib with abelian categories and gave the first formally verified proof of the snake lemma. She helped add the Freyd-Mitchell and Gabriel-Popescu theorems to mathlib and started human-eval-lean, a project for Lean solutions to the HumanEval AI benchmark with machine-checked proofs. As of October 2026, she is a Senior Tech Lead at the Lean FRO, a mathlib maintainer and a developer of Lean's standard library.

Timeline

  1. 2020

    Diagram chasing at KIT

    In April 2020, she completes a bachelor's thesis at KIT's Programming Paradigms Group (IPD Snelting), supervised by Sebastian Ullrich. The thesis extends Lean's mathematical library with abelian categories and pseudoelements, adds an interactive tactic for proving exactness statements by diagram chasing, and gives the first formally verified proof of the snake lemma.

  2. 2022–February 2025

    The Freyd-Mitchell theorem

    In January 2022, she maps out the work needed to prove the Freyd-Mitchell embedding theorem in mathlib; Jakob von Raumer joins the project, and Paul Reichert joins in February 2024. At ICMS in July 2024, she presents the project and says it is carried out entirely through pull requests to mathlib. The theorem enters mathlib in February 2025.

  3. September 2024

    Teaching Lean at TU Wien

    In September 2024, she teaches a Lean tutorial for mathematicians at TU Wien in Vienna as a Lean FRO tutor, covering Lean, sets and functions, Mathlib, and metaprogramming.

  4. March 2025–June 2025

    Gabriel-Popescu in mathlib

    Following a proof by Barry Mitchell in 1981, she adds the Gabriel-Popescu theorem to mathlib in March 2025. In June 2025, she and Joël Riou describe the new abelian-category results in a post on the Lean community blog.

  5. 2025

    HumanEval solutions in Lean

    In 2025, she starts human-eval-lean, a collection of hand-written Lean solutions to the HumanEval AI programming benchmark with machine-checked proofs of correctness. In June 2025, she describes a solution to task 24 that finds the largest proper divisor of an integer in time proportional to its square root.

  6. September 2025

    Lean standard-library tooling

    At the EuroProofNet Workshop on Proof Libraries in September 2025, she presents Lean's standard-library development methods and tooling. Her talk describes a Lean FRO tool that detects and tracks library defects through the GitHub pull-request workflow.

  7. January 2026

    Lean Together 2026

    She co-organizes the virtual Lean Together meeting held in January 2026. With Sofia Rodrigues, she presents standard-library features added in 2025 for building production-ready software in Lean.

  8. As of October 2026

    Senior tech lead at Lean FRO

    She is a Senior Tech Lead at the Lean FRO and a mathlib maintainer. She has a master's in pure mathematics in Cambridge, has formalized mathematics since 2020, and works as a software developer with a mathematics background. She continues work on Lean's standard library toward production-ready formally verified software. In July 2026, she writes about dot-notation-respects-open and a Lean 4.33 linter for ambiguous namespaces.

Career

  1. NowLean Focused Research OrganizationSenior Tech Lead

Education

  1. 2020Karlsruhe Institute of TechnologyBachelor's thesis
  2. University of CambridgeMaster's in pure mathematics

From the biography.

  1. Google has the highest combined h-index among AI organizationsIncludes Convergent Research. We estimate that Google holds the highest combined h-index at 8,016, while universities account for 73% of the deduplicated total across AI organizations.
  2. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of Cambridge. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  3. The median h-index is 48 at universities and 14 at frontier AI labsIncludes University of Cambridge. The median h-index is 48 at universities and 14 at frontier AI labs. We compare publishing careers, recent citations, dual appointments and job moves across 2,420 university researchers and 308 frontier-lab researchers.
  4. Companies supply the most prior-work hires at 7 of the 9 frontier AI labsIncludes University of Cambridge. Our estimates of the organizations where 550 people worked directly before joining 9 frontier AI labs across 620 career transitions, comparing the main feeder organizations per lab.

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 Julia Markus Himmel yet. Send us a free-licensed photo.

  1. Diagrammjagd in einem interaktiven Theorembeweiser (Bachelorarbeit abgeschlossen) pp.ipd.kit.edu. Checked 21 October 2026.
  2. Sonstiges: Diagram Chasing in Interactive Theorem Proving pp.ipd.kit.edu. Checked 21 October 2026.
  3. Theorems about abelian categories | Lean community blog leanprover-community.github.io. Checked 21 October 2026.
  4. ICMS 2024 - Session 2: Novel Formalisations of Mathematics in Lean icms-conference.org. Checked 21 October 2026.
  5. Lean Tutorial, September 18-20, 2024, TU Wien dmg.tuwien.ac.at. Checked 21 October 2026.
  6. The largest divisor - Julia Markus Himmel juliahimmel.de. Checked 21 October 2026.
  7. EuroProofNet Workshop on Proof Libraries europroofnet.github.io. Checked 21 October 2026.
  8. Lean Together 2026 leanprover-community.github.io. Checked 21 October 2026.
  9. What's new in the Lean standard library (Lean Together 2026) researchseminars.org. Checked 21 October 2026.
  10. Team — Lean Lang lean-lang.org. Checked 21 October 2026.
  11. Mathlib maintainers leanprover-community.github.io. Checked 21 October 2026.
  12. Now - Julia Markus Himmel juliahimmel.de. Checked 21 October 2026.
  13. An underappreciated Lean feature - Julia Markus Himmel juliahimmel.de. Checked 21 October 2026.
  14. Julia Markus Himmel juliahimmel.de. Checked 21 October 2026.