My CV is often more up-to-date than this page.
Peer Reviewed Publications:
-
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.
Books and Drafts:
-
Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, and Patrick Massot.
A tutorial about formalizing mathematics in Lean. In preparation.
-
Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn.
A textbook using the Lean theorem prover.
-
Robert Y. Lewis and Minchao Wu.
A bi-directional extensible ad hoc interface between Lean and Mathematica.
Under review.