One of the main application areas of interactive proof assistants is the formalization of mathematical texts. This formalization not only allows mathematical texts to be handled electronically, but also to be checked for correctness. Due to the level of detail required in the formalization, formalized texts eliminate ambiguities that may be present in an informally presented mathematical texts.
|Title of host publication||Mathematical Knowledge Management (Fourth International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised selected papers)|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|