5 papers
Iris in Lean
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu +9
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-…
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Matthew Bolan, Joachim Breitner, Jose Brox +31
We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project suc…
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Magnus O. Myreen, Mario Carneiro
Conway's Game of Life (GOL) is a cellular automaton that has captured the interest of hobbyists and mathematicians alike for more than 50 years. The Game of Life is Turing complete…
Lean4Lean: Verifying a Typechecker for Lean, in Lean
Mario Carneiro
In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference im…
Arithmetic in Metamath, Case Study: Bertrand's Postulate
Mario Carneiro
Unlike some other formal systems, the proof system Metamath has no built-in concept of "decimal number" in the sense that arbitrary digit strings are not recognized by the system w…