Session I: Foundations -- A Proof-Theoretic Approach to Hierarchical Math Library Organization -- An Exploration in the Space of Mathematical Knowledge -- Session II: Authoring -- Authoring Presentation for openmath -- Translating Mathematical Vernacular into Knowledge Repositories -- Assisted Proof Document Authoring -- Session III: Representations -- A Tough Nut for Mathematical Knowledge Management -- Textbook Proofs Meet Formal Logic – The Problem of Underspecification and Granularity -- Processing Textbook-Style Matrices -- Session IV: Proving -- A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity -- Impasse-Driven Reasoning in Proof Planning -- Literate Proving: Presenting and Documenting Formal Proofs -- Session V: MKManagement Tools -- Semantic Matching for Mathematical Services -- Mathematical Knowledge Browser with Automatic Hyperlink Detection -- A Database of Glyphs for OCR of Mathematical Documents -- Session VI: Documents -- Toward an Object-Oriented Structure for Mathematical Text -- Explanation in Natural Language of ?????-Terms -- Engineering Mathematical Knowledge -- Session VII: MKM Case Studies -- Computational Origami of a Morley’s Triangle -- Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study -- Gröbner Bases — Theory Refinement in the Mizar System -- Session VIII: Course Materials -- An Interactive Algebra Course with Formalised Proofs and Definitions -- Interactive Learning and Mathematical Calculus -- Session IX: Migration -- XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy -- Determining Empirical Characteristics of Mathematical Expression Use -- Transformations of MML Database’s Elements -- Translating a Fragment of Weak Type Theory into Type Theory with Open Terms.

This book constitutes the thoroughly refereed post-proceedings of the 4th International Conference on Mathematical Knowledge Management, MKM 2005, held in Bremen, Germany in July 2005. The 26 revised full papers presented were carefully selected during two rounds of reviewing and improvement from 38 submissions. The papers in this volume cover the whole area of mathematical knowledge management. Topics range from foundations and the representational and document-structure aspects of mathematical knowledge, over process questions like authoring, migration, and consistency management by automated theorem proving to applications in e-learning and case studies.