Formalizing Abstract Mathematics: Issues and Progress
Abstract: Many well-known theorems in mathematics have been formalized using a variety of tools and formal systems. Despite this success, some kinds of material remain difficult to formalize, especially if our aim is to develop an ever-growing book of mathematics rather than stopping once a certain theorem has been proved. Algebra, with its numerous abstract concepts that are refined and combined in countless ways, is particularly difficult to formalize, but other branches of mathematics, such as topology, present similar difficulties. The speaker will describe recent progress in this area using Isabelle's locale construct.