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.
- Now at
- Google DeepMind
- Works
- 8
- Citations
- 33
- h-index
- 3
Publication numbers from OpenAlex, as of 22 October 2026.
Timeline
-
2016
Bronze at the IMO
In 2016, he wins a bronze medal at the International Mathematical Olympiad.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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
- Since 2025Google DeepMindSenior research engineer
- 2021–2022ETH ZurichMaster's researcher
- 2021–2022AmazonSoftware developer intern
- 2021–2022Jump TradingQuantitative researcher intern
Education
- 2022ETH ZurichBachelor's in computer science
Most-cited works
- Olympiad-level formal mathematical reasoning with reinforcement learningWith Aja Huang, Borja Ibarz, David Silver, Demis Hassabis, Edward Hughes and Edward Lockhart
- Boosting Randomized Smoothing with Variance Reduced ClassifiersWith Martin Vechev
- Advancing mathematics research with AI-driven formal proof searchWith Adam Zsolt Wagner, Aja Huang, Edward Lockhart, Eric Wieser, Francisco J. R. Ruiz and Matej Balog
- (De-)Randomized Smoothing for Decision Stump EnsemblesWith Martin Vechev
- Robust and Accurate - Compositional Architectures for Randomized SmoothingWith Martin Vechev
Sources and credits
Photo: We have no published photo of Miklós Z. Horváth yet. Send us a free-licensed photo.
- Miklós Z. Horváth
- Miklós Z. Horváth: Selected Work
- Boosting Randomized Smoothing with Variance Reduced Classifiers
- (De-)Randomized Smoothing for Decision Stump Ensembles
- AI achieves silver-medal standard solving International Mathematical Olympiad problems
- Olympiad-level formal mathematical reasoning with reinforcement learning
- Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics
- Advancing Mathematics Research with AI-Driven Formal Proof Search

