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.

You can reach me by email at r.y.lewis@vu.nl, and you can find my cv here.

News and Updates

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

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