Robert Y. Lewis

Robert Y. Lewis

Lecturer at Brown University. Proof assistants, formal mathematics, logic, computation.

A formal proof of Hensel’s lemma over the p-adic integers

less than 1 minute read

Published:

Here you will find the supplementary materials to my paper A formal proof of Hensel’s lemma over the p-adic integers. This paper was published at CPP 2019. For more information, contact Robert Y. Lewis.

The Formal Development

The project described in the linked paper has been incorporated into the Lean mathlib repository. The current state of the p-adic number development can be found in the directory /data/padics/. See also the pull requests here and here.

Since mathlib is regularly updated, we preserve a branch here that shows its state when this paper was written.

You May Also Enjoy

Logic and Modeling course information

less than 1 minute read

Published:

In Spring 2020, I taught the course Logic and Modeling at the VU. The course was held entirely online due to the COVID-19 pandemic.

The Lean mathematical library

less than 1 minute read

Published:

Along with a number of other contributors, I have written a paper about the Lean mathematical library. The paper describes a large-scale, open project to which 68 people (and counting) have contributed. Rather than attribute the paper to some subset of this group, we decided to release it as a community effort. (Update, Nov 28: our paper has been accepted at CPP!)