Lean Together 2021 — Patrick Massot and I are organizing the third annual Lean users meeting: Lean Together 2021! The event will take place virtually January 4-7. We will have a variety of talks about formalizations, tools and infrastructure, and teaching with proof assistants.... Read more—
Hi, I'm Robert Y. Lewis. I'm a postdoc in the department of Theoretical Computer Science at the Vrije Universiteit Amsterdam, working with Jasmin Blanchette on the Matryoshka project.
I completed my PhD in Pure and Applied Logic at Carnegie Mellon University, under the supervision of Jeremy Avigad. I earned an MS in Logic, Computation, and Methodology in 2014 and an MS in Mathematics in 2015, both from CMU. Previously, I earned a BA from Rice University with a double major in Mathematics and Philosophy, and taught geometry, pre-calculus, and AP calculus at St. Agnes Academy in Houston.
My interests revolve around formal methods, logic, and the foundations of mathematics. I work on interactive theorem proving, formal verification, automated logical reasoning, and type theoretic foundations for mathematics. More details are available on my Research page.
News and Updates
Formalizing the Ring of Witt Vectors — Johan Commelin and I have released a preprint of our new paper, Formalizing the Ring of Witt Vectors! (Update, Nov 25: the paper has been accepted at CPP ‘21.) We describe the construction of the p-typical Witt vectors and their... Read more—
Metaprogramming in Lean tutorial — Johan Commelin and Patrick Massot are organizing the workshop Lean for the Curious Mathematician, taking place virtually July 13-17, 2020. The workshop aims to give working mathematicians a hands-on introduction to formal proof. As part of the “intermediate track” of... Read more—
Logic and Modeling course information — In Spring 2020, I taught the course Logic and Modeling at the VU. The course was held entirely online due to the COVID-19 pandemic. I have collected the course information, lecture recordings, and assignments here. (While the archive does not... Read more—
The Lean mathematical library — Along with a number of other contributors, I have written a paper about the Lean mathematical library. The paper describes a large-scale, open project to which 68 people (and counting) have contributed. Rather than attribute the paper to some subset... Read more—
Formalizing the solution to the cap set problem — Sander Dahmen, Johannes Hölzl, and I have formalized Ellenberg and Gijswijt’s solution to the cap set problem in Lean. Our paper about this project will appear at ITP 2019. Here are some slides from a talk I gave about this... Read more—
Lean Together 2019 — From the 7th to the 11th of January, 2019, we hosted a workshop Lean Together in Amsterdam. This workshop was meant to serve a few purposes. First, it was a meeting for Lean developers and users who have been working... Read more—
A formal proof of Hensel's lemma over the p-adic integers — Here you will find the supplementary materials to my paper A formal proof of Hensel’s lemma over the p-adic integers. This paper was published at CPP 2019. For more information, contact Robert Y. Lewis. The Formal Development The project described... Read more—
A bi-directional extensible interface between Lean and Mathematica — Minchao Wu and I have been working on a project that connects the computer algebra system Mathematica to the Lean theorem prover. Here you will find the supplementary materials corresponding to our paper draft. An early version of this work... Read more—
The Nature of Mathematical Reasoning — In 2015 I tought a course at Carnegie Mellon titled The Nature of Mathematical Reasoning. This course, aimed at non-mathematicians, took a philosophical look at the historical and modern practice of mathematics. The course materials can be found here. I... Read more—