Publications

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

Peer Reviewed Publications:

• 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.

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.