
A bidirectional extensible interface between Lean and Mathematica
We implement a userextensible ad hoc connection between the Lean proof ...
read it

Formalizing the Ring of Witt Vectors
The ring of Witt vectors 𝕎 R over a base ring R is an important tool in ...
read it

Maintaining a Library of Formal Mathematics
The Lean mathematical library mathlib is developed by a community of use...
read it

Simplifying Casts and Coercions
This paper introduces norm_cast, a toolbox of tactics for the Lean proof...
read it

Normalizing Casts and Coercions
This system description introduces norm_cast, a toolbox of tactics for t...
read it

A formal proof of Hensel's lemma over the padic integers
The field of padic numbers Q_p and the ring of padic integers Z_p are ...
read it

Formalizing the Solution to the Cap Set Problem
In 2016, Ellenberg and Gijswijt established a new upper bound on the siz...
read it

An Extensible Ad Hoc Interface between Lean and Mathematica
We implement a userextensible ad hoc connection between the Lean proof ...
read it
Robert Y. Lewis
is this you? claim profile