Publications

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.

  Mathematics in Lean.

  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.

• Robert Y. Lewis and Minchao Wu.

  A bi-directional extensible ad hoc interface between Lean and Mathematica.

  Under review.