Publications

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

Peer Reviewed Publications:

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

  In preparation.