PeopleofSuperintelligence

Builder

Marc Huisinga

Marc Huisinga is a software engineer whose Lean work spans compiler verification and developer tools for an interactive theorem prover. At KIT, he presented a bachelor's thesis on partial compiler verification in Lean 3 in 2019, tutored a Lean 4 lab in 2021, and completed a master's thesis on static uniqueness analysis in 2023. During the Lean FRO's first year, he maintained the Lean VS Code plugin and language server, while its roadmap named AI research in mathematics and verified code synthesis as goals for Lean. He later helped a Lean user troubleshoot import completion in March 2025 and added a user's InfoView example to an issue in January 2026. As of October 2026, he is a Senior Research Software Engineer on the Lean FRO team.

Timeline

  1. 2019

    A thesis on Lean compiler verification

    In 2019, he presents his KIT bachelor's thesis on partial verification of a compiler for reference-counting instructions in Lean 3. It sets out to formalize the compiler's correctness proof and supporting constructions in Lean.

  2. 2021

    Theorem Prover Lab tutor

    In summer 2021, he tutors KIT's Theorem Prover Lab. The course trains students to formalize and verify a language-technology project with Lean 4.

  3. 2023

    Static uniqueness analysis for Lean

    In 2023, he completes a master's thesis at KIT under Sebastian Ullrich on static uniqueness analysis for Lean 4. It sets out to check at compile time that values are used once, so generated code can omit matching run-time checks.

  4. August 2023–July 2024

    Lean editor and language server

    From August 2023 to July 2024, the Lean FRO appoints him official maintainer and developer of Lean's VS Code plugin and puts him at the helm of its language server. In October 2023, he invites the community to test new extension features. The roadmap describes Lean as an open-source programming language and proof assistant, and names AI research in mathematics and verified code synthesis among its goals.

  5. March 2025

    Lean import completion

    In March 2025, he helps a Lean user troubleshoot slow import completion in VS Code and points to a fix planned for the next release candidate.

  6. January 2026

    Adding an InfoView example

    In January 2026, he adds a user's example of the InfoView hiding goals and hypotheses during an incomplete tactic to the Lean 4 issue tracking the problem.

  7. As of October 2026

    Senior research software engineer

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

Career

  1. Since 2023Lean Focused Research OrganizationOfficial maintainer and developer
  2. 2021Karlsruhe Institute of TechnologyTutor

Education

  1. 2023Karlsruhe Institute of TechnologyMaster's degree
  2. 2019Karlsruhe Institute of TechnologyBachelor's degree

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.

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

  1. Marc Huisinga pp.ipd.kit.edu. Checked 21 October 2026.
  2. Formal verifiziertes Einfügen von Referenzzählungsinstruktionen (Bachelorarbeit abgeschlossen) pp.ipd.kit.edu. Checked 21 October 2026.
  3. Lean in the wild — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  4. Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie pp.ipd.kit.edu. Checked 21 October 2026.
  5. Statische Einzigartigkeitsanalyse für Lean (Masterarbeit abgeschlossen) pp.ipd.kit.edu. Checked 21 October 2026.
  6. The Lean FRO Year 1 Roadmap lean-lang.org. Checked 21 October 2026.
  7. Lean 4 extension update “Commands & Walkthrough” — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  8. Mathlib symbols not showing in VSCode for suggestions — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  9. InfoView hides goal/hypotheses when tactic incomplete — Zulip Chat Archive leanprover-community.github.io. Checked 21 October 2026.
  10. Team — Lean Lang lean-lang.org. Checked 21 October 2026.