In computerüberprüfbaren Beweisen sehen manche die Zukunft der Mathematik. Darüber, auf welchen formalen Grundlagen man Computerbeweise aufbauen sollte, gab es in den letzten Wochen einige hitzige Debatten. An möglichen Grundlagen für die Mathematik und insbesondere für formale Theorembeweiser gibt es neben der von den meisten Mathematikern verwendeten Mengenlehre („set theory“) noch verschiedene Arten von Typentheorien:…
Typentheorie ist ein Teil der Mathematik, von dem ich überhaupt nichts verstehe, obwohl sie zur Zeit sehr angesagt zu sein scheint. Grob gesagt geht es um die jedem Informatiker ins Blut gegangene Tatsache, dass das Ergebnis einer Verknüpfung mehrerer Objekte davon abhängt, zu welchem Typ die jeweiligen Objekte gehören: 2+2 kann 4 oder 22 sein,…
Letzte Kommentare