PeopleofSuperintelligence

Builder

Joscha Mennicken

Joscha Mennicken builds software for Lean, with work on language-server references, theorem-prover tooling, performance benchmarks and LLM-assisted proofs. In 2022, he completed a bachelor's thesis at Karlsruhe Institute of Technology on project-wide references in Lean 4. In September 2023, he explained how to benchmark untracked Mathlib commits with Speedcenter. In July 2025, he helped diagnose an LLM-proof encoding issue and improved the Lean Language Reference's print layout; in November 2025, he added Mathlib4 to Radar and imported its benchmark history. As of October 2026, he is a Research Software Engineer on Lean FRO's team.

Links
GitHub

Timeline

  1. November 2021

    Questions on Lean 4 proofs

    In November 2021, he asks how Lean 4's `have` and `let` constructs work with propositions. After a reply, he describes `have` as a way to explicitly throw away unnecessary information.

  2. April 2022

    Lean 4 language server

    In April 2022, he completes a bachelor's thesis at Karlsruhe Institute of Technology on locating project-wide references in Lean 4 and integrating them into Lean's Language Server Protocol implementation.

  3. September 2023

    Mathlib performance measurements

    In September 2023, he explains that two untracked Mathlib commits must be added to Speedcenter’s queue before it can compare their performance.

  4. July 2025

    Troubleshooting an AI proof file

    In July 2025, he traces garbled Lean code in an LLM-assisted proof experiment to Zulip's missing encoding signal to the browser. He says the proof file is correctly UTF-8 encoded.

  5. July 2025

    Printing the Lean reference

    In July 2025, he opens a pull request with CSS experiments for printing the Lean Language Reference. The generated PDF looks nicer after his tweaks.

  6. November–December 2025

    Mathlib benchmarks in Radar

    In November 2025, he adds Mathlib4 to Radar, which benchmarks new commits for comparison, and imports the older VelCom benchmark data. In December 2025, he turns off Speedcenter and makes Radar wait until a PR’s `awaiting-CI` label is removed before running a benchmark.

  7. As of October 2026

    Research software engineer

    As of October 2026, he is a Research Software Engineer on Lean FRO's team.

Career

  1. NowLean Focused Research OrganizationResearch Software Engineer

Education

  1. 2022Karlsruhe Institute of TechnologyBachelor's thesis

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 Karlsruhe Institute of Technology. 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 company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Karlsruhe Institute of Technology. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.
  4. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes Karlsruhe Institute of Technology. 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.

Sources and credits

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

  1. Zulip Chat Archive: have and let leanprover-community.github.io. Checked 21 October 2026.
  2. Other Publications: Locating and presenting lexical references in a theorem prover pp.ipd.kit.edu. Checked 21 October 2026.
  3. Lokalisierung & Darstellung von lexikalischen Referenzen in einem Theorembeweiser (Bachelorarbeit abgeschlossen) i44vm2.informatik.kit.edu. Checked 21 October 2026.
  4. More compact DiscrTree — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  5. MCP Tools for LLMs and Agentic Mathematics — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  6. Printable form of language reference? — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  7. mathlib4 speedcenter — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  8. Team — Lean Lang lean-lang.org. Checked 21 October 2026.