1 paper · 1 filter
Thomas Browning, Patrick Lutz
We describe a project to formalize Galois theory using the Lean theorem prover, which is part of a larger effort to formalize all of the standard undergraduate mathematics curricul…