PeopleofSuperintelligence

Researcher

Damiano Testa

Damiano Testa is a Warwick mathematician and Mathlib maintainer who works in Lean, which researchers also use to verify AI-generated output. He earned a mathematics PhD at MIT in 2005 and published research on rational curves and rational surfaces. From 2007 to 2008, he held a postdoctoral role in Bayreuth's Computational Arithmetic Geometry Group; his formalization work begins in 2020. His Mathlib work includes syntax linters and a 2025 paper on library maintenance, and he joined an AI for Math project to build an interface between Lean and Macaulay2. In 2026, he formalized a group theory result with Mathlib and co-organized an ICMS session on formalization, Lean tools, and AI-output verification; as of October 2026, he is a Warwick reader.

Works
53
Citations
368
h-index
10

Publication numbers from OpenAlex, as of 19 October 2026.

Timeline

  1. 2005

    A PhD at MIT

    He earns a mathematics PhD at MIT in 2005.

  2. 2006

    Rational curves on del Pezzo surfaces

    His 2006 paper proves that spaces of rational curves on del Pezzo surfaces are irreducible or empty, with one exception.

  3. June 2007–September 2008

    Postdoctoral work at Bayreuth

    From June 2007 to September 2008, he holds a postdoctoral position in Bayreuth's Computational Arithmetic Geometry Group.

  4. 2009–2011

    Work on rational surfaces

    In 2009, he coauthors Big rational surfaces with Anthony Várilly-Alvarado and Mauricio Velasco; it proves finite generation for Cox rings of rational surfaces with big anticanonical class. In 2011, with Antonio Laface, he studies when nef divisors on rational surfaces are semiample.

  5. Since 2020

    Formalizing mathematics

    His formalization work begins in 2020, and he serves on Mathlib's maintainer team.

  6. 2025

    Mathlib syntax tools

    With Michael Rothgang, he is one of Mathlib's main contributors to its syntax linters. In 2025, he coauthors Growing Mathlib, a paper about maintaining the expanding Lean mathematics library through deprecation tools, linters, faster compilation, and review software.

  7. 2025–2026

    Bridging proof and computation

    In 2025, he joins Matthew Ballard, Anton Leykin, and Mike Stillman on the AI for Math project Bridging proof and computation, which aims to connect Lean with Macaulay2. In 2026, he formalizes Fitting's theorem on nilpotent normal subgroups in Lean using Mathlib. He also co-organizes the Mathematics in Lean session at ICMS 2026, which covers formalization, Lean tools, and verification of AI-generated output.

  8. As of October 2026

    Reader at Warwick

    As of October 2026, he is a reader in the Department of Mathematics at the University of Warwick.

Career

  1. Since 2012University of WarwickReader
  2. 2009–2011University of Oxford
  3. 2007–2008University of BayreuthPostdoctoral researcher

Education

  1. 2005Massachusetts Institute of TechnologyPhD

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

Most-cited works

  1. Big rational surfaces2010 · Mathematische Annalen · 56 citations
  2. Descent via (3,3)-isogeny on Jacobians of genus 2 curves2014 · Acta Arithmetica · 34 citations
  3. The irreducibility of the spaces of rational curves on del Pezzo surfaces2008 · Journal of Algebraic Geometry · 33 citations
  4. Cox rings of degree one del Pezzo surfaces2009 · Algebra & Number Theory · 29 citations
  5. Gröbner bases, monomial group actions, and the Cox rings of Del Pezzo surfaces2007 · Journal of Algebra · 29 citations

From OpenAlex, as of 19 October 2026.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of Warwick. 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 2% to 32%Includes University of Warwick. We estimate where leading AI researchers worked when their most-cited papers appeared. The company share rose from 2% in 1975–1979 to 32% in 2020–2024.
  3. Stanford University trained or employed 20 of the 89 AI major-prize winners, more than any other universityIncludes University of Warwick. Stanford University trained or employed 20 of the 89 AI major-prize winners, more than any other university. We compare doctorate and employment links for major-prize and best-paper winners.
  4. The median h-index is 53 at universities and 19 at frontier AI labsIncludes University of Oxford. The median h-index is 53 at universities and 19 at frontier AI labs. We compare publishing careers, citations and moves to estimate how universities and frontier labs contribute to AI research.

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

  1. MIT affiliates win AI for Math grants to accelerate mathematical discovery oge.mit.edu. Checked 19 October 2026.
  2. The irreducibility of the spaces of rational curves on del Pezzo surfaces arxiv.org. Checked 19 October 2026.
  3. Computational Arithmetic Geometry at Bayreuth: People and Activities mathe2.uni-bayreuth.de. Checked 19 October 2026.
  4. Big rational surfaces arxiv.org. Checked 19 October 2026.
  5. Nef and semiample divisors on rational surfaces arxiv.org. Checked 19 October 2026.
  6. Mathlib maintainers leanprover-community.github.io. Checked 19 October 2026.
  7. Formalisation contributions math.uni-bonn.de. Checked 19 October 2026.
  8. Growing Mathlib: maintenance of a large scale mathematical library arxiv.org. Checked 19 October 2026.
  9. AI for Math - Bridging proof and computation matthewrobertballard.com. Checked 19 October 2026.
  10. Fitting's Theorem and Semirings of Normal Subgroups arxiv.org. Checked 19 October 2026.
  11. International Congress on Mathematical Software 2026 icms-conference.org. Checked 19 October 2026.