We give an overview of mathematical music theory as it has been developed in the past twenty years. The present theory includes a formal language for musical and musicological objects and relations. This language is built upon topos theory and its logic. Various models of musical phenomena have been developed. They include harmony (function theory, cadences, and modulations), classical counterpoint (Fux rules), rhythm, motif theory, and the theory of musical performance. Most of these models have also been implemented and evaluated in computer applications. Some models have been tested empirically in neuro-musicology and the cognitive science of music. The mathematical nature of this modeling process canonically embedds the given historical music theories in a variety of fictitious theories and thereby enables a qualification of historical reality against potential variants. As a result, the historical realizations often turn out to be some kind of »best possible world« and thus reveals a type of »anthropic principle« in music.

These models use different types of mathematical approaches, such as--for instance--enumeration combinatorics, group and module theory, algebraic geometry and topology, vector fields and numerical solutions of differential equations, Grothendieck topologies, topos theory, and statistics. The results lead to good simulations of classical results of music and performance theory. There is a number of classifiaction theorems of determined categories of musical structures.

The overview concludes by a discussion of mathematical and musicological challenges which issue from the investigation of music by mathematics, including the project of »Grand Unification« of harmony and counterpoint and the classification of musical performance.