I am a postdoc in the department of Theoretical Computer Science at the Vrije Universiteit Amsterdam, working with Jasmin Blanchette on the Matryoshka project.

I recently finished my PhD in Pure and Applied Logic at Carnegie Mellon University, under the supervision of Jeremy Avigad. Here is my dissertation. 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 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 download a copy of my CV here.

My office at the VU is W&N S-414. You may reach me by email at r.y.lewis@vu.nl.

I recently finished my PhD in Pure and Applied Logic at Carnegie Mellon University, under the supervision of Jeremy Avigad. Here is my dissertation. 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 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 download a copy of my CV here.

My office at the VU is W&N S-414. You may reach me by email at r.y.lewis@vu.nl.

### Recent news:

My paper *A formal proof of Hensel's lemma over the p-adic integers* was accepted at CPP 2019.

I am organizing Lean Together, a meeting for mathematically-oriented Lean users, in January 2019.

I am organizing a session at ICMS 2018 on formal and informal mathematical corpora in July 2018.

I am giving an invited talk at Hales60, a conference in honor of Tom Hales' 60th birthday, in June 2018.