Researcher

Miklós Z. Horváth

Miklós Z. Horváth is a senior research engineer at Google DeepMind who works on reinforcement learning and large language models and created the test-time reinforcement learning method behind AlphaProof, the first AI system to reach medal-level performance at the International Mathematical Olympiad. A bronze medallist at the 2016 Olympiad, he studied computer science at ETH Zürich, where his Master's research in the SRI Lab produced an ICLR 2022 spotlight paper and a 2022 NeurIPS paper on randomized smoothing. At DeepMind, he was a core contributor to AlphaProof, which reached silver-medal level in 2024 and which Nature described in November 2025, and to the gold-medal effort at the 2025 Olympiad. In 2026, he co-authored the Formal Conjectures benchmark of Lean-formalized problems and contributed to AlphaProof Nexus, which resolved nine open Erdős problems.

Works
8
Citations
33
h-index
3

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 2016

    Bronze at the IMO

    In 2016, he wins a bronze medal at the International Mathematical Olympiad.

  2. 2021–2022

    Randomized smoothing at ETH Zürich

    At ETH Zürich, where he earns Bachelor's and Master's degrees in computer science, he does Master's research in the SRI Lab with Mark Niklas Müller, Marc Fischer and Martin Vechev. In 2021, he and those collaborators post "Boosting Randomized Smoothing with Variance Reduced Classifiers" to arXiv, and the paper becomes an ICLR 2022 spotlight with him as first author. During his Master's, he also interns as a software developer at Amazon and as a quantitative researcher at Jump Trading.

  3. 2022

    Smoothing for decision stump ensembles

    In 2022, he is co-first author of "(De-)Randomized Smoothing for Decision Stump Ensembles" with Mark Niklas Müller, Marc Fischer and Martin Vechev, published at NeurIPS 2022. The paper proposes deterministic smoothing for decision stump ensembles, a way to certify the robustness of tree-based models.

  4. July 2024

    AlphaProof at the 2024 IMO

    In July 2024, Google DeepMind announces that AlphaProof and AlphaGeometry 2 together solve four of the six problems at the International Mathematical Olympiad, for 28 of 42 points and the level of a silver medalist. He is among the team members credited with key contributions to AlphaProof, which Thomas Hubert, Rishi Mehta and Laurent Sartran lead.

  5. 2025

    The IMO 2025 gold-medal effort

    In 2025, he is a core contributor to DeepMind's effort at the International Mathematical Olympiad, which produces end-to-end natural-language solutions at gold-medal standard under human competition conditions.

  6. November 2025

    AlphaProof published in Nature

    In November 2025, Nature publishes the AlphaProof paper "Olympiad-level formal mathematical reasoning with reinforcement learning", with him among the authors at Google DeepMind. He is a core contributor and creates its test-time reinforcement learning (TTRL) inference method, which solves three of the six IMO 2024 problems. AlphaProof is the first AI system to reach medal-level performance at the IMO.

  7. 2026

    Formal Conjectures and AlphaProof Nexus

    In May 2026, he is co-first author of Formal Conjectures, an evolving benchmark of 2615 problem statements formalized in Lean 4 that includes 1029 open research conjectures. In 2026, he also contributes to AlphaProof Nexus, an AI-driven formal proof search that resolves 9 of 353 open Erdős problems and appears in Science.

  8. As of October 2026

    Senior research engineer at DeepMind

    He is a senior research engineer at Google DeepMind, working on reinforcement learning and large language models. From 2025 to 2026, he contributes to post-training across the Gemini 3 and 4 model families, and in 2025 he contributes to SynthID-Image, image watermarking deployed at internet scale.

Career

  1. Since 2025Google DeepMindSenior research engineer
  2. 2021–2022ETH ZurichMaster's researcher
  3. 2021–2022AmazonSoftware developer intern
  4. 2021–2022Jump TradingQuantitative researcher intern

Education

  1. 2022ETH ZurichBachelor's in computer science

Most-cited works

  1. Olympiad-level formal mathematical reasoning with reinforcement learning2025 · Nature · 19 citationsWith Aja Huang, Borja Ibarz, David Silver, Demis Hassabis, Edward Hughes and Edward Lockhart
  2. Boosting Randomized Smoothing with Variance Reduced Classifiers2021 · 7 citationsWith Martin Vechev
  3. Advancing mathematics research with AI-driven formal proof search2026 · Science · 3 citationsWith Adam Zsolt Wagner, Aja Huang, Edward Lockhart, Eric Wieser, Francisco J. R. Ruiz and Matej Balog
  4. (De-)Randomized Smoothing for Decision Stump Ensembles2022 · neural information processing systems · 2 citationsWith Martin Vechev
  5. Robust and Accurate - Compositional Architectures for Randomized Smoothing2022 · 1 citationsWith Martin Vechev

Sources and credits

Photo: We have no published photo of Miklós Z. Horváth yet. Send us a free-licensed photo.

  1. Miklós Z. Horváth miklos.ai. Checked 20 October 2026.
  2. Miklós Z. Horváth: Selected Work miklos.ai. Checked 20 October 2026.
  3. Boosting Randomized Smoothing with Variance Reduced Classifiers arxiv.org. Checked 20 October 2026.
  4. (De-)Randomized Smoothing for Decision Stump Ensembles arxiv.org. Checked 20 October 2026.
  5. AI achieves silver-medal standard solving International Mathematical Olympiad problems deepmind.google. Checked 20 October 2026.
  6. Olympiad-level formal mathematical reasoning with reinforcement learning nature.com. Checked 20 October 2026.
  7. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics arxiv.org. Checked 20 October 2026.
  8. Advancing Mathematics Research with AI-Driven Formal Proof Search arxiv.org. Checked 20 October 2026.