StartseiteMathlog

7824

Von / 31. Mai 2016 / 17 Kommentare
Mehr

“Der längste Mathe-Beweis der Welt” nennt es Spiegel Online. 200 Terabyte lang ist die Berechnung, wieviele natürliche Zahlen sich mit zwei Farben (rot und blau) färben lassen ohne dass es ein einfarbiges pythagoräisches Zahlentripel gibt. (Ein pythagoräisches Zahlentripel ist eine ganzzahlige Lösung der Gleichung a2+b2=c2, zum Beispiel 32+42=52 oder 52+122=132. Wenn man also beispielsweise 3 und 4 rot gefärbt hat, dann muss 5 blau sein, und dann können 12 und 13 nicht beide ebenfalls blau sein.)

Für kleine Anzahlen ist es natürlich leicht, solche Färbungen zu finden. Die Frage war gewesen, welches die maximal mögliche Zahl ist, für die eine solche Lösung existiert. Die mit dem Computer gefundene Antowrt ist jetzt: 7824.
image
(Die weißen Felder entsprechen Zahlen, die in keinem pythagoräischen Tripel vorkommen, bei denen es also egal ist, wie man sie einfärbt.)

Veröffentlicht wird das in der Arbeit Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer von Heule, Kullmann und Marek.

Was bringt das jetzt für die Mathematik? William Thurston schrieb in seinem vor 20 Jahren kontrovers diskutierten Essay “On proof and progress in Mathematics”:

[…] only perpetuates the myth that our progress is measured in units of standard theorems deduced. This is a bit like the fallacy of the person who makes a printout of the first 10,000 primes. What we are producing is human understanding. We have many different ways to understand and many different processes that contribute to our understanding. We will be more satisfied, more productive and happier if we recognize and focus on this. […] More than the knowledge, people want personal understanding.

