PeopleofSuperintelligence

Researcher

Mirek Olšák

Also known as Miroslav Olšák

Mirek Olšák is a mathematician at Google DeepMind who moved from the study of Maltsev conditions to machine learning for theorem proving and olympiad geometry. He posted Loop conditions on arXiv in 2017 and coauthored a graph-based encoding of formulas for theorem provers with Cezary Kaliszyk and Josef Urban in 2020. By 2023 he was a postdoctoral mathematician at IHES, and in 2024 he coauthored Graph2Tac, a graph neural network for the Coq proof assistant. In July 2024, Google DeepMind credited him with key contributions to AlphaGeometry 2, which joined AlphaProof in solving four of six problems at the 2024 International Mathematical Olympiad at silver-medalist level. The AlphaGeometry2 paper he coauthored in 2025 reports an 84% solving rate on 25 years of geometry problems, and in June 2026 he coauthored LEAP, an agentic Lean prover that solves all 12 problems of the 2025 Putnam Competition.

Works
45
Citations
337
h-index
8
Badges

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 2017

    Loop conditions in algebra

    In 2017, he posts Loop conditions on arXiv, a study of Maltsev conditions that consist of one linear equation. He classifies the conditions given by undirected graphs and shows that the Siggers term is the weakest non-trivial loop condition.

  2. 2020

    Embeddings for automated reasoning

    In 2020, he coauthors Property Invariant Embedding for Automated Reasoning with Cezary Kaliszyk and Josef Urban for the 24th European Conference on Artificial Intelligence. The paper encodes formulas as graphs for neural networks, with symbols represented only by nodes, and shows gains over the best earlier characterizations in a tableaux connection prover.

  3. 2022–2023

    Postdoc at IHES

    In 2022, he appears on the ITP programme of the Federated Logic Conference with an affiliation at the Institut des Hautes Études Scientifiques (IHES). In 2023, he is one of the postdoctoral mathematicians at IHES who speak to visiting middle-school students, and he explains how computers can solve problems.

  4. January 2024

    Graph2Tac for Coq

    In January 2024, he coauthors Graph2Tac with Lasse Blaauwbroek, Jason Rute, Vasily Pestun and others. The graph neural network builds hierarchical representations of new definitions for the Tactician platform of the Coq proof assistant, and its online definition task solves 1.5 times as many theorems as an offline baseline.

  5. July 2024

    AlphaGeometry 2 at the IMO

    In July 2024, Google DeepMind announces that AlphaProof and AlphaGeometry 2 together solve four of the six problems at the 2024 International Mathematical Olympiad, at silver-medalist level. Trieu Trinh and Yuri Chervonyi lead the development of AlphaGeometry 2, and he makes key contributions.

  6. September 2024

    Olympiad talk at AITP 2024

    In September 2024, he gives the 55-minute talk "Math Olympiad – to the geometry and beyond" at the 9th Conference on Artificial Intelligence and Theorem Proving in Aussois, France. He attends from the University of Cambridge.

  7. 2025

    Gold-medalist geometry with AlphaGeometry2

    In 2025, he is third author of the AlphaGeometry2 paper, with affiliations at Google DeepMind and the University of Cambridge. The system surpasses an average gold medalist in olympiad geometry, and its solving rate on geometry problems from the last 25 years rises to 84%, from 54% for the original AlphaGeometry.

  8. June 2026

    LEAP, a Lean proving framework

    In June 2026, he and colleagues at Google DeepMind and Google Cloud AI Research post LEAP, an agentic framework that lets general-purpose foundation models prove theorems in Lean. LEAP solves all 12 problems of the 2025 Putnam Competition and lifts the one-shot formal solve rate on the new Lean-IMO-Bench from below 10% to 70%.

Career

  1. NowGoogle DeepMindMathematician
  2. 2023–2025University of Cambridge
  3. 2022–2023Institute of Advanced Scientific StudiesPostdoctoral mathematician
  4. 2022–2024Université Paris-Saclay
  5. 2019–2023Universität Innsbruck
  6. 2017–2023Charles University

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

Most-cited works

  1. Reinforcement Learning of Theorem Proving2018 · 41 citationsWith Josef Urban
  2. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)2020 · Lecture notes in computer science · 37 citationsWith Josef Urban
  3. Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures2019 · Journal of Mathematical Logic · 26 citations
  4. Property Invariant Embedding for Automated Reasoning2020 · Frontiers in artificial intelligence and applications · 23 citationsWith Josef Urban
  5. Dichotomy for Symmetric Boolean PCSPs2019 · 18 citations

From OpenAlex, as of 21 October 2026.

  1. The median h-index is 48 at universities and 14 at frontier AI labsIncludes Mirek Olšák. The median h-index is 48 at universities and 14 at frontier AI labs. We compare publishing careers, recent citations, dual appointments and job moves across 2,420 university researchers and 308 frontier-lab researchers.
  2. 16% of AI career moves in the 2020s went from a university to a companyIncludes Mirek Olšák. We estimate that 16% of AI career moves in the 2020s went from a university to a company; 29% of moves starting at a university went to a company, and 76% ended the university role.
  3. Google had the most people shaping AI every year from 2014 to 2025Includes Google. Our estimates of which organizations employed the most people shaping AI each year from 1955 to 2025, tracing the shift from university labs to companies.
  4. Google has the highest combined h-index among AI organizationsIncludes Google. 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.

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 Mirek Olšák yet. Send us a free-licensed photo.

  1. [1701.00260] Loop conditions arxiv.org. Checked 20 October 2026.
  2. Property Invariant Embedding for Automated Reasoning - Computational Logic cl-informatik.uibk.ac.at. Checked 20 October 2026.
  3. Miroslav Olšák - FLoC 2022: Federated Logic Conference 2022 easychair.org. Checked 20 October 2026.
  4. Middle school students at IHES - IHES ihes.fr. Checked 20 October 2026.
  5. [2401.02949] Graph2Tac: Online Representation Learning of Formal Math Concepts arxiv.org. Checked 20 October 2026.
  6. AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind deepmind.google. Checked 20 October 2026.
  7. AITP'24: 9th Conference on Artificial Intelligence and Theorem Proving aitp-conference.org. Checked 20 October 2026.
  8. [2502.03544] Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2 arxiv.org. Checked 20 October 2026.
  9. Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2 arxiv.org. Checked 20 October 2026.
  10. [2606.03303] LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks arxiv.org. Checked 20 October 2026.
  11. LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks arxiv.org. Checked 20 October 2026.