15 citations · 42 across the 8 of their papers we have counts for
Showing 2020Show all
3 papers · 1 filter
cs.LO2020★ 7 cited
Formalizing the Ring of Witt Vectors
Johan Commelin, Robert Y. Lewis
The ring of Witt vectors over a base ring is an important tool in algebraic number theory and lies at the foundations of modern -adic Hodge theory. $\mathbb{W…
cs.PL2020★ 15 cited
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…
cs.PL2020★ 1 cited
Simplifying Casts and Coercions
Robert Y. Lewis, Paul-Nicolas Madelaine
This paper introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frust…