Reading an algebra textbook.
Clemens Ballarin · 2013
Abstract. We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising. 1