PeopleofSuperintelligence

Researcher

Andrej Bauer

Andrej Bauer is a mathematician and computer scientist whose work connects computation, formal mathematics, and AI tools for mathematical research. He earned a doctorate from Carnegie Mellon in 2000, visited the Institute for Advanced Study in 2012, and helped write a book on homotopy type theory in 2013. His work includes the Coq-based HoTT Library and an article on constructive mathematics that earned him the 2022 AMS Conant Prize. As of October 2026, he is a professor at the University of Ljubljana and principal investigator of BRIDGE, which connects AI, proof assistants, and mathematical data. In July 2026, he and an AI assistant built Bridge MCP for querying mathematical objects.

Now at
University of Ljubljana and Institute of Mathematics, Physics, and Mechanics
Works
93
Citations
847
h-index
15
Badges

Publication numbers from OpenAlex, as of 18 October 2026.

Timeline

  1. 2000

    Logic at Carnegie Mellon

    In 2000, he earns a PhD in pure and applied logic from Carnegie Mellon's School of Computer Science.

  2. September–December 2012

    A visiting IAS role

    From September to December 2012, he is a visiting member at the Institute for Advanced Study's School of Mathematics. His interests include logic, computation, category theory, type theory, and constructive mathematics.

  3. 2013–2016

    Formalizing homotopy type theory

    In 2013, he joins the collaborative effort behind a book on homotopy type theory. In 2016, he and five coauthors describe the HoTT Library, a Coq formalization of homotopy type theory.

  4. By 2019

    Professor at Ljubljana

    By 2019, he is a professor of computational mathematics at the University of Ljubljana and works on computer tools that assist mathematicians with formally verified mathematics.

  5. 2022

    A Conant Prize

    In 2022, he receives the American Mathematical Society's Levi L. Conant Prize for his article “Five stages of accepting constructive mathematics.”

  6. 2025

    Funding for BRIDGE

    In 2025, Renaissance Philanthropy selects BRIDGE for funding through its AI for Math Fund, with Bauer on its team. The project links AI, proof assistants, and mathematical data, and its team develops large datasets, formalized-theorem dependency graphs, and recommendation systems.

  7. As of October 2026

    Professor and BRIDGE lead

    As of October 2026, he is principal investigator of BRIDGE, head of theoretical computer science at IMFM, and professor of computational mathematics at the University of Ljubljana. In July 2026, he and an AI assistant build Bridge MCP, a tool with a database of mathematical objects and a mathematical query language.

Career

  1. Since 2007Institute of Mathematics, Physics, and MechanicsHead of Theoretical Computer Science
  2. Since 2006University of LjubljanaProfessor of Computational Mathematics
  3. 2012Institute for Advanced StudyVisiting Member

Education

  1. 2000Carnegie Mellon UniversityPhD

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. Equilogical spaces2003 · Theoretical Computer Science · 85 citations
  2. The realizability approach to computable analysis and topology2000 · 84 citations
  3. The HoTT library: a formalization of homotopy type theory in Coq2016 · 57 citations
  4. An Effect System for Algebraic Effects and Handlers2014 · Logical Methods in Computer Science · 55 citations
  5. Five stages of accepting constructive mathematics2016 · Bulletin of the American Mathematical Society · 53 citations

From OpenAlex, as of 18 October 2026.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of Ljubljana. Our estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.
  2. The company share of AI researchers’ top papers rose from 3% to 32%Includes University of Ljubljana. We estimate where leading AI researchers worked when their most-cited papers appeared. The company share rose from 3% in 1975–1979 to 32% in 2020–2024.
  3. Google has the highest combined h-index among AI organizationsIncludes Carnegie Mellon University. Our estimates of combined and median h-index at AI organizations, using current affiliations and OpenAlex records.
  4. The median h-index is 54 at universities and 20 at frontier AI labsIncludes Carnegie Mellon University. The median h-index is 54 at universities and 20 at frontier AI labs. We compare publishing careers, citations and moves to estimate how universities and frontier labs contribute to AI research.

Colleagues

People with dated positions at the same organization in the same years.

Sources and credits

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

  1. FPSAC 2019 – Invited speakers fpsac2019.fmf.uni-lj.si. Checked 18 October 2026.
  2. The HoTT book math.andrej.com. Checked 18 October 2026.
  3. The HoTT Library: A formalization of homotopy type theory in Coq arxiv.org. Checked 18 October 2026.
  4. Prof. Andrej Bauer receives prestigious prize of the American Mathematical Society dmfa.si. Checked 18 October 2026.
  5. Naši matematiki med prejemniki prestižnih sredstev za projekt BRIDGE fmf.uni-lj.si. Checked 18 October 2026.
  6. Team bridge.imfm.si. Checked 18 October 2026.
  7. Making AI smarter with AI math.andrej.com. Checked 18 October 2026.