terence tao bietet eine belohnung für das stärkste gehirn im internet! ki-menschen unterwandern mathematische probleme? die internetnutzer von versailles sind weg
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
herausgeber: aeneas so schläfrig[einführung in die neue weisheit]kürzlich hat tao zhexuan die mehrheit der internetnutzer und mathematikbegeisterten herausgefordert: können beliebte mathematikbegeisterte, beweisassistenten, automatisierte assistenten und ki ihre kräfte bündeln, um mathematische probleme zu beweisen, die sich um mehrere größenordnungen erstrecken?
möchten sie am von terence tao ins leben gerufenen mathematik-forschungsprojekt „crowdsourcing“ teilnehmen?die gelegenheit ist gekommen!ki-gestützte beweismathematische forschung wird immer machbarer
jeder von ihnen ist mit aspekten des projekts ausreichend vertraut, um die beiträge des anderen zu bestätigen.wenn sie jedoch größere mathematische forschungsprojekte organisieren möchten, insbesondere projekte mit öffentlichen beiträgen, ist dies viel schwieriger.der grund dafür ist, dass es schwierig ist, den beitrag aller zu überprüfen.ende 2023 gab terence tao bekannt, dass das lean4-projekt, das den beweis der polynomischen freiman-ruzsa-vermutung formalisierte, nach drei wochen erfolgreich war (das bild zeigt den aktuellen stand)bedenken sie, dass ein einzelner fehler in einem teil eines mathematischen arguments zum scheitern des gesamten projekts führen kann.darüber hinaus ist es angesichts der komplexität eines typischen mathematikprojekts unrealistisch, von der öffentlichkeit mit einem grundstudium in mathematik zu erwarten, dass sie sinnvolle beiträge leistet.daraus können wir auch erkennen, dass die einbindung von ki-tools in mathematische forschungsprojekte ebenfalls eine große herausforderung darstellt.da ki argumente generieren kann, die vernünftig erscheinen, aber tatsächlich keinen sinn ergeben, ist eine zusätzliche überprüfung erforderlich, bevor der von der ki generierte teil dem projekt hinzugefügt werden kann.glücklicherweise bieten beweisgestützte sprachen wie lean potenzielle möglichkeiten, diese hindernisse zu überwinden und die zusammenarbeit zwischen professionellen mathematikern, der breiten öffentlichkeit und ki-tools zu ermöglichen.dieser ansatz basiert auf der prämisse, dass projekte modular in kleinere teile zerlegt werden können, die abgeschlossen werden können, ohne das gesamte projekt verstehen zu müssen.aktuelle beispiele sind vor allem projekte, die bestehende mathematische ergebnisse formalisieren (wie die formalisierung der kürzlich von marton bewiesenen pfr-vermutung).diese formalisierungen erfolgen in erster linie durch crowdsourcing durch menschliche mitwirkende (darunter professionelle mathematiker und interessierte mitglieder der öffentlichkeit).gleichzeitig gibt es auch einige neue versuche, stärker automatisierte tools zur lösung der aufgabe einzuführen, darunter traditionelle automatische theorembeweiser und modernere ki-basierte tools.es wird möglich, neue mathematische probleme zu erforschen
und,terence taoes wird auch angenommen, dass dieses neue paradigma nicht nur zur formalisierung bestehender mathematik, sondern auch zur erforschung völlig neuer mathematik genutzt werden kann!in der vergangenheit organisierten er und sein nachfolger ein online-kooperationsprojekt „polymath“, das ein gutes beispiel ist.allerdings wurde bei diesem projekt keine beweis-hilfssprache in den arbeitsablauf integriert, und die beiträge mussten von menschlichen moderatoren verwaltet und überprüft werden, was sehr zeitaufwändig war und den weiteren ausbau dieser projekte einschränkte.nun hofft tao zhexuan, dass das hinzufügen einer beweishilfssprache diesen engpass beseitigen kann.sein besonderes interesse gilt der frage, ob es möglich ist, mit diesen modernen werkzeugen eine klasse mathematischer probleme gleichzeitig zu untersuchen, anstatt sich nur auf ein oder zwei probleme gleichzeitig zu konzentrieren.im wesentlichen ist dieser ansatz für sich wiederholende aufgaben modular aufgebaut, und crowdsourcing- und automatisierungstools können besonders nützlich sein, wenn eine plattform vorhanden ist, um alle beiträge streng zu koordinieren.ein solches mathematisches problem wäre mit früheren methoden nicht skalierbar gewesen. es sei denn, sie untersuchen über viele jahre hinweg langsam einen datenpunkt nach dem anderen anhand einzelner arbeiten, bis sie eine vernünftige vorstellung von dieser art von problem bekommen.darüber hinaus kann ein großer problemdatensatz dazu beitragen, leistungsbewertungen verschiedener automatisierungstools durchzuführen und die effizienz verschiedener arbeitsabläufe zu vergleichen.im juli dieses jahres wurde die fünfte busy beaver-nummer mit 47.176.870 bestätigt.einige frühere crowdsourcing-computing-projekte, wie z. b. great internet mersenne prime search (gimps), ähneln im geiste diesen projekten, verwenden jedoch einen traditionelleren proof-of-work-mechanismus, anstatt eine hilfssprache zu beweisen.terence tao sagte, es würde ihn interessieren, ob es weitere beispiele für crowdsourcing-projekte gibt, die mathematische räume erforschen, und ob daraus erkenntnisse gewonnen werden können, die genutzt werden können.tao zhexuan schlägt neue projekte vor
zu diesem zweck schlug tao selbst ein projekt vor, um dieses paradigma weiter zu testen.dieses projekt wurde von der mathoverflow-frage des letzten jahres inspiriert.bald darauf diskutierte tao zhexuan in seinem mathstodon weiter darüber.dieses problem gehört zum bereich der universellen algebra und beinhaltet eine mittelgroße untersuchung der theorie einfacher gleichungen der ursprünglichen gruppe (magma).die ursprüngliche gruppe ist eine gruppe, die mit binären operationen ausgestattet istdie menge g.anfänglich sind dieser operation o keine zusätzlichen axiome zugeordnet, sodass die ursprüngliche gruppe selbst eine relativ einfache struktur aufweist.durch das hinzufügen zusätzlicher axiome wie identitätsaxiome oder assoziativitätsaxiome können wir natürlich bekanntere mathematische objekte wie gruppen, halbgruppen oder monoide erhalten.hier interessieren uns die (konstantenfreien) axiome der gleichheit. diese axiome betreffen die gleichheit von ausdrücken, die aus operationen o und einer oder mehreren unbekannten variablen in g konstruiert werden.zwei bekannte beispiele für solche axiome sind das kommutativgesetz xoy = yox und das assoziativgesetz (xoy) oz = xo (yoz).wobei x, y, z unbekannte variablen in der ursprünglichen gruppe g sind.andererseits wird das (linke) identitätsaxiom eox = x hier nicht als gleichungsaxiom betrachtet, da es eine konstante e ∈ g beinhaltet. solche axiome mit konstanten werden in dieser studie nicht diskutiert.als nächstes stellte terence tao zur veranschaulichung des von ihm initiierten forschungsprojekts elf beispiele für gleichheitsaxiome über primitive gruppen vor.diese gleichheitsaxiome sind gleichungen, die nur primitive gruppenoperationen und unbekannte variablen beinhalten –so stellt beispielsweise gleichung 7 das kommutative axiom dar, während gleichung 10 das assoziative axiom darstellt.das konstante axiom gleichung 1 ist das stärkste, da es die ursprüngliche gruppe g auf höchstens ein element beschränkt. im gegensatz dazu ist das reflexive axiom gleichung 11 das schwächste und alle ursprünglichen gruppen erfüllen dieses axiom.als nächstes können wir die ableitungsbeziehung zwischen diesen axiomen untersuchen: welche axiome können welche axiome ableiten?beispielsweise führt gleichung 1 zu allen anderen axiomen in dieser liste, was wiederum zu gleichung 11 führt.gleichung 8 kann als sonderfall zur ableitung von gleichung 9 verwendet werden, die wiederum als sonderfall zur ableitung von gleichung 10 verwendet werden kann.die vollständige ableitungsbeziehung zwischen diesen axiomen kann durch das folgende hasse-diagramm beschrieben werden:dieses ergebnis beantwortet speziell eine frage auf der mathematik-q&a-website mathoverflow: gibt es gleichungsaxiome zwischen dem konstanten axiom (gleichung 1) und dem assoziativitätsaxiom (gleichung 10)?es ist erwähnenswert, dass die meisten implikationsbeziehungen hier leicht zu beweisen sind. es besteht jedoch eine nicht triviale implikationsbeziehung.diese beziehung wurde in einer antwort auf einen mathoverflow-beitrag gefunden, der eng mit der vorherigen frage zusammenhängt:satz 1: gleichung 4 impliziert gleichung 7beweis: angenommen, g erfüllt gleichung 4es gilt für alle x,y ∈ g.insbesondere wenn y = xox, folgt daraus, dass (xox) o (xox) = (xox) ox.wenn wir (1) erneut anwenden, können wir schlussfolgern, dass xox idempotent ist:wenn wir nun in (1) x durch xox ersetzen und (2) verwenden, erhalten wir (xox) oy = yo (xox).insbesondere sind xox und yoy austauschbar:darüber hinaus erhalten wir durch zweimaliges anwenden von (1) (xox) o (yoy) = (yoy) ox = xoy.daher kann (3) zu xoy = yox vereinfacht werden, was gleichung 7 entspricht.die formalisierung des obigen argumentationsprozesses findet sich in lean.es ist jedoch erwähnenswert, dass die allgemeine frage, ob ein satz von gleichheitsaxiomen einen anderen satz von gleichheitsaxiomen bestimmt, unentscheidbar ist.daher ist die situation hier etwas ähnlich wie bei der „busy beaver“-herausforderung, das heißt, ab einem bestimmten punkt der komplexität werden wir zwangsläufig auf unentscheidbare probleme stoßen, aber bevor wir diese schwelle erreichen, hoffen wir immer noch, interessante probleme und phänomene zu entdecken.das obige hass-diagramm bestätigt nicht nur die folgerungsbeziehungen zwischen den aufgeführten gleichheitsaxiomen, sondern auch die nicht-implikationsbeziehungen zwischen den axiomen.wie in der abbildung gezeigt, impliziert beispielsweise das kommutative axiom gleichung 7 nicht das axiom von gleichung 4 (x + x) + y = y + x.um dies zu beweisen, suchen sie einfach ein beispiel einer primitiven gruppe, die das kommutative axiom gleichung 7 erfüllt, aber nicht das axiom gleichung 4.in diesem fall können wir beispielsweise die natürliche zahlenmenge n wählen, deren operation xoy := x+y ist.allgemeiner gesagt bestätigt das diagramm die folgenden nicht-implikationsbeziehungen, die (zusammen mit den bereits erwähnten implikationsbeziehungen) den teilweise geordneten satz von implikationsbeziehungen zwischen diesen elf axiomen vollständig beschreiben:hier lädt tao zhexuan die leser ein, gegenbeispiele vorzuschlagen, um einige der beweise zu vervollständigen.das am schwierigsten zu findende gegenbeispiel ist, dass gleichung 9 gleichung 8 nicht ableiten kann.eine lösung kann mit lean gegeben werden.darüber hinaus stellt tao zhexuan auch ein github-repository bereit, das lean-beweise aller oben genannten inklusions- und anti-inklusionsbeziehungen enthält.es ist ersichtlich, dass allein die berechnung des haas-diagramms aus 11 gleichungen bereits etwas umständlich ist.das von terence tao vorgeschlagene projekt ist ein versuch, dieses hass-diagramm um mehrere größenordnungen zu erweitern, um einen größeren bereich von gleichungssätzen abzudecken.der von ihm vorgeschlagene satz war ε, der satz von gleichungen, der die ursprüngliche gruppenoperation o höchstens viermal verwendete, bis die axiome der reflexivität und symmetrie der summengleichungen neu benannt wurden.dazu gehören die oben genannten elf gleichungen, aber es gibt noch viele weitere.denken sie daran, dass die katalanische zahl c_n die anzahl der möglichkeiten ist, einen ausdruck mit der binäroperation o zu bilden (angewandt auf n+1 platzhaltervariablen), und dass die bell-zahl b_m bei einer zeichenfolge von m platzhaltervariablen die anzahl der möglichkeiten ist, die diese variablen haben zugewiesene namen (die umbenennt werden können), wodurch bestimmten platzhaltern derselbe name zugewiesen werden kann.daher beträgt die anzahl der gleichungen, die höchstens vier operationen umfassen, wenn man die symmetrie außer acht lässtdie anzahl der gleichungen, deren linke und rechte seite gleich sind, beträgtdiese entsprechen den reflexiven axiomen (gleichung 11).die verbleibenden 9118 gleichungen erscheinen aufgrund der symmetrie der gleichungen paarweise, sodass die gesamtgröße von ε beträgt
tao zhexuan sagte, dass er noch keine vollständige liste solcher identitäten erstellt habe, aber er vermutet, dass dies mit python leicht zu bewerkstelligen sei.mithilfe von ki-tools sollten sie in der lage sein, den größten teil des erforderlichen codes zu generieren.er sagte, er habe keine ahnung, wie die geometrie von ε aussehen würde.werden die meisten gleichungen nicht miteinander vergleichbar sein? wird es in „starke“ axiome und „schwache“ axiome unterteilt?mittlerweile gibt es im nachrichtenbereich von terence tao dutzende kommentare.interessierte leser, tao zhexuan hat auch eine einladung an sie gerichtet.
