PeopleofSuperintelligence

Researcher

Robert Y. Lewis

Robert Y. Lewis is a computer scientist who builds tools for Lean and studies machine-generated Lean proofs. He earns master's degrees at Carnegie Mellon in 2014 and 2015, then a PhD in Pure and Applied Logic in 2018. At Brown, he works on Mathlib, a shared library of formal mathematics, and uses Lean to formalize results from number theory and functional analysis. As of October 2026, he is an associate teaching professor in Brown's Department of Computer Science.

Works
19
Citations
57
h-index
5

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. By 2015

    Teaching math and CMU degrees

    Before graduate study, he teaches high-school mathematics for two years at St. Agnes Academy in Houston. At Carnegie Mellon, he earns an MS in Logic, Computation, and Methodology in 2014 and an MS in Mathematics in 2015.

  2. 2017

    Lean and Mathematica

    His 2017 paper builds a user-extensible connection between Lean and Mathematica. It lets Lean verify some Mathematica computations while moving information between the systems.

  3. 2018

    A Pure and Applied Logic PhD

    He completes a PhD in Pure and Applied Logic at Carnegie Mellon in 2018 with a dissertation titled “Two tools for formalizing mathematical proofs.” His first postdoctoral position is in theoretical computer science at Vrije Universiteit Amsterdam.

  4. 2019

    Hensel's lemma in Lean

    In 2019, he constructs the p-adic numbers and integers in Lean and formally proves a strong form of Hensel's lemma.

  5. 2020

    Maintaining Mathlib

    As a Mathlib maintainer, he writes much of the community's 2020 paper “The Lean mathematical library.” He also coauthors “Maintaining a Library of Formal Mathematics,” which describes tools that check proofs for subtle mistakes and generate documentation for contributors.

  6. 2021

    Joining Brown CS

    He joins Brown CS as a lecturer in 2021 after three years in the Netherlands. He identifies Mathlib, an open-source library of formal mathematics written in Lean, as his main research interest.

  7. 2022

    Semilinear functional analysis

    With Frédéric Dupuis and Heather Macbeth, he implements semilinear maps in Mathlib and formalizes the Fréchet–Riesz representation theorem and the spectral theorem for compact self-adjoint operators over real and complex Hilbert spaces in 2022.

  8. As of October 2026

    Associate teaching professor

    In 2026, Lewis coauthors “Mining Machine-Generated Lean Proofs: Advice for Users, Developers, and Testers.” He is an associate teaching professor in Brown's Department of Computer Science and works on interactive theorem proving, automated reasoning, and type theory.

Career

  1. Since 2021Brown UniversityLecturer
  2. 2018–2021Vrije Universiteit AmsterdamPostdoctoral researcher
  3. St. Agnes AcademyHigh-school mathematics teacher

Education

  1. 2018Carnegie Mellon UniversityPhD in Pure and Applied Logic
  2. 2015Carnegie Mellon UniversityMS in Mathematics
  3. 2014Carnegie Mellon UniversityMS in Logic, Computation, and Methodology

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

Most-cited works

  1. An Extensible Ad Hoc Interface between Lean and Mathematica2017 · Electronic Proceedings in Theoretical Computer Science · 10 citations
  2. Formalizing the solution to the cap set problem2019 · 10 citations
  3. A Heuristic Prover for Real Inequalities2016 · Journal of Automated Reasoning · 9 citations
  4. A formal proof of Hensel's lemma over the p-adic integers2019 · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) · 8 citations
  5. Formalizing the ring of Witt vectors2021 · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) · 7 citations

From OpenAlex, as of 21 October 2026.

  1. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes Brown University. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  2. 84% of people shaping AI with recorded undergraduate and doctoral schools changed institutions for their doctorateIncludes Brown University. 84% of people shaping AI with recorded undergraduate and doctoral schools changed institutions for their doctorate. Across 2,116 people with both an undergraduate degree and a doctorate recorded, we trace which undergraduate schools feed which doctoral programs, how often students stay at the same school, and how paths differ by birth-country region.
  3. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes Brown University. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  4. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Brown University. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.

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 Robert Y. Lewis yet. Send us a free-licensed photo.

  1. Robert Y. Lewis Joins Brown CS As Lecturer cs.brown.edu. Checked 20 October 2026.
  2. Home - Robert Y. Lewis robertylewis.com. Checked 20 October 2026.
  3. An Extensible Ad Hoc Interface between Lean and Mathematica arxiv.org. Checked 20 October 2026.
  4. Pure and Applied Logic logic.cmu.edu. Checked 20 October 2026.
  5. A Formal Proof of Hensel's Lemma over the p-adic Integers arxiv.org. Checked 20 October 2026.
  6. Maintaining a Library of Formal Mathematics arxiv.org. Checked 20 October 2026.
  7. Publications - Robert Y. Lewis robertylewis.com. Checked 20 October 2026.
  8. Formalized Functional Analysis with Semilinear Maps arxiv.org. Checked 20 October 2026.
  9. AITP'26: 11th Conference on Artificial Intelligence and Theorem Proving aitp-conference.org. Checked 20 October 2026.