Der Code der Mathematik

Motiviert durch aktuelle Entwicklungen in der abhngigen Typentheorie und bei Unendlichkategorien prsentiert dieses Buch die Ideengeschichte der Begriffe Wahrheit, Beweis, Gleichheit und quivalenz. Neben ausgewhlten Ideen von Platon, Aristoteles, Leibniz, Kant, Frege und anderen werden Resultate von Gdel und Tarski ber Unvollstndigkeit, Unentscheidbarkeit und Wahrheit in deduktiven Systemen und ihren semantischen Modellen vorgestellt. Der Hauptgegenstand dieses Textes ist die abhngige Typentheorie und neuere Entwicklungen in der Homotopy Type Theory. Diese Theorien beinhalten Identittstypen, die neue Mglichkeiten fr Gleichheit, Symmetrie, quivalenz und Isomorphie auf konzeptuelle Weise erffnen. Die Interaktion von Typentheorie und Unendlichkategorien ist ein neues Paradigma fr eine strukturelle Sichtweise auf die Mathematik. Sie frdert auch den neuen Trend zur Formalisierung von Mathematik in Form von Beweisassistenten.