Publications

My CV is often more up-to-date than this page.

Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth.
Formalized Functional Analysis with Semilinear Maps. ITP, 2022.
Robert Y. Lewis and Minchao Wu.
A bi-directional extensible ad hoc interface between Lean and Mathematica. Journal of Automated Reasoning, 2022.
Johan Commelin and Robert Y. Lewis.
Formalizing the Ring of Witt Vectors. CPP, 2021. (Distinguished Paper Award)
Robert Y. Lewis and Paul-Nicolas Madelaine.
Simplifying casts and coercions. PAAR, 2020.
Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis.
Maintaining a library of formal mathematics. CICM, 2020.
The mathlib Community.
The Lean mathematical library. CPP, 2020.
This paper describes a collective project with many contributors. I am a maintainer of the project and wrote much of this paper.
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the solution to the cap set problem. ITP, 2019.
Robert Y. Lewis.
A formal proof of Hensel’s lemma over the p-adic integers. CPP, 2019.
Robert Y. Lewis.
An extensible ad hoc interface between Lean and Mathematica. PxTP, 2017.
Jeremy Avigad, Robert Y. Lewis, and Cody Roux.
A heuristic prover for real inequalities (journal version). Journal of Automated Reasoning, 2016.
Jeremy Avigad, Robert Y. Lewis, and Cody Roux.
A heuristic prover for real inequalities. ITP, 2014.
Leobardo Rosales, Robert Y. Lewis, et al.
Energy minimizing unit vector fields. Involve, 2010.

Robert Y. Lewis and Heather Macbeth.
Classification of one-dimensional isocrystals.
A blog post on the Lean community website.

A tutorial about formalizing mathematics in Lean. In preparation.

Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn.
Logic and Proof.
A textbook using the Lean theorem prover.