3 papers
math.RA2025
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…
cs.PL2025
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…
cs.FL2025
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…