PeopleofSuperintelligence

Researcher

Paul Reichert

Also known as datokrat

Paul Reichert is a Research Software Engineer whose work extends Lean and mathlib for formal mathematics. In 2022, he worked to formalize a chapter of convex geometry in Lean while writing a master's thesis; he later published mathematical notes and a software-security essay, and helped add the Freyd-Mitchell and Gabriel-Popescu theorems to mathlib. His later Lean work included an iterator library and a simp-set tactic labeled LLM-generated. As of October 2026, he is a Research Software Engineer on the Lean FRO team.

Timeline

  1. 2022

    A thesis in convex geometry

    In August 2022, he writes a master's thesis in convex geometry in Karlsruhe, Germany, while trying to formalize a chapter on Brunn-Minkowski theory in Lean. He plans to contribute some of the missing Brunn-Minkowski results to mathlib.

  2. August 2023

    Mathematics on paulr.de

    On paulr.de, he publishes English notes about mathematical problems he enjoyed. His August 2023 posts include "Linearly independent subsets," "Three palindromes," and "Necklaces and triangulations of quadrilaterals."

  3. December 2023

    Read-only Turing machines

    In December 2023, he publishes "Read-only Turing machines," a mathematics note on his site.

  4. February 2024–2025

    The abelian categories project

    In February 2024, he joins Julia Markus Himmel and Jakob von Raumer on the mathlib project about abelian categories; its first part spans more than 100 pull requests. In 2025, the team completes the project with the Freyd-Mitchell and Gabriel-Popescu theorems in mathlib; the Freyd-Mitchell embedding theorem enters mathlib in February 2025.

  5. April 2024

    An essay on software security

    In April 2024, he publishes "Thoughts on software security," noting how much code and how many authors people trust every day.

  6. September 2025–December 2025

    Lean's iterator library

    In his GitHub repository, he works on a Lean iterator library intended for the standard library. In September 2025, he says polymorphic ranges need many type classes and plans a manual for iterators and ranges. In October 2025, he proposes total extrinsic termination proofs so `it.toList` can be used before an iterator's finiteness is proved. After a contributor proposes `scan` in December 2025, he says it needs `Finite` and `Productive` instances and lemmas like those for `drop` before it can enter the standard library.

  7. March 2026

    An LLM-generated Lean tactic

    By March 2026, his datokrat GitHub gists include a Lean tactic named `minimize_simps`, described as an LLM-generated simp-set minimizer.

  8. As of October 2026

    Research Software Engineer at Lean FRO

    As of October 2026, he is a Research Software Engineer on the Lean FRO team. Leo de Moura is Chief Architect and Co-Founder; Sebastian Ullrich is Head of Engineering and Co-Founder.

  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. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI each year from 1955 to 2025, tracing the shift from university labs to companies.
  3. The United States employs an estimated 48% of people shaping AIWe estimate where the people shaping AI work today, how universities, companies and research institutes split across countries, and how country shares have changed since the 1960s.
  4. 43% of living people shaping AI work outside their country of birthWe estimate that 43% of living people shaping AI work outside their country of birth (520 of 1,198 people with known birth and employment countries).

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

  1. Topic: Hello! - Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  2. Paul Reichert paulr.de. Checked 21 October 2026.
  3. Theorems about abelian categories | Lean community blog leanprover-community.github.io. Checked 21 October 2026.
  4. Freyd-Mitchell and Gabriel-Popescu - Julia Markus Himmel juliahimmel.de. Checked 21 October 2026.
  5. Thoughts on software security paulr.de. Checked 21 October 2026.
  6. datokrat (Paul Reichert) · GitHub github.com. Checked 21 October 2026.
  7. Topic: Iterating ranges with PRange - Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  8. Topic: Extrinsic finiteness proofs for iterators - Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  9. Topic: scan combinator for iterators - Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  10. datokrat’s gists · GitHub gist.github.com. Checked 21 October 2026.
  11. Team — Lean Lang lean-lang.org. Checked 21 October 2026.