Eine kleine Gemeinschaft von Mathematikern nutzt Lean, um eine neue digitale Basis aufzubauen. Sie hoffen, dass dies die Zukunft ihres wissenschaftlichen Fachgebiets sichern wird.
Jeden Tag treffen sich Dutzende gleichgesinnter Mathematiker im Zulip-Chat, um daran zu arbeiten, was ihrer Meinung nach die Zukunft ihres wissenschaftlichen Fachgebiets gestalten soll.
Sie alle sind Fans des Lean- Programms . Es ist ein interaktives Theorembeweisungswerkzeug, das im Prinzip Mathematikern helfen kann, Beweise zu schreiben. Dazu müssen Mathematiker jedoch manuell mathematische Regeln in die Programmbasis eingeben, um das über Tausende von Jahren gesammelte Wissen in eine Form zu bringen, die ein Computer verstehen kann.
Für viele Projektteilnehmer sind die Vorteile kaum oder gar nicht zu erklären.
"Grundsätzlich ist es offensichtlich, dass etwas, das einmal digitalisiert wurde, auf neue Weise verwendet werden kann", sagte Kevin Buzzardvom Imperial College London. "Und wir werden die Mathematik digitalisieren und verbessern."
Die Digitalisierung der Mathematik ist ein alter Traum. Die erwarteten Vorteile reichen von der trivialen Überprüfung der Hausaufgaben der Schüler mit Computern bis zum Außergewöhnlichen: Verwendung künstlicher Intelligenz, um neue mathematische Entdeckungen zu machen und neue Lösungen für alte Probleme zu finden. Mathematiker glauben, dass automatische Theoremprüfer auch in der Lage sein werden, Artikel zu überprüfen, die in Zeitschriften eingereicht wurden, Fehler zu finden, die von menschlichen Rezensenten manchmal übersehen werden, und sich an der mühsamen technischen Arbeit zu beteiligen, den Beweis mit allen erforderlichen Details auszufüllen.
Aber zuerst müssen Mathematiker, die sich in einem Chat treffen, Lean im Rahmen der Schulmathematik mit Wissen ausstatten, und bis jetzt ist diese Aufgabe nur zur Hälfte erledigt. In naher Zukunft ist es unwahrscheinlich, dass Lean offene Probleme lösen kann, aber die Mitarbeiter der Basis sind sich fast sicher, dass das Programm in nur wenigen Jahren zumindest lernen wird, Probleme auf Prüfungsebene in der High School zu verstehen.
Wer weiß? Die am Projekt beteiligten Mathematiker haben nicht immer eine klare Vorstellung davon, wofür digitale Mathematik nützlich sein kann.
"Wir wissen nicht genau, wohin wir gehen", sagte Sebastien Gösel von der Universität Rennes.
Sie planen, Lean funktioniert
Im Sommer veranstaltete eine Gruppe fortgeschrittener Lean-Benutzer ein Online-Seminar " Lean for Curious Mathematicians ". In der ersten Lektion zeigte Scott Morrison von der University of Sydney, wie man mit einem Programm einen Beweis schreiben kann.
Zunächst schrieb er die Aussage auf, die er schlank beweisen wollte. In der menschlichen Sprache bedeutete es "es gibt unendlich viele Primzahlen". Es gibt verschiedene Möglichkeiten, diese Behauptung zu beweisen, aber Morrison wollte eine leicht modifizierte Version der ersten Beweise verwenden, die Euklid ab 300 v. Chr. Gefunden hatte. Im Beweis werden alle bekannten Primzahlen multipliziert, und nach Addition von 1 wird eine neue Primzahl erhalten (entweder das Produkt selbst oder einer seiner Teiler ist eine Primzahl). Morrisons Wahl basierte auf einer der Grundregeln für die Verwendung von Lean: Der Benutzer muss die Hauptidee des Beweises selbst entwickeln.
"Sie sind für die erste Vermutung verantwortlich", sagte Morrison in einem Interview.
Nachdem Morrison die Behauptung eingegeben und eine Strategie ausgewählt hatte, skizzierte er in wenigen Minuten die Struktur des Beweises. Er identifizierte eine Abfolge von Zwischenschritten, von denen jeder relativ leicht zu beweisen war. Lean kann zwar keine allgemeine Beweisstrategie anbieten, kann Ihnen jedoch dabei helfen, kleine, konkrete Schritte auszuführen. Morrison zerlegte den Beweis in zugängliche Unteraufgaben und war ein bisschen wie ein Koch, der gewöhnliche Köche anwies, Zwiebeln zu hacken oder Wasser zu kochen. "Hier hoffen Sie, dass Lean die Kontrolle übernimmt und Ihnen hilft", sagte Morrison.
Lean erledigt Zwischenaufgaben mithilfe automatisierter Prozesse, die als Taktik bezeichnet werden. Hierbei handelt es sich um kurze Algorithmen, mit denen sehr spezifische Aufgaben ausgeführt werden können.
Morrison arbeitete mit Beweisen und startete eine Taktik namens Bibliothekssuche. Sie durchsuchte die Mathematikdatenbank des Programms und gab mehrere Sätze zurück, von denen sie glaubte, dass sie die Lücken in einem bestimmten Abschnitt des Beweises füllen könnten. Unterschiedliche Taktiken führen unterschiedliche mathematische Aufgaben aus. Einer von ihnen, Linarith, kann eine Reihe von Ungleichungen für beispielsweise zwei reelle Zahlen nehmen und die Wahrheit der neuen Ungleichung bestätigen, die die dritte Zahl enthält: Wenn a 2 ist und b größer als a ist, dann ist 3a + 4b größer als 12. Der andere macht den größten Teil der Arbeiten Sie mit algebraischen Grundregeln wie Assoziativität.
"Vor zwei Jahren musste die Assoziativität bei Lean manuell angewendet werden", sagte Amelia Livingston, eine Mathematikstudentin am Imperial College London, die Lean bei Buzzard studiert. - Und dann hat jemand eine Taktik geschrieben, die das für Sie erledigt. Ich bin jedes Mal glücklich, wenn ich es benutze. "
Insgesamt brauchte Morrison 20 Minuten, um den Beweis von Euklid zu vervollständigen. Hier und da vervollständigte er die Details selbst; manchmal haben die Taktiker es für ihn getan. Nach jedem Schritt überprüfte Lean die Konsistenz des Beweises anhand integrierter logischer Regeln, die in einer formalen Sprache namens abhängige Typentheorie geschrieben waren .
„Es sieht aus wie eine Sudoku-App. Wenn Sie einen falschen Schritt machen, ertönt ein Piepton “, sagte Buzzard. Infolgedessen bestätigte Lean die Verarbeitbarkeit von Morrisons Beweis.
Es war eine sehr lustige Übung - wie es normalerweise der Fall ist, wenn Technologie etwas für Sie tut. Euklids Beweis gibt es jedoch seit über 2000 Jahren. Die Fragen der heutigen Mathematiker sind so komplex, dass Lean die Fragen immer noch nicht verstehen kann, geschweige denn helfen kann, sie zu beantworten.
"Es wird wahrscheinlich Jahrzehnte dauern, bis dieses Tool bei der Forschung hilft", sagte Heather Macbeth von der Fordham University, eine der Benutzerinnen von Lean.
Bevor Mathematiker mit Lean an Fragen arbeiten können, die für sie wirklich interessant sind, müssen sie dem Programm weitere mathematische Regeln hinzufügen. Und das ist in der Tat eine ziemlich einfache Aufgabe.
Anatomie eines Proof-Building-Programms: Lean hilft Mathematikern, Theoreme zu beweisen, indem es die Arbeit überprüft und einige Proof-Schritte automatisiert.
1) Der Mathematiker beschreibt die Grundstruktur des Beweises und schreibt die Abfolge der Schritte in Lean auf.
2) Die Mathlib-Bibliothek von Mathematikprogrammen verfügt über eine Reihe von Taktiken, die die Schritte dieses Beweises ausführen. Mathematiker fügen Mathlib immer wieder neue Daten hinzu. Die bewährten Theoreme werden zu mathlib hinzugefügt.
3) Der Kernel-Algorithmus überprüft die Richtigkeit des Beweises anhand einfacher Regeln.
* Der Oktopus ist irgendwie zu einer Bezeichnung für freudige Emotionen in der Lean-Community geworden.
"Damit Lean etwas verstehen kann, müssen die Leute Mathematiklehrbücher in eine Form übersetzen, die das Programm verstehen kann", sagte Morrison.
Leider bedeutet die Einfachheit eines Problems nicht, dass es leicht zu lösen ist - da ein Großteil der Mathematik nicht in Lehrbüchern behandelt wird.
Verstreutes Wissen
Wenn Sie keine fortgeschrittene Mathematik studiert haben, scheint Ihnen dieser Bereich genau und gut beschrieben zu sein. Algebra, Differentialrechnung, mathematische Analyse - alles folgt aus allem, und es gibt Antworten auf alle Fragen, die am Ende des Lehrbuchs aufgeführt sind.
Die Mathematik im Lehrplan, im Lehrplan und sogar im größten Teil der Universität ist jedoch ein verschwindend kleiner Teil des gesamten Wissens. Die meisten von ihnen sind nicht gut organisiert.
Es gibt große und wichtige Bereiche der Mathematik, die nicht vollständig beschrieben werden. Sie sind in den Köpfen einer kleinen Anzahl von Menschen gespeichert, die ihr Teilgebiet Mathematik von Menschen gelernt haben, es von denen gelernt haben, die es erfunden haben - das heißt, sie existieren auf der Grundlage von Folklore.
Es gibt andere Bereiche, in denen das Grundmaterial niedergeschrieben wurde, aber es ist so komplex und lang, dass noch niemand seine Richtigkeit überprüfen konnte. Stattdessen glauben Mathematiker einfach an ihn.
„Wir verlassen uns auf den Ruf des Autors. Wir wissen, dass er ein Genie und ein akribischer Typ ist, daher ist der Beweis höchstwahrscheinlich wahr “, sagte Patrick Massot von der Universität Paris-Saclay.
Dies ist einer der Gründe, warum Theoremprüfungsprogramme so attraktiv sind. Die Übersetzung von Mathematik in eine für einen Computer verständliche Sprache zwingt Mathematiker, ihr Wissen endgültig zu katalogisieren und alle Objekte genau zu definieren.
Assia MabubiDas französische staatliche Institut für Informatik- und Automatisierungsforschung erinnert sich an das erste Mal, als sie das Potenzial einer solchen geordneten digitalen Bibliothek erkannte: „Ich war fasziniert von der Möglichkeit, die gesamte mathematische Literatur theoretisch in der Sprache der reinen Logik zu erfassen, die gesamte mathematische Bibliothek auf einem Computer zu speichern, Daten darin zu überprüfen und zu suchen mit Hilfe von Programmen ".
Lean ist nicht das erste Programm, das dieses Potenzial besitzt. Der erste, Automath, erschien in den 1960er Jahren, und Coq, einer der beliebtesten heute, erschien 1989. Coq-Benutzer formalisierten viel Mathematik in Programmsprache, aber diese Arbeit war dezentralisiert und nicht gut organisiert. Mathematiker arbeiteten nur an Projekten, die für sie von Interesse waren, und identifizierten nur die Objekte, die sie für ihre eigene Arbeit benötigten, und beschrieben sie häufig auf einzigartige Weise. Infolgedessen sehen die Bibliotheken für Coq überladen aus, wie ein Plan für eine Stadt, die auf natürliche Weise gewachsen ist.
"Coq ist heute ein alter Mann mit Narben", sagte Mabubi, der mit dem Programm aktiv war. "Er wurde lange Zeit von vielen Menschen unterstützt, und dank seiner langen Geschichte sind seine Mängel mittlerweile bekannt."
Im Jahr 2013 startete Leonardo de Mura , ein Forscher bei Microsoft, das Lean-Projekt. Sein Name [schlank] spiegelt de Moores Wunsch wider, ein effizientes und sauberes Programm zu erstellen. Er ging davon aus, dass das Programm ein Werkzeug zur Überprüfung der Genauigkeit des Codes anderer Programme sein würde, nicht der Mathematik. Es stellt sich jedoch heraus, dass das Überprüfen der Richtigkeit eines Programms dem Überprüfen eines Beweises sehr ähnlich ist.
"Wir haben Lean entwickelt, weil wir an Softwareentwicklung interessiert sind, und es gibt eine Analogie zwischen dem Erstellen von Mathematik und dem Schreiben von Code", sagte de Moore.
Heather Macbeth von der Fordham University, eine der Lean-Benutzerinnen
Zum Zeitpunkt der Veröffentlichung von Lean gab es einige andere Hilfsprogramme, darunter Coq, das Lean am ähnlichsten ist. Die logische Grundlage für beide Programme basiert auf der Theorie der abhängigen Typen. Lean bietet jedoch die Möglichkeit, von vorne zu beginnen.
Sie zog schnell Mathematiker an. Sie nutzten es mit solcher Begeisterung, dass sie anfingen, die gesamte Freizeit von de Moore mit ihren Fragen zur Entwicklung auf dem Gebiet der Mathematik zu verbringen. "Er hatte ein bisschen genug von führenden Mathematikern und sagte - warum macht ihr nicht ein separates Repository?" Sagte Morrison.
Mathematiker haben diese Bibliothek im Jahr 2017 erstellt. Sie nannten es Mathlib und machten sich eifrig daran, es mit weltmathematischem Wissen zu füllen und so etwas wie ein Analogon der Bibliothek von Alexandria zu schaffen.im 21. Jahrhundert. Mathematiker erstellten und luden Ausschnitte digitalisierter Mathematik hoch und erstellten schrittweise einen Katalog für Lean. Und da mathlib neu war, konnten sie aus den Einschränkungen früherer Systeme wie Coq lernen und verfolgen, wie das Material organisiert war.
"Es wird absichtlich versucht, eine monolithische mathematische Bibliothek zu erstellen, deren Fragmente miteinander funktionieren", sagte Macbeth.
Alexandrian Mathlib
Die mathlib Projekt - Homepage hat Graphen , die die Fortschritte des Projekts in Echtzeit zeigt. Das Projekt hat eine Liste von Führungskräften, die am meisten in das Projekt investieren, sortiert nach der Anzahl der Codezeilen [übrigens ist der russische Mathematiker Juri Kudryaschow / ca. übersetzt.]. Die Gesamtzahl der digitalisierten mathematischen Objekte wird ebenfalls berechnet: Anfang Oktober enthält sie 18.756 Definitionen und 39.157 Theoreme.
Alle diese Bestandteile der Mathematik können miteinander gemischt werden, um Mathematik in Lean zu erstellen. Bisher ist ihre Reichweite trotz der scheinbar beeindruckenden Zahlen stark eingeschränkt. Es gibt fast nichts aus Bereichen komplexer Analyse oder Differentialgleichungen - und dies sind zwei Grundelemente vieler Bereiche höherer Mathematik. Darüber hinaus weiß das Programm noch nicht genug, um eines der Millenniumsprobleme zu beschreiben - mathematische Probleme, die vom Clay Mathematical Institute im Jahr 2000 als "wichtige klassische Probleme, die seit vielen Jahren nicht mehr gelöst wurden" definiert wurden.
mathlib füllt sich langsam aber sicher aus. Die Arbeit erfolgt im Geiste der Teamarbeit. Im Zulip-Chat wählen Mathematiker Definitionen aus, die formalisiert werden müssen, werden aufgefordert, diese aufzuschreiben und umgehend Feedback zur Arbeit anderer zu geben.
"Jeder Forschungsmathematiker kann Mathlib studieren und eine Liste von 40 Dingen erstellen, die nicht da sind", sagte Macbeth. - Also beschließt er, einen dieser Mängel zu beheben. Und sofortiges Vergnügen ist garantiert - jemand wird Ihre Arbeit lesen und innerhalb von 24 Stunden einen Kommentar dazu hinterlassen. "
Viele Add-Ons sind klein - wie Sophie Morel herausfandvon der Lyon Normal School während des Online-Seminars "Lean for Curious Mathematicians". Die Organisatoren der Konferenz gaben den Teilnehmern relativ einfache mathematische Aussagen, die sie in Lean als Praxis beweisen konnten. In Zusammenarbeit mit einem von ihnen erkannte Morel, dass ihr Beweis ein Lemma erforderte - ein kleines Zwischenergebnis -, das in Mathlib nicht gefunden wurde.
„Es war ein kleines Stück aus der linearen Algebra, das aus irgendeinem Grund noch nicht da war. Die Leute, die Mathlib füllen, versuchen, alles zu erfassen, aber Sie können nicht alle Optionen vorhersehen “, sagte Morel, die das erforderliche Lemma in drei Zeilen selbst in die Basis einging.
Andere Beiträge sind wichtiger. Seit einem Jahr arbeitet Gösel an der Definition eines glatten Verteilers für Mathlib. Glatte Mannigfaltigkeiten sind Mengen (wie Linien, Kreise oder Oberflächen einer Kugel), die eine grundlegende Rolle bei der Untersuchung von Geometrie und Topologie spielen. Sie spielen auch häufig eine wichtige Rolle bei Problemen aus Bereichen wie der Zahlentheorie und der Analysis. Die meisten mathematischen Forschungen sind ohne sie nicht möglich.
Glatte Verteiler können sich jedoch unter verschiedenen Deckmänteln verstecken - alles hängt vom Kontext ab. Sie können eine endliche oder unendliche Anzahl von Dimensionen haben, Grenzen haben oder nicht, über verschiedene Zahlensysteme definiert werden - auf der Menge von real, komplex oder p-adischZahlen. Die Definition einer reibungslosen Vielfalt ist wie die Definition von Liebe: Sie erkennen sie, wenn Sie sie treffen, aber jede strenge Definition lässt sicherlich einige der offensichtlichsten Beispiele für dieses Phänomen fallen.
"Wenn Sie grundlegende Dinge definieren, müssen Sie keine Entscheidungen treffen", sagte Gösel. "Komplexere Objekte können jedoch auf 10 bis 20 verschiedene Arten formalisiert werden."
Gösel muss ein Gleichgewicht zwischen Spezifität und Verallgemeinerung aufrechterhalten. "Ich hatte eine Regel - ich wollte in der Lage sein, 15 verschiedene Verwendungen von Verteilern zu definieren", sagte er. "Gleichzeitig wollte ich nicht, dass die Definition zu allgemein ist, sonst wäre es unmöglich, damit zu arbeiten."
Die Definition, die er entwickelt hat, passt in 1.600 Codezeilen - ziemlich viel für eine Definition von mathlib, aber vielleicht nicht so sehr im Vergleich zu allen mathematischen Möglichkeiten, die er Lean eröffnet.
"Jetzt, da wir die Sprache haben, die wir brauchen, können wir beginnen, Theoreme zu beweisen", sagte er.
Die richtige Definition eines Objekts mit dem richtigen Grad an Allgemeinheit zu finden, ist die Hauptbeschäftigung der Mathematiker, die Mathlib füllen. Die Ersteller der Bibliothek hoffen, Objekte auf eine Weise zu definieren, die heute nützlich und gleichzeitig so flexibel ist, dass diese Objekte heute auf unvorhersehbare Weise verwendet werden können.
"Die Notwendigkeit, dass alles für den Einsatz in ferner Zukunft nützlich ist, wird unterstrichen", sagte Macbeth.
Perfectoids werden aus der Praxis geboren
Lean ist jedoch nicht nur ein nützliches Werkzeug, sondern bietet Mathematikern auch die Möglichkeit, ihre Arbeit wieder aufzunehmen. Macbeth erinnert sich noch immer an das erste Mal, als sie ein Programm zum Schreiben von Beweisen ausprobierte. Es war 2019 und das Programm war Coq (obwohl es jetzt auf Lean umgestellt wurde). Sie konnte nicht aufhören.
"An einem verrückten Wochenende habe ich 12 Stunden hintereinander mit diesem Programm gearbeitet", sagte sie. "Es war eine echte Sucht."
Andere Mathematiker beschreiben ihre Erfahrungen auf ähnliche Weise. Lean, sagen sie, ist wie ein Computerspiel - bis auf die gleichen Belohnungshormone, die es schwierig machen, einen Gamecontroller beiseite zu legen. "Sie können dies 14 Stunden am Tag tun, ohne sich den ganzen Tag müde und in einem erhöhten Zustand zu fühlen", sagte Livingston. "Sie erhalten ständig positives Feedback."
Sebastien Gösel
Die Lean-Community versteht jedoch, dass es für viele Mathematiker einfach nicht genug Level in ihrem Programm gibt.
"Wenn Sie den Prozentsatz der formalisierten Mathematik quantifizieren, würde ich sagen, dass noch weniger als ein Tausendstel Prozent fertig ist", sagte Christian Szegedi, ein Google-Programmierer, der an KI-Systemen arbeitet und davon träumt, Mathematiklehrbücher unabhängig lesen und formalisieren zu können.
Aber Mathematiker erhöhen diesen Prozentsatz. Wenn Mathlib heute den größten Teil des Materials enthält, das von Studenten im zweiten Studienjahr unterrichtet wird, hoffen die Projektteilnehmer, den Rest des Programms in ein paar Jahren hinzuzufügen - und dies wird eine bedeutende Leistung sein.
"In allen 50 Jahren dieser Systeme hat niemand vorgeschlagen: Setzen wir uns und organisieren eine konsistente Wissensbasis der Mathematik, die das Institutsmaterial beschreibt", sagte Buzzard. "Wir schaffen etwas, das die Fragen der Institutsprüfung verstehen kann - das ist noch nie passiert."
Es wird wahrscheinlich Jahrzehnte dauern, bis der Inhalt von mathlib mit der Forschungsbibliothek übereinstimmt, aber Lean-Benutzer demonstrieren zumindest die theoretische Möglichkeit, einen solchen Katalog zu erstellen - und das Erreichen dieses Ziels hängt einfach davon ab, dass die gesamte Mathematik in Form von Programmcode in die Datenbank eingegeben wird.
Zu diesem Zweck haben Buzzard, Masso und Johan Kommelin von der Universität Freiburg im vergangenen Jahr ein Projekt umgesetzt, das die Realisierbarkeit dieses Traums beweist. Sie haben die schrittweise Befüllung der Basis mit Institutsmaterial vorübergehend verschoben und sind in fortgeschrittene Gebiete übergegangen. Ihr Ziel war es, eine der größten Innovationen in der Mathematik des 21. Jahrhunderts zu identifizieren - ein Objekt wie den "Perfectoid Space", der in den letzten zehn Jahren von Peter Scholze von der Universität Bonn entwickelt wurde. 2018 erhielt er für seine Arbeit den Fields Prize, den größten Preis in Mathematik.
Buzzard, Masso und Commelin wollten zeigen, dass Lean zumindest im Prinzip mit Mathematik arbeiten kann, an der Mathematiker wirklich interessiert sind. "Sie nahmen etwas sehr Komplexes und Neues und zeigten, dass diese Objekte mit einem Programm manipuliert werden können, um Beweise zu schreiben", sagte Mabubi.
Kevin Buzzard
Um einen Perfectoid-Raum zu definieren, mussten drei Mathematiker mehr als 3.000 Definitionen mathematischer Objekte und 30.000 Verbindungen zwischen ihnen kombinieren. Die Definitionen erstrecken sich über viele Bereiche der Mathematik, von der Algebra über die Topologie bis hin zur Geometrie. Sie in einer Definition zusammenzufassen, war ein eindrucksvoller Beweis für die zunehmende Komplexität der Mathematik im Laufe der Zeit - und warum es so wichtig ist, die Grundlagen für Mathlib richtig zu machen.
"In vielen Bereichen der fortgeschrittenen Mathematik müssen Sie alle Arten von Mathematik kennen, die den Schülern beigebracht werden", sagte Macbeth.
Der Dreifaltigkeit ist es gelungen, den Perfectoid-Raum zu definieren, aber bisher gibt es wenig, was Mathematiker damit anfangen können. Viele weitere mathematische Definitionen müssen in Lean eingeführt werden, bevor das Programm zumindest die komplexen Fragen formulieren kann, in denen diese perfektoiden Räume entstehen.
"Es ist ziemlich albern, dass Lean weiß, was ein perfekter Raum ist, aber keine komplexe Analyse kennt", sagte Masso.
Buzzard stimmt ihm zu und nennt die Formalisierung des Perfectoid-Raums eine "Spielerei" - ein Trick, mit dem manchmal neue Technologien gezeigt werden, um ihre Nützlichkeit zu demonstrieren. Und diesmal hat der Trick funktioniert.
"Sie müssen nicht glauben, dass dank unserer Arbeit alle Mathematiker auf der Erde Programme verwendeten, um Beweise zu schreiben", sagte Masso, "aber ich denke, viele von ihnen haben diese Möglichkeit bemerkt und angefangen, Fragen zu stellen."
Es wird lange dauern, bis Lean zu einem echten Bestandteil der mathematischen Forschung wird. Dies bedeutet jedoch nicht, dass das Programm heute ein Bild aus der Science-Fiction ist. Die an seiner Entwicklung beteiligten Mathematiker vergleichen ihre Arbeit mit der Verlegung der ersten Eisenbahnschienen - dem notwendigen Start eines wichtigen Unternehmens, auch wenn sie selbst möglicherweise nicht in der Lage sind, auf der Strecke zu fahren.
"Es wird so cool, dass es sich heute lohnt", sagte Macbeth. "Ich investiere heute meine Zeit in sie, damit jemand in der Zukunft eine so erstaunliche Erfahrung mit ihr machen kann."