Werbung: Hier kannst du 30 Tage kostenlos alles ausprobieren, was Brilliant zu bieten hat: brilliant.org/DorFuchs. Außerdem gibt es über den Link 20 % Rabatt auf ein jährliches Premium-Abonnement.
Ich hatte Brilliant auch mal für ein paar Monate wegen dem amerikanischen UA-camr Blackpenredpen. Ich muss zugeben, dass ich nicht viel durch die App gelernt habe. Ich finde durch normale UA-cam Videos lernt man mehr und deswegen war es mir das Geld nicht wert. Trotzdem cool, dass du eine K ooperation mit einem so großen Anbieter machen kannst.
Es wäre super cool wenn du ein Video über Lean, also wie es funktioniert und was dahinter steckt, machen könntest. Als Nichtmathematiker ist es nahezu unmöglich zu verstehen, was da passiert und wie es abläuft. Gleiches gilt auch für den Risch-Algorithmus, der ist vermutlich sogar leichter zu erklären.
Mittlerweile halte ich es für wahrscheinlicher, dass zu meinen Lebzeiten eine KI die Riemann Hypothese und viele Weitere beweist, als dass das ein Mensch schafft. Edit nachdem ich das Video durchgeschaut habe: Witzig, dass du selber auch Riemann erwähnst. Ich würde auch mein Statement dahingehend anpassen, dass vielleicht ein Mensch die Hypothese beweisen wird, aber mit starker Hilfe solcher Modelle. Kreativität ist vielleicht schwer zu simulieren, aber Mathe ist genau wie Programmierung streng logisch, folgt exakten Regeln und wäre damit ideal für Computer, daher könnte ich mir schon gut vorstellen, dass man in ein paar Jahrzehnten große Teile der Informatik und Mathematik "durchgespielt" hat. Und ich geh mir dann einen neuen Job suchen. :D
Es sei anzumerken, dass Lean einfach die größte Mathematikbibliothek hat und deshalb für die Mathematik vielleicht der fortgeschritteste Beweisassistent ist. Von der darutnerliegenden Theorie ist Lean eigentlich nicht fortgeschrittener als andere Beweisassistenten.
11:30 Wo du schon auf diesen Punkt hinweist ... man hätte denken können, dass die Leute sich heimlich Hilfe von der KI geholt haben. Zumindest Nordkorea wurde schon mal wegen Betrugsversuch qualifiziert und sah sich öfter dem Verdacht ausgesetzt, zum Beispiel weil die Schüler ungewöhnlich lange auf Toilette waren. Aber wenn die KI mehrere Tage an manchen Problemen gesessen hat, scheidet diese Abkürzung wohl derzeit zumindest noch aus. Interessant ist, dass die KI nur 0 oder 7 Punkte auf Aufgaben erhalten hat. Schüler schreiben ja manchmal noch Lösungsansätze hin, auf die es Punkte gibt. Ebenso gibt der ChatBot mir regelmäßig halbrichtige Antworten auf meine Fragen.
@@pamesankaese "nicht nur" und das stimmt auf jeden Fall. Es gibt einen großen Schnitt an Berufen die einem recht gut gefallen und in denen man einigemaßen gut verdient denke ich
Ist nur eine Frage der Zeit, bis der Fortschritt in KI auch die Robotik revolutioniert (was in Ansätzen auch bereits der Fall ist, siehe Figure 01, NVIDIA Dr. Eureka, etc.). Aber eine Handwerksausbildung kann uns aktuell vielleicht noch ein paar Jahre Zeit erkaufen :D
Super-Video, vielen Dank! Mit der Prognose am Ende wäre ich aber vorsichtig. Wenn es um reine Menge geht, also z.B. Schülerwissen vs. globales Wissen, sind Computer in ihrem Element. Diese Art von Grenzen zu überwinden sollte nur wenige Jahre benötigen - wenn überhaupt. Die Frage ist für mich eher, ob es noch prinzipielle Grenzen gibt. Können die beiden fehlenden Lösungen in einer neuen Instanz ein paar Tage später schon mitgelöst werden? Dann könnte eine selbst den besten Menschen in aller Regel überlegene KI nur noch Monate entfernt sein, und dann wird es auch neue Erkenntnisse hageln. Man wird sehen.
Es wäre ein leichtes, die Lösungen der beiden fehlenden Aufgaben den Trainingsdaten hinzuzufügen. Die Lösungsfähigkeiten des Lösers hätte man damit aber noch nicht wesentlich erweitert.
Klasse informatives Video! Ich hätte eine Frage: Wenn ich das Diagramm zur Verteilung der Auszeichnungen bei der IMO richtig verstehe (es ist gerade schon nach 0:30 Uhr): Warum gab es für den gleichen Punktwert manchmal eine "ehrende Erwähnung" und manchmal ein "Nichts"? Lustig finde ich (ich habe selbst einen kleinen Mathe-Olympioniken zu hause), dass das Training der menschlichen Teilnehmer*innen auch so funktioniert, dass sie ganz viele bekannte Olympiade-Aufgaben lösen und mit diesem Wissen dann auf neue Aufgaben im Wettbewerb losgelassen werden. Wirklich interessant wäre es, wenn man zeigen könnte, dass sich mit diesem Vorgehen (egal ob von einer künstlichen oder menschlichen Intelligenz) tatsächlich ein noch ungelöstes Problem lösen lässt oder vielleicht auch nur ein bekanntes Problem auf eine bisher unbekannte Art und Weise lösen lässt.
Die Medaillen werden nicht anhand fester Punktgrenzen vergeben. Soweit ich weiß, werden die Schüler der Reihe nach anhand der Punkte sortiert und dann bekommt 1/12 eine Goldmedaille, 1/6 eine Silbermedaille und 1/4 eine Bronzemedaille.
kleine Kritik: Das Beispiel bei 16:00 ist schon ein wenig schlecht. Bei dem Beispiel zählt die KI einfach Brute Force durch und benutzt keine Algebra. Ist ja nicht der Sinn der Aufgabe.
@the_master_of_cramp Ich stimme dir zu. Ich war bei der Verkündung, dass Numina gewonnen hat, dabei und auch dort kam als Beispiel eine Abzählfrage, welche mit einem Loop/Brute-Force gelöst worden ist.
Mal so als Videoidee, falls du (/man) dahingehend über eine Prognose stellen kann: Inwiefern wird AI in Zukunft Einfluss auf mathematische Forschung haben und werden Mathematiker mit der Zeit tendentiell obsolet -> zwar nicht ganz, aber sodass gewisse Gruppen oder Massen von Mathematikern "abgelöst" werden?
Es gab schon Leute, die glaubten, dass Mathematiker durch Mathematica und Maple überflüssig werden würden. Wie wir heute wissen, ist das nicht eingetreten.
Der Teil der Übersetzung von natürlicher Sprache in formale Sprache ist derjenige, der sich nicht maschinell überprüfen lässt. Der ist bei Matheolympia-Aufgaben wichtig, entfällt aber bei Forschungsaufgaben, denn ein Mathematiker sollte sein Forschungsproblem selbst korrekt formalisieren können. Übersetzung in formale Sprache, heißt auch nicht weniger, als die Aufgabe richtig zu verstehen. Wie oft ist es mir bei MO-Aufgaben passiert, dass ich gedacht habe, die Lösung ist aber ganz einfach. Aber wenn die Lösung zu einfach ist, hat man die Aufgabe sicher nicht richtig verstanden.
Beweisassistenten werden vielleicht in Zukunft so etwa wie LaTeX ein Hilfsmittel, was alle Mathematiker verwenden. Also mach einen Einsteiger-Kurs in Lean, falls es das irgendwo gibt, oder arbeite die von der Lean-Community empfohlenen Materialien zum Einstieg durch und dann mach einfach die Mathematik, die dich interessiert und formalisiere in dem Bereich. (Alles geschrieben von jemandem, der selbst noch nie einen formalen Beweis geschrieben hat!)
@@DorFuchs da freue ich mich sehr drauf. Ich habe mal ein wenig elementare Gruppeneigenschaften mit einem Beweisassistenten bewiesen. Das wird in der Zukunft sicher hilfreich und zeitsparend in peer-reviews sein.
Gibt auch einiges an Lean Content auf UA-cam. Und gibt auch ein paar interaktive Einführungen auf dem "Lean Game Server" (findet man per Google). Aber gibt auch paar gute Guides auf der Lean Website. Und auf dem Lean Zulip Chat kriegt man bei Fragen auch leicht Hilfe. Module in die Richtung, vor allem zur Entwicklung/Forschung von Beweisassistenten, statt sie einfach nur zu verwenden, gibt es vermutlich an den meisten Unis noch eher wenig. An der TU München gibt es den Informatik Lehrstuhl für Logic and Verification, die Entwickeln Isabelle, ein anderer bekannter Beweisassistent, da gibt es auf jeden Fall ein paar Module dazu. Gibt aber auch anderswo Professoren, die Lean benutzen oder vllt. sogar selbst mit Entwickeln und da geben sicher auch manche Module, bei denen das zumindest angeschnitten wird. Sonst sind generell sicher Module in Richtung Logik/Formalisierung/Verifikation und generell sowas wie funktionale Programmierung relevant. Zumindest bei Lean kann man glaub ich aber auch vergleichsweise einfach so mitmachen. Das ist ja alles öffentlich auf GitHub bzw. die Kommunikation auf Zulip.
@@Leo-io4bq "Mathematics in Lean" ist eine schöne Schritt-für-Schritt-Anleitung, die die einzelnen mathematischen Grunddisziplinen anhand von selbst nachzuturnenden Beispielen abarbeitet.
Wenn ich das richtig verstanden habe, ist das so. Ein informelles Problem wird von der KI formalisiert und zwar mehrfach (so ähnlich wie bei den Antworten von Chatgpt komm aucht hier halt jedes mal etwas anderes raus). Da kann nämlich einiges schiefgehen. Am Ende wird einfach alles akzeptiert, was typkorrekt ist, also wo sowohl die Aussage als auch der Beweis stimmt. Natürlich kann es sein, dass die Aussage beim Formalisieren verändert wurde. Das ist aber für die Trainingsdaten kein Problem. Fürs Trainieren braucht man nur korrekte Aussagen mitsamt Beweisen.
@@Hustler1256 Das haben Leute auch schon nach dem Erscheinen von Mathematica und Maple vor Jahrzehnten behauptet. Das Problem mit Mathematik in der Praxis ist, dass Leute mit Halbwissen halbgare Lösungen für Probleme entwickeln, was aber keinem auffällt, weil die Abnehmer auch Mathematikphobiker sind. Und Chatbots sind gerade bei halbgaren Lösungen führend, weil sie ihre Lösungsvorschläge eben nicht verstehen.
@ das ist logisches Denken mein Lieber . Quantencomputer können schon jetzt das , was Mathematiker nicht können. Ist nur nh Frage der Zeit , bleib realistisch .
Das ist sehr interessant, allerdings auch unschön für alle, die gerade Mathematik studieren. Da wird sich in den kommenden Jahren nochmal ordentlich etwas ändern. :D
Nenne mir einen Studiengang bei denen das nicht der Fall ist... Informatik, Jura, BWL... Bis auf die Bereiche wo auch ein "Handwerklicher Teil" dabei ist wie Medizin fragen sich alle in welche Richtung es gehen wird.
naja ich finde mathematik als olympia sehr trauig.. es ist zwar keine wissenschaft und kann somit sehr gut zu sport dazugezählt werden aber mathematik ist dann doch ein bisschen wichtiger als tischtennis und schwimmen im frei stil finde ich persöhnlich
Ja, das hab ich gerade erst gemerkt, als ich mir das Video nach der Veröffentlichung nochmal angesehen habe. LEAN ist halt kein "Beweis-Finder" in dem Sinne, dass hier Beweise nicht automatisch generiert werden, sondern "nur" gegebene Beweise auf Korrektheit geprüft werden. Deswegen wollte ich das nochmal anders formulieren. Aber dann hab ich auch etwas schneller als sonst das Video gerendert und abgeschlossen, weil ich Brilliant versprochen hatte, noch diesen Monat zu veröffentlichen. 😅
Dass Deutschland nicht mal in den Top 12 bei den Länderergebnissen bei der 65. IMO ist, finde ich etwas schade. Das sollte meiner Meinung nach mehr gefördert werden
Hallo, danke für deinen Beitrag. Eine kleine Ergänzung: In den vergangenen Jahren hat Deutschland die Plätze 20, 7 und 12 belegt und auch in diesem Jahr haben alle sechs Teilnehmenden eine Medaille gewonnen - wenn auch leider keine goldene.
Das ist für ein Land mit vergleichsweise wenig Einwohnern nicht so einfach zu erreichen. Zudem sollte man sich auch die Frage stellen, ob man Zustände wie z.B. in China haben will. Klar, besser geht immer, aber schlecht ist das Ergebnis nicht.
@@leichter5865natürlich will man keine Verhältnisse wie in China, aber auch europäische Länder wie England (7. Platz), Italien, Frankreich etc. mit ähnlichen Verhältnissen haben besser als Deutschland (31. Platz) abgeschnitten und das obwohl Deutschland 20 Mio Einwohner mehr hat. Meiner Meinung nach liegt es nicht an den Menschen, die sind genauso intelligent wie die anderen, sondern am System. Man sollte früher Begabungen entdecken und fördern. Dies erfordert Änderungen im Schulsystem. Das Ergebnis ist nicht schlecht, aber wie man an den anderen europäischen Ländern sieht, gibt es Verbesserungsbedarf in Deutschland (das sollte auch keine Kritik an den 6 Kandidaten sein, die ihr bestes gegeben haben und Respekt und Anerkennung verdienen)
@@sieskilltkeinw582 Ich würde als deutscher Einwohner gerne wissen wie man sich dafür vorbereitet. Bei mir in der Schule ist es einfach: "Achso du willst bei der Mathe-Olympiade mitmachen? Ich melde dich an" und das wars dann auch
ChatGPT ist auch ein LLM und keine KI, die für physikalisches/mathematisches Verständnis trainiert wurde. Das ist so, als würdest du sagen: "Mein Lamborghini versagt im Offroad aber vollständig." Ja no s**t Sherlock!
Also ohne da jetzt weiter dran zu überlegen würde ich ja spontan sagen, die Lösung von Aufgabe 5 ist 3: In der ersten und letzten Zeile gibt es kein Monster. Strategie: In der zweiten Zeile durchgehen, bis man auf das Monster trifft. Dann das Monster entweder links oder rechts herum umgehen (1. Zeile hat kein Monster, 2. Zeile hat kein weiteres Monster und 3. Zeile kann das Monster nur entweder beim Weg rechts oder links um das Monster herum haben). Dann einfach in der Spalte mit dem Monster in der 2. Zeile bis nach unten durchkriechen. Edit: und natürlich habe ich den Randfall nicht betrachtet, was passiert, wenn das Monster in der zweiten Zeile sich ganz außen befindet. oof.
Ach Mann, ich wollte Mathematiker werden und ggf. in die Forschung gehen, aber bis ich fertig mit meinem Studium, haben KI's wahrscheinlich schon den Menschen übertrumpft. 😢 Dann werde ich halt Patty Flipper bei MC'es.
Werbung: Hier kannst du 30 Tage kostenlos alles ausprobieren, was Brilliant zu bieten hat: brilliant.org/DorFuchs. Außerdem gibt es über den Link 20 % Rabatt auf ein jährliches Premium-Abonnement.
Ich hatte Brilliant auch mal für ein paar Monate wegen dem amerikanischen UA-camr Blackpenredpen. Ich muss zugeben, dass ich nicht viel durch die App gelernt habe. Ich finde durch normale UA-cam Videos lernt man mehr und deswegen war es mir das Geld nicht wert.
Trotzdem cool, dass du eine K ooperation mit einem so großen Anbieter machen kannst.
Respekt an Dorfuchs, dass er nach seinem letzn langen Video so schnell ein neues gemacht hat, mach weiter so!
Es wäre super cool wenn du ein Video über Lean, also wie es funktioniert und was dahinter steckt, machen könntest. Als Nichtmathematiker ist es nahezu unmöglich zu verstehen, was da passiert und wie es abläuft. Gleiches gilt auch für den Risch-Algorithmus, der ist vermutlich sogar leichter zu erklären.
Bei Lean kannst du einfach auf die Packungsbeilage schauen 👍🏼
Hier kann man übrigens den Math Olympiad Solver von Numina ausprobieren: huggingface.co/spaces/AI-MO/math-olympiad-solver
Mittlerweile halte ich es für wahrscheinlicher, dass zu meinen Lebzeiten eine KI die Riemann Hypothese und viele Weitere beweist, als dass das ein Mensch schafft.
Edit nachdem ich das Video durchgeschaut habe: Witzig, dass du selber auch Riemann erwähnst. Ich würde auch mein Statement dahingehend anpassen, dass vielleicht ein Mensch die Hypothese beweisen wird, aber mit starker Hilfe solcher Modelle. Kreativität ist vielleicht schwer zu simulieren, aber Mathe ist genau wie Programmierung streng logisch, folgt exakten Regeln und wäre damit ideal für Computer, daher könnte ich mir schon gut vorstellen, dass man in ein paar Jahrzehnten große Teile der Informatik und Mathematik "durchgespielt" hat. Und ich geh mir dann einen neuen Job suchen. :D
5:28 Schnittfehler? :D
Es sei anzumerken, dass Lean einfach die größte Mathematikbibliothek hat und deshalb für die Mathematik vielleicht der fortgeschritteste Beweisassistent ist. Von der darutnerliegenden Theorie ist Lean eigentlich nicht fortgeschrittener als andere Beweisassistenten.
11:30 Wo du schon auf diesen Punkt hinweist ... man hätte denken können, dass die Leute sich heimlich Hilfe von der KI geholt haben. Zumindest Nordkorea wurde schon mal wegen Betrugsversuch qualifiziert und sah sich öfter dem Verdacht ausgesetzt, zum Beispiel weil die Schüler ungewöhnlich lange auf Toilette waren. Aber wenn die KI mehrere Tage an manchen Problemen gesessen hat, scheidet diese Abkürzung wohl derzeit zumindest noch aus.
Interessant ist, dass die KI nur 0 oder 7 Punkte auf Aufgaben erhalten hat. Schüler schreiben ja manchmal noch Lösungsansätze hin, auf die es Punkte gibt. Ebenso gibt der ChatBot mir regelmäßig halbrichtige Antworten auf meine Fragen.
Handwerkausbildung ich komme👍
@pafu015in einer idealen Fantasiewelt vielleicht. Die Realität sieht für die meisten anders aus.
@@pamesankaese "nicht nur" und das stimmt auf jeden Fall. Es gibt einen großen Schnitt an Berufen die einem recht gut gefallen und in denen man einigemaßen gut verdient denke ich
Hab ich mir nach meinen Mathestudium auch gedacht 😂
Ist nur eine Frage der Zeit, bis der Fortschritt in KI auch die Robotik revolutioniert (was in Ansätzen auch bereits der Fall ist, siehe Figure 01, NVIDIA Dr. Eureka, etc.). Aber eine Handwerksausbildung kann uns aktuell vielleicht noch ein paar Jahre Zeit erkaufen :D
@@tannenbaumxy Also was soll man dann überhaupt noch arbeiten in Zukunft?
Spannendes Video!
Super-Video, vielen Dank! Mit der Prognose am Ende wäre ich aber vorsichtig. Wenn es um reine Menge geht, also z.B. Schülerwissen vs. globales Wissen, sind Computer in ihrem Element. Diese Art von Grenzen zu überwinden sollte nur wenige Jahre benötigen - wenn überhaupt. Die Frage ist für mich eher, ob es noch prinzipielle Grenzen gibt. Können die beiden fehlenden Lösungen in einer neuen Instanz ein paar Tage später schon mitgelöst werden? Dann könnte eine selbst den besten Menschen in aller Regel überlegene KI nur noch Monate entfernt sein, und dann wird es auch neue Erkenntnisse hageln. Man wird sehen.
Es wäre ein leichtes, die Lösungen der beiden fehlenden Aufgaben den Trainingsdaten hinzuzufügen. Die Lösungsfähigkeiten des Lösers hätte man damit aber noch nicht wesentlich erweitert.
einfach mal bei 5:30 den Cut vergessen ;)
Neues DorFuchs Video. Perfekter Start in den Tag 😊
Es ist fast 2 Uhr 😳
Klasse informatives Video! Ich hätte eine Frage: Wenn ich das Diagramm zur Verteilung der Auszeichnungen bei der IMO richtig verstehe (es ist gerade schon nach 0:30 Uhr):
Warum gab es für den gleichen Punktwert manchmal eine "ehrende Erwähnung" und manchmal ein "Nichts"?
Lustig finde ich (ich habe selbst einen kleinen Mathe-Olympioniken zu hause), dass das Training der menschlichen Teilnehmer*innen auch so funktioniert, dass sie ganz viele bekannte Olympiade-Aufgaben lösen und mit diesem Wissen dann auf neue Aufgaben im Wettbewerb losgelassen werden. Wirklich interessant wäre es, wenn man zeigen könnte, dass sich mit diesem Vorgehen (egal ob von einer künstlichen oder menschlichen Intelligenz) tatsächlich ein noch ungelöstes Problem lösen lässt oder vielleicht auch nur ein bekanntes Problem auf eine bisher unbekannte Art und Weise lösen lässt.
Eine ehrende Erwähnung erhalten alle, die keine Medaille gewonnen haben, aber eine Aufgabe komplett richtig lösen konnten.
Die Medaillen werden nicht anhand fester Punktgrenzen vergeben. Soweit ich weiß, werden die Schüler der Reihe nach anhand der Punkte sortiert und dann bekommt 1/12 eine Goldmedaille, 1/6 eine Silbermedaille und 1/4 eine Bronzemedaille.
Kann man eigentlich das Shirt was du anhast kaufen? Konnte es im Shop nicht finden
5:20 Lean ist nicht mehr nur bei Rappern beliebt, sondern hat auch die Mathematikszene erobert! Wer hätte das gedacht! 😂
Ich bin also nicht der Einzige der immer erst an lila Saft denkt...
kleine Kritik: Das Beispiel bei 16:00 ist schon ein wenig schlecht.
Bei dem Beispiel zählt die KI einfach Brute Force durch und benutzt keine Algebra. Ist ja nicht der Sinn der Aufgabe.
@the_master_of_cramp Ich stimme dir zu. Ich war bei der Verkündung, dass Numina gewonnen hat, dabei und auch dort kam als Beispiel eine Abzählfrage, welche mit einem Loop/Brute-Force gelöst worden ist.
Mal so als Videoidee, falls du (/man) dahingehend über eine Prognose stellen kann:
Inwiefern wird AI in Zukunft Einfluss auf mathematische Forschung haben und werden Mathematiker mit der Zeit tendentiell obsolet -> zwar nicht ganz, aber sodass gewisse Gruppen oder Massen von Mathematikern "abgelöst" werden?
Es gab schon Leute, die glaubten, dass Mathematiker durch Mathematica und Maple überflüssig werden würden. Wie wir heute wissen, ist das nicht eingetreten.
Ob Ki bald mathematische Probleme lösen kann? Ich freue mich jedenfalls schon auf die Formel für Primzahlen :D
Der Teil der Übersetzung von natürlicher Sprache in formale Sprache ist derjenige, der sich nicht maschinell überprüfen lässt. Der ist bei Matheolympia-Aufgaben wichtig, entfällt aber bei Forschungsaufgaben, denn ein Mathematiker sollte sein Forschungsproblem selbst korrekt formalisieren können.
Übersetzung in formale Sprache, heißt auch nicht weniger, als die Aufgabe richtig zu verstehen. Wie oft ist es mir bei MO-Aufgaben passiert, dass ich gedacht habe, die Lösung ist aber ganz einfach. Aber wenn die Lösung zu einfach ist, hat man die Aufgabe sicher nicht richtig verstanden.
Kennt einer von euch eine gute KI für Chemie?
AlphaFold
Beweisassistenten finde ich sehr interessant. Welche Module sollte man belegen, um zukünftig an ihnen forschen zu können?
Beweisassistenten werden vielleicht in Zukunft so etwa wie LaTeX ein Hilfsmittel, was alle Mathematiker verwenden.
Also mach einen Einsteiger-Kurs in Lean, falls es das irgendwo gibt, oder arbeite die von der Lean-Community empfohlenen Materialien zum Einstieg durch und dann mach einfach die Mathematik, die dich interessiert und formalisiere in dem Bereich.
(Alles geschrieben von jemandem, der selbst noch nie einen formalen Beweis geschrieben hat!)
@@DorFuchs da freue ich mich sehr drauf. Ich habe mal ein wenig elementare Gruppeneigenschaften mit einem Beweisassistenten bewiesen.
Das wird in der Zukunft sicher hilfreich und zeitsparend in peer-reviews sein.
Gibt auch einiges an Lean Content auf UA-cam. Und gibt auch ein paar interaktive Einführungen auf dem "Lean Game Server" (findet man per Google). Aber gibt auch paar gute Guides auf der Lean Website. Und auf dem Lean Zulip Chat kriegt man bei Fragen auch leicht Hilfe.
Module in die Richtung, vor allem zur Entwicklung/Forschung von Beweisassistenten, statt sie einfach nur zu verwenden, gibt es vermutlich an den meisten Unis noch eher wenig. An der TU München gibt es den Informatik Lehrstuhl für Logic and Verification, die Entwickeln Isabelle, ein anderer bekannter Beweisassistent, da gibt es auf jeden Fall ein paar Module dazu. Gibt aber auch anderswo Professoren, die Lean benutzen oder vllt. sogar selbst mit Entwickeln und da geben sicher auch manche Module, bei denen das zumindest angeschnitten wird.
Sonst sind generell sicher Module in Richtung Logik/Formalisierung/Verifikation und generell sowas wie funktionale Programmierung relevant.
Zumindest bei Lean kann man glaub ich aber auch vergleichsweise einfach so mitmachen. Das ist ja alles öffentlich auf GitHub bzw. die Kommunikation auf Zulip.
Wenn man an Beweisassistenten forschen will, muss man in die Programmiersprachenforschung gehen.
@@Leo-io4bq "Mathematics in Lean" ist eine schöne Schritt-für-Schritt-Anleitung, die die einzelnen mathematischen Grunddisziplinen anhand von selbst nachzuturnenden Beispielen abarbeitet.
Wie ham die es hingekriegt aus den 1M informal problems die 100M formal problems zu machen, also warum sind das so viel mehr?
Wenn ich das richtig verstanden habe, ist das so. Ein informelles Problem wird von der KI formalisiert und zwar mehrfach (so ähnlich wie bei den Antworten von Chatgpt komm aucht hier halt jedes mal etwas anderes raus). Da kann nämlich einiges schiefgehen. Am Ende wird einfach alles akzeptiert, was typkorrekt ist, also wo sowohl die Aussage als auch der Beweis stimmt. Natürlich kann es sein, dass die Aussage beim Formalisieren verändert wurde. Das ist aber für die Trainingsdaten kein Problem. Fürs Trainieren braucht man nur korrekte Aussagen mitsamt Beweisen.
11:30
Naja, hätte man den Computer 100x Rechenleistung gegeben, dann hätte er es auch im offiziellen Zeitrahmen geschafft.
Eine Olympiade ist ein Zeitraum, kein Wettbewerb.
KI wird die Mathematiker definitiv ersetzen steht schon mal fest .
Vielleicht zeigen die Erfolge der KI-Löser auch nur, dass die heutigen Matheolympiaaufgaben nicht mehr wirklich neu sind.
@ mal abgesehen von Olympia Aufgaben . Die Berufsfelder der Mathematiker werden Stück für Stück verschwinden
@@Hustler1256 Das haben Leute auch schon nach dem Erscheinen von Mathematica und Maple vor Jahrzehnten behauptet. Das Problem mit Mathematik in der Praxis ist, dass Leute mit Halbwissen halbgare Lösungen für Probleme entwickeln, was aber keinem auffällt, weil die Abnehmer auch Mathematikphobiker sind. Und Chatbots sind gerade bei halbgaren Lösungen führend, weil sie ihre Lösungsvorschläge eben nicht verstehen.
@ das ist logisches Denken mein Lieber . Quantencomputer können schon jetzt das , was Mathematiker nicht können. Ist nur nh Frage der Zeit , bleib realistisch .
@ übrigens kann ich dir das als VWLer getrost mitgeben ;)
[10:35] ".. also -- Absolute Maschine, der Typ! ..." ---- Eben nicht! ;-)))))
Das eigentliche Problem bei IMO ist, geeignete Aufgaben zu finden.
Oha
Das ist sehr interessant, allerdings auch unschön für alle, die gerade Mathematik studieren. Da wird sich in den kommenden Jahren nochmal ordentlich etwas ändern. :D
Nenne mir einen Studiengang bei denen das nicht der Fall ist... Informatik, Jura, BWL... Bis auf die Bereiche wo auch ein "Handwerklicher Teil" dabei ist wie Medizin fragen sich alle in welche Richtung es gehen wird.
Nö, noch kann die AI nichts neues erfinden. Es werden nur unterqualifizierte Fachkräfte ausgemistet, deren Existenz auf bestehenden Wissen basiert.
Bisher sind das ja nur die Schulmathematikaufgaben.
Internationale Matheolympiade hat nichts mit Schulmathe zutun.
@@ValentinMorio Gerade in der Medizin wird es einen gigantischen Umbruch geben
naja ich finde mathematik als olympia sehr trauig.. es ist zwar keine wissenschaft und kann somit sehr gut zu sport dazugezählt werden aber mathematik ist dann doch ein bisschen wichtiger als tischtennis und schwimmen im frei stil finde ich persöhnlich
Soll ich doch kunst studieren
5:16 kleiner editing fehler
Ja, das hab ich gerade erst gemerkt, als ich mir das Video nach der Veröffentlichung nochmal angesehen habe. LEAN ist halt kein "Beweis-Finder" in dem Sinne, dass hier Beweise nicht automatisch generiert werden, sondern "nur" gegebene Beweise auf Korrektheit geprüft werden. Deswegen wollte ich das nochmal anders formulieren.
Aber dann hab ich auch etwas schneller als sonst das Video gerendert und abgeschlossen, weil ich Brilliant versprochen hatte, noch diesen Monat zu veröffentlichen. 😅
@@DorFuchs Auf den letzten Drücker haha
Ich habe den Schnitt nun noch nach dem Veröffentlichen per UA-cam-Editor machen können.
@@DorFuchs Deswegen hatte ich auch den Kommentar geschrieben, hatte mal davon gehört das man so kleine Dinge auch im Nachhinein bearbeiten kann :)
Dass Deutschland nicht mal in den Top 12 bei den Länderergebnissen bei der 65. IMO ist, finde ich etwas schade. Das sollte meiner Meinung nach mehr gefördert werden
Hallo, danke für deinen Beitrag. Eine kleine Ergänzung: In den vergangenen Jahren hat Deutschland die Plätze 20, 7 und 12 belegt und auch in diesem Jahr haben alle sechs Teilnehmenden eine Medaille gewonnen - wenn auch leider keine goldene.
Das ist für ein Land mit vergleichsweise wenig Einwohnern nicht so einfach zu erreichen. Zudem sollte man sich auch die Frage stellen, ob man Zustände wie z.B. in China haben will. Klar, besser geht immer, aber schlecht ist das Ergebnis nicht.
@@leichter5865natürlich will man keine Verhältnisse wie in China, aber auch europäische Länder wie England (7. Platz), Italien, Frankreich etc. mit ähnlichen Verhältnissen haben besser als Deutschland (31. Platz) abgeschnitten und das obwohl Deutschland 20 Mio Einwohner mehr hat. Meiner Meinung nach liegt es nicht an den Menschen, die sind genauso intelligent wie die anderen, sondern am System. Man sollte früher Begabungen entdecken und fördern. Dies erfordert Änderungen im Schulsystem. Das Ergebnis ist nicht schlecht, aber wie man an den anderen europäischen Ländern sieht, gibt es Verbesserungsbedarf in Deutschland (das sollte auch keine Kritik an den 6 Kandidaten sein, die ihr bestes gegeben haben und Respekt und Anerkennung verdienen)
@@sieskilltkeinw582 Ich würde als deutscher Einwohner gerne wissen wie man sich dafür vorbereitet. Bei mir in der Schule ist es einfach: "Achso du willst bei der Mathe-Olympiade mitmachen? Ich melde dich an" und das wars dann auch
@@BirdsAreVeryCoolist das in anderen Ländern anders?
Und wann kann sie Bots aus den Comments löschen?
Gute Frage. Die zwei, die ich unter diesem Video sah, habe ich manuell gelöscht und auf dem Kanal ausgeblendet.
Ja, aber es gibt auch klare Lösungswege für diese Aufgaben, die mehr oder weniger kompliziert sind. Mathematische Kreativität ist noch etwas anderes.
Bei meinen Höma und Physik Aufgaben versagt Chatgbt vollständig 😂
ChatGPT ist auch ein LLM und keine KI, die für physikalisches/mathematisches Verständnis trainiert wurde. Das ist so, als würdest du sagen: "Mein Lamborghini versagt im Offroad aber vollständig." Ja no s**t Sherlock!
Man sollte eine ki ungelöste Probleme machen lassen
Die Lösungen sind meistens nicht zielführend weil ki’s auf bereits vorhandenen daten trainiert wird. Aber in Zukunft sieht es womöglich anders aus.
cool ein computer der rechnen kann :) das wir das noch erleben dürfen
Shi Haojia liebe Freunde wurde dieses Jahr 16 Jahre alt. Die Wunderkinder
Also ohne da jetzt weiter dran zu überlegen würde ich ja spontan sagen, die Lösung von Aufgabe 5 ist 3:
In der ersten und letzten Zeile gibt es kein Monster. Strategie: In der zweiten Zeile durchgehen, bis man auf das Monster trifft. Dann das Monster entweder links oder rechts herum umgehen (1. Zeile hat kein Monster, 2. Zeile hat kein weiteres Monster und 3. Zeile kann das Monster nur entweder beim Weg rechts oder links um das Monster herum haben). Dann einfach in der Spalte mit dem Monster in der 2. Zeile bis nach unten durchkriechen.
Edit: und natürlich habe ich den Randfall nicht betrachtet, was passiert, wenn das Monster in der zweiten Zeile sich ganz außen befindet. oof.
Ach Mann, ich wollte Mathematiker werden und ggf. in die Forschung gehen, aber bis ich fertig mit meinem Studium, haben KI's wahrscheinlich schon den Menschen übertrumpft. 😢
Dann werde ich halt Patty Flipper bei MC'es.
@@mr.austria8041 Dann werde ich halt UA-camr 🙃