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—
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
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 ad hoc 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 earlier 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—