Aber natürlich bringt diese Berechnung potentiell auch etwas für das Verständnis der pythagoräischen Zahlentripel bzw. der Ramseytheorie, in die dieses Problem eigentlich gehört. Wer nach einer konzeptuellen Lösung des Problems sucht, der weiß jetzt jedenfalls was herauskommen muss und vielleicht wird das nun bekannte Ergebnis ja bei der Suche nach einem verständlichen Beweis oder zumindest bei dessen Überprüfung helfen.

Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek (2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer SAT

Stichworte: , ,
Mehr

Kommentare (17)

  1. #1 Matthias
    31. Mai 2016

    Wäre nicht hier auf scienceblogs der richtige Ort, um mehr ins Detail zu gehen? So wirklich mehr Infos als im SPON Artikel stehen hier ja nicht, und die Kommentare dort: “… einfach ausprobieren ist kein Beweis …; … für mich ist ein Computerbeweis was anderes …” usw. sprechen doch dafür, dass es Klärungsbedarf gibt.

    So weit ich das sehe, ist ja nicht “die Berechnung” 200T gross, sondern der UNSAT Beweis im DRAT Format für die in Aussagenlogik codierte Aussage, dass es mehr solcher Tripel gäbe. Während gleichzeitig die Aussage, dass es 7824 solcher Tripel gibt, erfüllbar ist und man diese auch gefunden hat.

  2. #2 Thilo
    31. Mai 2016

    Es ist natürlich richtig, dass der Computerbeweis nicht einfach nur “brute force” ist, sondern einiges an nichttrivialer Mathematik verwendet. Die Autoren ordnen ihre Arbeit in die Arbeiten zum https://de.wikipedia.org/wiki/Erfüllbarkeitsproblem_der_Aussagenlogik (SAT) und speziell in die Arbeiten der “SAT-Community” zur Ramseytheorie ein. Grob gesagt scheint der Beweis nicht in einem Durchprobieren aller möglichen Lösungen, sondern in einem Verfahren zum logischen Umformulieren der Behauptungen zu bestehen. (“A DRAT proof is a sequence of additions and deletions of clauses such that …”). Die beiden verwendeten Transformationen (“blocked clause elimination” und “symmetry breaking”) sind dann auf Seite 8 der Arbeit beschrieben.

  3. #3 cero
    31. Mai 2016

    Mich würde interessieren woher die Motivation für dieses Färbungsproblem stammt. Du hattest die Ramseytheorie erwähnt, mir ist aber nicht ganz klar welche Bedeutung dort pythagoräische Tripel haben.

    (Graphenfärbung und grundlegende Ramseytheorie kenne ich.)

  4. #4 Thilo
    31. Mai 2016

    Es ist halt ein spezielles Problem, das man in der Ramseytheorie stellen kann. Ein ähnliches, klassischeres Problem wäre der Satz von Schur https://en.wikipedia.org/wiki/Schur%27s_theorem (den deutschen Wiki-Artikel dazu finde ich eher verwirrend, auch wenn die Formulierung dort natürlich äquivalent ist). Im Satz von Schur geht es darum, die ganzen Zahlen so zu färben, dass die ganzzahligen Punkte der Ebene z=x+y niemals drei gleichen Farben entsprechen. Das Problem mit den pythagoräischen Tripeln ist im Prinzip dieselbe Aufgabe, nur dass man statt x+y=z jetzt die Gleichung x^2+y^2=z^2 betrachtet.

    Im klassischen Problem x+y=z ist übrigens 4 die maximale Lösung, schon bei Zahlen von 1 bis 5 gibt es zwangsläufig ein einfarbiges Tripel, dass die Gleichung löst. (Interessanter wird es mit mehr als zwei Farben.)

  5. #5 Dr. Webbaer
    31. Mai 2016

    Die Frage war gewesen, welches die maximal mögliche Zahl ist, für die eine solche Lösung existiert. Die mit dem Computer gefundene Antowrt ist jetzt: 7824.

    Mit dem Computer ist das Beispiel 7824 gefunden worden und mit Hilfe mathematischer Überlegungen konnten größere Zahlen ausgeschlossen werden?

    —
    Ansonsten ist diese Aussage – ‘More than the knowledge, people want personal understanding.’ – problematisch, denn es stehen dann Beweise zur Verfügung, deren Beweisführung letztlich niemand mehr nachvollziehen kann.
    BTW: Für viele Spiele gibt es mittlerweile derartige Beweise, die Richtigkeit optimaler Spielzüge meinend.

    MFG
    Dr. Webbaer

  6. #6 Thilo
    31. Mai 2016

    Mit dem Computer wurde bewiesen, dass es keine solche Färbung der Zahlen von 1 bis 7825 gibt. Der Computerbeweis ist (wie oben gesagt) nicht einfach ein Durchprobieren aller Möglichkeiten. Ob man den Computerbeweis nachvollziehen kann, ist zugegebenermaßen Ansichtssache. Ich verstehe ihn nicht, aber vielleicht ist das eher mein Problem.

  7. #7 MartinB
    31. Mai 2016

    Kannst du die Problemstellung nochmal schärfer fassen? Was genau wird gesucht?
    Eine Menge von beliebigen Zahlen, für die die Bedingung gilt, wobei die einzelnen Elemente der Menge selbst alle Bestandteil eines Zahlentripels sein müssen, dessen andere Zahlen ebenfalls in der Menge enthalten sind?

  8. #8 Thilo
    31. Mai 2016

    Die Zahlen von 1 bis 7825 sollen mit zwei Farben (rot und blau) so eingefärbt werden, dass keine drei Zahlen gleicher Farbe die Gleichung a^2+b^2=c^2 erfüllen.

    Zum Beispiel dürfen 3,4,5 nicht alle dieselbe Farbe haben. Oder 5,12,13 dürfen nicht alle dieselbe Farbe haben.

  9. #9 Matthias
    31. Mai 2016

    Das ist das Theorem aus dem Paper:

    The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.

    das ganze wird in 2 aussagenlogische Formeln codiert, der erste Teil ist erfüllbar (SAT), wobei eine solche Partition gefunden wird, der zweite Teil ist nicht erfüllbar (UNSAT), wobei ein DRAT Beweis ausgegeben wird.

    Was genau ein DRAT Beweis ist, steht auch im Artikel. Im Prinzip ist das ein Beweis, dass man aus einer Aussage “falsch” ableiten kann und damit die Aussage an sich nicht erfüllbar ist. Ein solcher Beweis ist von einem Programm nachvollziehbar, das viel simpler ist, als das Programm, das den Beweis findet.

    Damit hat man das auch für alle anderen Zahlen gezeigt, da man für alle {1..n} mit n>7825 ja auch die Teilmenge {1..7825} aufteilen müsste, was man aber nicht kann.

  10. #10 user unknown
    https://demystifikation.wordpress.com/2016/01/27/der-biodeutsche/
    1. Juni 2016

    Irritierend ist, dass immer von 2 Farben die Rede ist, aber die Beispielillustration 3 zeigt (+grün).

  11. #11 Thilo
    1. Juni 2016

    Die grüne Kante kann man rot ODER blau einfärben.

  12. #12 cero
    1. Juni 2016

    @Thilo: Ich versuche mal meine Frage anders zu stellen: Gibt es einen Grund, warum man gerade pythagoräische Tripel betrachtet statt einer beliebigen anderen Gleichung?

    Kann man pythagoräische Tripel stellvertretend für eine Reihe von Eigenschaften verwenden?

    Also warum ist der Erkenntnisgewinn hier höher als wenn ich z.B. 3x-y=5z betrachte?

    Bei dem Satz von Schur kann ich mir zumindest vorstellen, dass das zum Erkenntnisgewinn z.B. bei der Betrachtung von Minkowski-Summen (bzgl. ihrer Mächtigkeit) beiträgt.

  13. #13 Thilo
    1. Juni 2016

    Wahrscheinlich geht es einfach nur darum, dass das Problem eben viel schwieriger ist als bei einer linearen Gleichung, aber natürlich noch viel einfacher als bei komplizierteren (z.B. kubischen) Gleichungen.

  14. #14 Anderer Michael
    14. Juni 2016

    Thilo
    Mathematik war ab der 10.Klasse nur ein Rätsel für mich.
    Zum Verständnis : 7824 ist die höchste Zahl ,die gefunden wurde und entspricht cQuadrat (wie man das hochgestellte 2 eintippt weiß ich nicht) aus der Formel aQuadrat +bQuadrat= cQuadrat. Also 7824Ouadrat.
    Frage 1. Soweit richtig?

    Frage 2. Falls ja.
    2 a Wieviel Zahlen gibt es? Zur Beantwortung könnte ich die doch die blauen und roten Kästchen abzählen, geschätzt 7000.
    Frage 3 Wieviel Dreiecke lassen sich damit darstellen?

    Was mich als Nichtmathmatiker wundert, dass es eine obere Grenze gibt. Die Menge der Zahlen ist doch unendlich. Gibt es dafür eine Erklärung? Oder ist diese Frage unsinnig?

  15. #15 Thilo
    15. Juni 2016

    Ich versuche es mal mit dem einfacheren Beispiel, wenn man die Gleichung a+b=c statt a^2+b^2=c^2 nimmt.

    Dann ist also die Frage, wieviele Zahlen man rot und blau einfärben kann, ohne dass es Lösungen von a+b=c gibt, wo a,b,c die gleiche Farbe hat.

    Es ist egal, ob wir die erste Zahl rot oder blau färben; sagen wir mal, wir färben die 1 rot. Wegen 1+1=2 kann dann nicht auch die 2 rot sein, also ist die 2 blau. Wegen 2+2=4 kann dann nicht auch die 4 blau sein, also ist die 4 rot. Wegen 1+3=4 und weil 1 und 3 bereits rot sind, muss die 3 dann blau sein.

    Soweit alles kein Problem. Wir können die Zahlen von 1 bis 4 färben ohne dass es Zahlen gleicher Farbe mit a+b=c gibt.

    Die 5 können wir jetzt aber weder blau färben (denn 1 und 4 sind blau und 1+4=5) noch können wir sie rot färben (denn 2 und 3 sind rot und 2+3=5).

    Also ist 4 bei a+b=c die maximale Zahl bis zu der man färben kann und bei 5 geht es nicht mehr.

    Und bei a^2+b^2=c^2 statt bei a+b=c ist 7824 statt 4 die obere Grenze, was sich aber nicht mehr so einfach in wenigen Zeilen begründen läßt.

  16. #16 rolak
    15. Juni 2016

    →nicht mehr so einfach in wenigen Zeilen

    Ohne an der Unwahrscheinlichkeit kratzen zu wollen: Es würde mich freuen, wenn es doch geschafft würde.
    Insbesondere, wenn ich das dann verstünde ;‑)

  17. #17 Anderer Michael
    16. Juni 2016

    Danke ,kapiert. Das Grundproblem hatte ich schon nicht richtig verstanden. Deswegen ist mein Hinweis auf die Unendlichkeit der Zahlen ohne Relevanz.
    Mathe kann manchmal schon interessant sein