Der Philosoph Karl Popper ist vor allem dafür bekannt, geschlossene Denkstrukturen angegriffen zu haben, sowohl in der Politik („Die offene Gesellschaft und ihre Feinde“) wie in der Wissenschaft („Vermutungen und Widerlegungen“). Das ging dann soweit, dass er Wissenschaft als auf die Falsifikation von wissenschaftlichen Theorien ausgerichtet sehen wollte, statt auf deren Konstruktion. “Unser Wissen ist…

Algorithmen kontrollieren immer mehr, aber wer kontrolliert eigentlich die Algorithmen? Einen eher harmlosen(1) Aspekt dieses Themas diskutiert seit einigen Tagen die Frage- und Antwortseite mathoverflow: Proof assistent, cura te ipsum2 (1) nicht nur weil Beweisassistenten im Alltagsgeschäft der Mathematik noch keine große Rolle spielen (2) dtsch.: “Beweisassistent, heile dich selbst” Die Frage ist, wie man…

Das P=NP-Problem ist der heilige Gral der theoretischen Informatik, auf seine Lösung hat das Clay-Institut ein Preisgeld von 1 Million Dollar ausgesetzt. Es fragt, ob jedes von einer nichtdeterministischen Turingmaschine in polynomieller Zeit lösbare Problem auch von einer deterministischen Turingmaschine in polynomieller Zeit gelöst werden kann. Ein gestern von Norbert Blum, Informatikprofessor an der Universität…

Vor Jahren hörte ich mal einen Kolloquiumsvortrag, in dem ein australischer Professor über eine Theorie referierte, in der aus der Verneinung der Verneinung nicht die Richtigkeit einer Aussage folgt. Zum Abschluß meinte er noch geheimnisvoll, seine Theorie sei “not without applications” und war sich der Komik dieses Statements – aus dem in seiner Logik ja…

Vor zwei Wochen hat Google’s ALphaGo Sedol Lee geschlagen und seitdem geht unter Mathematikern die (je nachdem) Angst oder Hoffnung um, dass Computer bald auch besser mathematische Theoreme finden und beweisen könnten als wir. Diskutiert wird das auch auf MathOverflow, eigentlich die Seite für fachmathematische Fragen und Antworten, aber gelegentlich auch für Metadebatten. Dort wird…

|- import_tame_classification /\ the_nonlinear_inequalities ==> the_kepler_conjecture ist ein mit Hilfe von HOL formalisiertes Theorem, wobei the_kepler_conjecture definiert ist durch `(!V. packing V ==> (?c. !r. &1 &(CARD(V INTER ball(vec 0,r)))

Noch ein Nachtrag zum Artikel von gestern: ob Fermat seine berühmte Randnotiz wirklich so geschrieben hat wie wir sie kennen, das ist durchaus nicht erwiesen – die einzige Quelle hierfür ist bekanntlich sein Sohn, der den Nachlass herausgab mit den Randnotizen in Diophants Arithmetica. Noch viel unklarer ist, ob Fermat wirklich meinte, was er schrieb,…

Vor einigen Jahren hatten wir hier mal zu den neuen Möglichkeiten der Computer-Verifikation mathematischer Beweise geschrieben (Was ist ein Beweis?). Das Thema hat sich inzwischen weiterentwickelt, u.a. gab es am IAS in Princeton ein thematisches Jahr 2012/13 über die “univalenten Grundlagen der Mathematik”, aus dem auch ein Buch hervorgegangen ist, und natürlich gab es einige…

Im Februar 2012 wurde die Willmore-Vermutung bewiesen. Sie beschreibt, welche Donuts Seifenblasen am nächsten kommen, d.h. die geringste Willmore-Energie haben. Willmore-Energie Wir hatten uns hier in der Reihe einige Folgen lang mit Minimalflächen befaßt, u.a. in TvF 233 etwas über die Klassifikation der Minimalflächen im R3 geschrieben (soweit bekannt). Diese Minimalflächen im R3 haben immer…

Bei Math Overflow ist mir zufällig dieser alte Thread aufgefallen, der -obwohl längst geschlossen- es doch noch mal auf die Startseite geschafft hatte. Es ging um mathematische Beweise durch suggestive Bilder. Einige Beispiele: