PeopleofSuperintelligence

Researcher

Joachim Breitner

Also known as nomeata

Joachim Breitner is a Principal Research Software Engineer at the Lean FRO, where he helps build Lean, a dependently typed programming language and theorem prover in which mathematicians formalize mathematics. His 2016 doctorate at the Karlsruhe Institute of Technology implemented the Call Arity transformation in the Haskell compiler GHC and proved in Isabelle that it does not degrade program performance. As a postdoc at the University of Pennsylvania, he coauthored the 2017 paper presenting hs-to-coq, which translates Haskell programs into Coq for verification; at the DFINITY Foundation, he built the backend of the Motoko language before leaving in 2021. After joining the Lean FRO in November 2023, he created the Mathlib search engine Loogle and worked on recursive definitions and functional induction in Lean. In December 2025, he was one of 34 authors, with Terence Tao, of the Equational Theories Project paper, a machine-assisted collaboration that settled more than 22 million implications between equational laws using human-generated and automated proofs checked in Lean.

Born
1985

Years link to their sources.

Timeline

  1. 2010–2016

    Call Arity and a KIT doctorate

    He completes a diploma thesis at the Karlsruhe Institute of Technology in 2010. In 2014, he coauthors "Safe Zero-cost Coercions for Haskell" at ICFP with Richard Eisenberg, Simon Peyton Jones and Stephanie Weirich, and his Call Arity paper wins a best student paper award at Trends in Functional Programming. His 2016 doctoral thesis at KIT's Institute for Program Structures and Data Organization, supervised by Gregor Snelting, implements Call Arity in GHC and proves in Isabelle that it does not degrade program performance.

  2. 2016–2017

    Postdoc at UPenn

    In 2016, he moves to Philadelphia to work as a postdoc at the University of Pennsylvania. With Antal Spector-Zabusky, Christine Rizkallah and Stephanie Weirich, he presents hs-to-coq in 2017, a tool that translates total Haskell programs into the Coq proof assistant so that their properties can be mechanically verified.

  3. 2016–2024

    GHC Steering Committee secretary

    He answers the 2016 call for nominations to the new GHC Steering Committee, joins its first members and, in February 2017, takes on the role of secretary for the GHC proposal process. In January 2024, he announces his resignation after seven years as member and secretary.

  4. June 2021

    Motoko at DFINITY

    At the DFINITY Foundation, he builds the backend of the Motoko programming language, helps with the formalism of the Candid interoperability layer and verifies its soundness criterion in Coq. He leaves in June 2021 after almost three years, once he has seen the launch of the Internet Computer through.

  5. November 2023

    Joining the Lean FRO

    He joins the Lean FRO, a Focused Research Organization, in November 2023 to work on Lean, a dependently typed programming language and theorem prover whose community formalizes mathematics in the Mathlib library. While getting up to speed, he creates Loogle, a Mathlib search engine inspired by Haskell's Hoogle.

  6. 2024

    Recursion and functional induction

    He works on recursive definitions and functional induction in Lean and explains both on the official Lean blog: termination of recursive functions in January 2024, and the functional induction principle of the Lean 4.8 release in May 2024.

  7. December 2025

    The Equational Theories Project

    In December 2025, he is one of 34 authors, with Terence Tao, of the Equational Theories Project paper. The online project explores collaboration in mathematics with machine assistance and determines all 22,028,942 implications between the 4,694 simplest equational laws on magmas, using human-generated and automated proofs validated by Lean.

  8. As of October 2026

    Principal engineer at the Lean FRO

    He is a Principal Research Software Engineer at the Lean FRO. In February 2026, after a colleague builds a debugger for a small Lean-embedded language in one day with GPT-Codex 5.3, he writes that Lean is a particularly well-suited platform for AI coding agents.

Career

  1. Since 2023Lean Focused Research OrganizationPrincipal Research Software Engineer
  2. Until 2021DFINITY Foundation
  3. 2016–2017University of PennsylvaniaPostdoc
  4. 2016–2024GHC Steering CommitteeMember, Secretary

Education

  1. 2016Karlsruhe Institute of TechnologyPhD
  2. 2010Karlsruhe Institute of TechnologyDiploma

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. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes University of Pennsylvania. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  3. People shaping AI work at a median of 3 organizations over a career: 3 for university starters and institute and lab starters, versus 2 for company startersIncludes University of Pennsylvania. Across 6,853 people shaping AI with a dated work role, we estimate a median of 3 parent organizations over a career (mean 3.6), comparing role groups, starting sectors and starting decades from the 1950s to 2020–2026.
  4. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of Pennsylvania. 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.

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 Joachim Breitner yet. Send us a free-licensed photo.

  1. Publications – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  2. Lazy Evaluation: From natural semantics to a machine-checked compiler transformation (KITopen) publikationen.bibliothek.kit.edu. Checked 20 October 2026.
  3. Eine Woche Philadelphia – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  4. [1711.09286] Total Haskell is Reasonable Coq arxiv.org. Checked 20 October 2026.
  5. GHC Steering Committee Retrospective – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  6. Leaving DFINITY – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  7. Joining the Lean FRO – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  8. Blogging on Lean – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  9. Recursive definitions in Lean — Lean lean-lang.org. Checked 20 October 2026.
  10. Functional induction — Lean lean-lang.org. Checked 20 October 2026.
  11. [2512.07087] The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale arxiv.org. Checked 20 October 2026.
  12. Team — Lean Lang lean-lang.org. Checked 20 October 2026.
  13. Joachim Breitner – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.
  14. Vibe-coding a debugger for a DSL – Blog – Joachim Breitner's Homepage joachim-breitner.de. Checked 20 October 2026.