Startseite
Forum
Fragen
Suchen
Formeleditor
Über Uns
Registrieren
Login
FAQ
Suchen
Foren-Übersicht
->
Sonstiges
Antwort schreiben
Benutzername
(du bist
nicht
eingeloggt!)
Titel
Nachrichtentext
Smilies
Weitere Smilies ansehen
Schriftfarbe:
Standard
Dunkelrot
Rot
Orange
Braun
Gelb
Grün
Oliv
Cyan
Blau
Dunkelblau
Indigo
Violett
Weiß
Schwarz
Schriftgröße:
Schriftgröße
Winzig
Klein
Normal
Groß
Riesig
Tags schließen
Schreibt eure Formeln hier im Board am besten mit Latex!
So gehts:
Latex-Kurzbeschreibung
|
Formeleditor
[quote="MBastieK"][quote="Qubit"]Nach meinem Verständnis nutzt Lean eben keine KI-Algorithmen, es ist ein "klassischer Proofer". Aber es macht durchaus Sinn, ihn auch mit KI-Input zu füttern. Manchmal kommt da etwas sinnvolles heraus :)[/quote] Die KI erstellt Beweis-Taktik-Befehl-Abläufe und testet diese in Lean, ob alle Beweis-Ziele gelöst werden.[/quote]
Optionen
HTML ist
aus
BBCode
ist
an
Smilies sind
an
BBCode in diesem Beitrag deaktivieren
Smilies in diesem Beitrag deaktivieren
Spamschutz
Text aus Bild eingeben
Alle Zeiten sind GMT + 1 Stunde
Gehe zu:
Forum auswählen
Themenbereiche
----------------
Mechanik
Elektrik
Quantenphysik
Astronomie
Wärmelehre
Optik
Sonstiges
FAQ
Sonstiges
----------------
Off-Topic
Ankündigungen
Thema-Überblick
<table border="0" cellpadding="3" cellspacing="1" width="100%" class="forumline"> <tr> <th class="thCornerL" width="22%" height="26">Autor</th> <th class="thCornerR">Nachricht</th> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 06. Okt 2026 11:59<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Qubit hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Nach meinem Verständnis nutzt Lean eben keine KI-Algorithmen, es ist ein "klassischer Proofer". Aber es macht durchaus Sinn, ihn auch mit KI-Input zu füttern. Manchmal kommt da etwas sinnvolles heraus <img src="images/smiles/balloon.gif" alt="smile" border="0" /></td> </tr></table><span class="postbody"> <br />Die KI erstellt Beweis-Taktik-Befehl-Abläufe und testet diese in Lean, ob alle Beweis-Ziele gelöst werden.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 05. Okt 2026 22:28<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Qubit hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Nach meinem Verständnis nutzt Lean eben keine KI-Algorithmen, es ist ein "klassischer Proofer". </td> </tr></table><span class="postbody"> <br />Völlig richtig.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Qubit</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 05. Okt 2026 18:16<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Nach meinem Verständnis nutzt Lean eben keine KI-Algorithmen, es ist ein "klassischer Proofer". Aber es macht durchaus Sinn, ihn auch mit KI-Input zu füttern. Manchmal kommt da etwas sinnvolles heraus <img src="images/smiles/balloon.gif" alt="smile" border="0" /></span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 03. Okt 2026 11:39<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Ja, das vermute ich auch, aber oben stand "Test".</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 03. Okt 2026 11:14<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Da wäre es nun interessant zu wissen, ob man Lean für Software<span style="font-weight: bold">tests</span> verwendet, oder für den sehr seltenen anzutreffenden Spezialfall des <span style="font-weight: bold">Beweises</span> der Korrektheit der Software.</td> </tr></table><span class="postbody"> <br />Eher 2.tes, denke ich.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 03. Okt 2026 06:39<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Da wäre es nun interessant zu wissen, ob man Lean für Software<span style="font-weight: bold">tests</span> verwendet, oder für den sehr seltenen anzutreffenden Spezialfall des <span style="font-weight: bold">Beweises</span> der Korrektheit der Software. <br /> <br />Für <span style="font-weight: bold">Tests</span> definiert man eine Auswahl von Test Cases, für die zu den Inputs die die jeweiligen Outputs vorab bekannt sind. Dann überprüft man, ob die Software für jeden Input den bekannten Output reproduziert. I.A. liegen zu viele mögliche Inputs vor, als dass man alle durchtesten könnte. <br /> <br />Für einen <span style="font-weight: bold">Beweis</span> müsste Lean für die Software beweisen, dass diese formal äquivalent ist zu einem vorab bekannten und in Lean formalisierten Algorithmus; dazu bedarf es einer Übersetzung der Software nach Lean (dass die Software selbst in Lean geschrieben ist, wäre ein Spezialfall). Ist das möglich, kommt man völlig ohne Test Cases aus. <br /> <br />Evtl. findet man sowas im Umfeld der Kryptographie. Das wäre insofern sinnvoll, als der Raum der Test Cases viel zu groß ist, um eine vollständige Testabdeckung zu erreichen.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 20:42<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">So wie ich es verstanden habe wird über Lean die Software (oder Parts) quasi vollständig induktiv getestet, anstatt per unvollständigem Brute-Forcing oder vermuteten aber unvollständigen Test-Cases. <br />Lean-Prinzip halt.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Nakamoto</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 16:05<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Lean soll auch für Software-Testing auf einem diskret qualitativ höherem Niveau nützlich sein.</td> </tr></table><span class="postbody"> <br /> <br />Das mag stimmen, nur fehlt mir die eigene Erfahrung in diesem Bereich, um dazu seriös etwas sagen zu können. (Ich kann zwar Programme schreiben, habe damit aber speziell nie gearbeitet). Das müssten also Informatiker bewerten oder Leute, die das tatsächlich schon gemacht haben.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 15:56<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Nakamoto hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Lean ist zwar sehr nützlich, aber man kann nicht sagen, dass ein Beweis "lückenlos verifiziert ist" nur weil er durch Lean durchgeht. Man kann da auch ziemlichen Unsinn "verifizieren". <br /> <br />Jemand der sich wirklich mit Typentheorie auskennt, kann zwar mit Lean bombenfeste Beweise schreiben, jemand der aber wenig Ahnung hat, kann damit auch ziemlichen Unsinn anstellen. <span style="font-weight: bold">Daher ist das eigentlich ein Tool für Spitzenmathematiker/Logiker/Philosophen und nicht </span>für Physiker und bei KIs muss alles von einem Profi exakt geprüft werden.</td> </tr></table><span class="postbody"> <br />Lean soll auch für Software-Testing auf einem diskret qualitativ höherem Niveau nützlich sein.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Nakamoto</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 12:54<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Ich dachte, du wolltest mit Junk auf etwas anderes hinaus.</td> </tr></table><span class="postbody"> <br /> <br />Ich meine jetzt gar keinen eigenen Begriff, nur den, der in "Mathe-Slang" bei solchen Theoremen oft verwendet wird, wenn sie geprüft werden. Ebene: Axiome sind nicht sinnvoll, Definitionen nicht oder Beweisziel wird verfehlt usw.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 11:48<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Ich habe ja explizit gesagt, dass nicht Lean vermutet, sondern die KI. <br /> <br />Dein formulierter Anspruch ist natürlich absolut sinnvoll. Wenn wir annehmen, dass die formale Basis, von der Lean ausgeht, konsistent ist, dann werden zwar keine falschen Theoreme bewiesen, jedoch nutzlose, und die Beweise sind für den Menschen völlig unverständlich und damit ebenfalls nutzlos. Nehmen wir an die KI liefert Satz plus Beweis, formalisiert mittels Gödelisierung. Der Satz erstreckt sich über einige tausend Zeilen, der Beweis über Millionen. Wer soll nun erkennen, ob die KI einfach nur das Produkt zweier riesiger Matrizen berechnet hat, oder ob darin ein Beweis der Riemann Vermutung steckt? Was von beidem nun vorliegt, könnte uns die KI umgangssprachlich erklären, aber darauf dürfen wir selbstverständlich nicht vertrauen. <br /> <br />Mit dem Vertrauen in deinem letzten Satz habe ich aber ein Problem. Unter der oben genannten Annahme würde ich Lean schon vertrauen, dass der Satz bzw. der Beweis korrekt ist, was aber nichts damit zu tun hat, ob der Satz inhaltlich etwas sinnvolles besagt. <br /> <br />Ich dachte, du wolltest mit Junk auf etwas anderes hinaus. Das ist natürlich ein zusätzliches Problem im Zusammenspiel zwischen KI und Lean, dass die KI zwischen dem eigentlichen Gehalt und den modellabhängigen Zutaten nicht unterscheiden kann, da sie beides einfach nur Text ist.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Nakamoto</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 11:15<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Was bedeutet das nun genau für das Zusammenspiel zwischen Lean und KI? Dass ersteres nutzlose, aber logisch zutreffende Junk-Theoreme vermutet und letzteres diese beweist?</td> </tr></table><span class="postbody"> <br /> <br />Das verstehe ich nicht. Lean vermutet nichts und bewertet auch nicht, ob ein Theorem mathematisch sinnvoll oder relevant ist. Lean prüft lediglich, ob ein formal formulierter Beweis im zugrunde liegenden formalen System tatsächlich aus den angegebenen Voraussetzungen folgt. <br /> <br />Mein Punkt ist ein anderer: Menschen können sich von einer KI Beweise in Lean erzeugen lassen, die anschließend von Lean formal bestätigt werden, ohne dass damit automatisch geklärt ist, ob der Beweis auch die mathematischen Anforderungen erfüllt, die man an einen guten Beweis stellt. Ein Mathematiker – ich habe seinen Namen leider vergessen – meinte vor Kurzem in einem Interview sinngemäß, dass Menschen KI-generierte Beweise erst dann veröffentlichen sollten, wenn sie den Beweis mindestens auf dem fachlichen Niveau eines promovierten Mathematikers erklären können. Dadurch könnten insbesondere inhaltliche Fehler, trivialisierte Problemstellungen oder Beweise, die zwar formal korrekt, aber am eigentlichen mathematischen Problem vorbeigehen, bereits vor der Veröffentlichung erkannt werden. Das halte ich für einen sinnvollen Anspruch. <br /> <br />„Dein Theorem“ ist für sich genommen auch überhaupt kein problematischer Fall, weil man unmittelbar erkennen kann, worum es geht. Das Problem entsteht bei der Größenordnung. Wenn ich beispielsweise 300 Seiten Lean-Code vor mir habe und irgendwo darin eine problematische Stelle steckt, reicht es nicht mehr, nur darauf zu verweisen, dass Lean den gesamten Code akzeptiert hat. Man müsste den Beweis zunächst inhaltlich nachvollziehen und den Code Zeile für Zeile analysieren, um überhaupt feststellen zu können, was dort tatsächlich bewiesen wurde und ob es dem entspricht, was ursprünglich behauptet oder beabsichtigt war. <br /> <br />Genau deshalb würde ich zwischen zwei Fragen unterscheiden: <br /> <br />1. Ist der formale Lean-Beweis korrekt? <br /> Das kann Lean innerhalb seines formalen Systems prüfen. <br /> <br />2. Ist das, was dort formal bewiesen wurde, auch der mathematisch relevante und inhaltlich überzeugende Beweis des behaupteten Resultats? <br /> Das kann Lean nicht allein dadurch garantieren, dass es den Code akzeptiert. <br /> <br />Bei einem kleinen und überschaubaren Theorem kann ich diese zweite Frage selbst relativ schnell überprüfen. Bei einem sehr großen KI-generierten Beweis wird das dagegen zu einem erheblichen Problem. Solange ich einen solchen konkreten Beweis nicht selbst inhaltlich nachvollzogen habe und er – insbesondere bei einem großen oder bedeutenden mathematischen Problem wie dem aktuell diskutierten – nicht zusätzlich von Fachleuten geprüft und anerkannt wurde, würde ich ihm daher zunächst mit begründetem Misstrauen begegnen. Nicht, weil ich annehme, dass Lean falsch arbeitet, sondern weil die formale Verifikation des Codes und die fachliche Validierung des mathematischen Inhalts zwei verschiedene Dinge sind (und hier spreche ich explizit nicht davon, ob er "wirklich logisch richtig oder falsch ist" (oder mathematisch, was 2 verschiedene Dinge sind) sondern nur, ob er der "normalen wissenschaftlichen Praxis" in Mathe oder Logik entspricht.) <br /> <br />Mir geht es übrigens auch nicht um die Frage: <br /> <br /></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Ist dieser Unsinn nun logisch falsch oder einfach nur Junk?</td> </tr></table><span class="postbody"> <br /> <br />Damit würde man sofort eine viel grundsätzlichere Diskussion darüber eröffnen, was überhaupt unter „Logik“ zu verstehen ist. <br /> <br />Meine eigentliche Frage ist viel enger: Welchen mathematischen Status wollen wir KI-gestützten Mathematik-Lean-Beweisen zusprechen, wenn sie zwar formal von Lean verifiziert wurden, aber nicht von einem Menschen inhaltlich verstanden und nachvollzogen wurden? Ich würde jedenfalls nicht automatisch denselben Status annehmen wie bei einem von einem Mathematiker selbst durchdachten, verstandenen und erklärbaren Beweis. <br /> <br />Darum mein erster Beitrag, nur weil Lean den Code bestätigt, ist er noch nicht "Zeile für Zeile verifiziert", das ist er erst, wenn jemand der sich mit Lean auskennt, das selber geprüft hat.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 10:02<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Nakamoto hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Lean ist ein konstruktivistisches Beweissystem und daher sogar noch anfälliger für Junk-Theoreme, als klassische Beweisführung in der Mathematik (selbst da kann man schnell Junktheoreme schreiben). </td> </tr></table><span class="postbody"> <br />Was bedeutet das nun genau für das Zusammenspiel zwischen Lean und KI? Dass erstere nutzlose aber logisch zutreffende Junk-Theoreme vermutet und letztere diese beweist? <br /> <br /></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Nakamoto hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Lean ist zwar sehr nützlich, aber man kann nicht sagen, dass ein Beweis "lückenlos verifiziert ist" nur weil er durch Lean durchgeht. Man kann da auch ziemlichen Unsinn "verifizieren". </td> </tr></table><span class="postbody"> <br />Ist dieser Unsinn nun logisch falsch oder einfach nur Junk? <br /> <br />Beispiel: definiert man die natürlichen Zahlen nach von Neumann, so erhält man folgende Darstellung: <br /> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?0 &= \{\} = \emptyset "> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?1 &= \{0\} = \{\emptyset\} "> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?2 &= \{0, 1\} = \{\emptyset, \{\emptyset\}\}"> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?3 &= \{0, 1, 2\} = \{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}"> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?\ldots"> <br /> <br />Damit folgt das Junk-Theorem. <br /> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?n \cap n+k = n"> <br /> <br />Dieses Theorem ist aber innerhalb der Peano-Arithmetik nicht falsch, es ist zunächst überhaupt nicht formulierbar. Es entsteht als Zusatz zu den üblichen Eigenschaften der natürlichen Zahlen aufgrund einer speziellen Darstellung (in diesem speziellen Fall kann man dem Theorem sogar einen Sinn verleihen, wenn man die Schnittmengenbildung mit min(n, n+k) identifiziert) <br /> <br />Übertragen auf KI + Lean würde ich nun vermuten, dass man schlicht vermeiden muss, mit derartigem Junk zugemüllt zu werden. <br /> <br />Ist es das, was du meinst?</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 09:48<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Wolkenlicht8934 hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Die KI schaufelt am Ende nur die Varianten heran, aber der formale Beweis im Hintergrund macht die Arbeit. </td> </tr></table><span class="postbody"> <br />Verglichen mit der menschlichen Art Mathematik zu betreiben, würde ich schon sagen, dass beides Arbeit ist. <br /> <br />Die KI erledigt ja in gewisser Weise einen kreativen Job, nämlich ausgehend von einem enormen Erfahrungsschatz lose Enden zu identifizieren, Vermutungen zu präsentieren und ähnliches. <br /> <br />Zum Vergleich: McKay, Conway und Norton stellten fest, dass die Dimensionen der irreduziblen Darstellungen der Monstergruppe mit Koeffizienten der q-Reihe der elliptischen Modulfunktion j(τ) zusammenhängen. Die harte Arbeit steckt hier in der jahrelangen Ausbildung. Ich weiß nicht, inwieweit dieses Beispiel auf die aktuellen Ansätze mit KI + Lean passt, aber es springt auch einem Laien ins Auge, der von Mathematik keine Ahnung hat, insofern es mittels konkreter Zahlen geeignet aufbereitet wurde: <br /> <br /><a href="https://en.wikipedia.org/wiki/Monstrous_moonshine#McKay" target="_blank">https://en.wikipedia.org/wiki/Monstrous_moonshine#McKay</a>'s_observation_and_the_Conway%E2%80%93Norton_conjecture <br /> <br />Eine gut trainierte KI, der man das Wissen über die Vermutung vorenthalten hätte, würde derartiges mittels pattern matching wohl sehr schnell finden; daraus aber ein Theorem zu formulieren, das man Lean vorwerfen kann, ist nochmal eine ganz andere Nummer. <br /> <br />Nehmen wir an, die konkrete Zahlen hätten es nie in die Trainingsdaten der KI geschafft, dann wäre diese wohl nie in der Lage, eine derartige Verbindung zu vermuten; McKay, Conway und Norton aber wohl auch nicht …</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Nakamoto</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 02. Okt 2026 06:49<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Rechenpower draufzuhauen und im Grunde nur hochkomplex zu „brute-forcen“ ist die eine Sache, aber dass ein Tool wie Lean das Ganze mathematisch absolut lückenlos verifiziert, ist das eigentliche Brett</td> </tr></table><span class="postbody"> <br /> <br />Lean ist ein konstruktivistisches Beweissystem und daher sogar noch anfälliger für Junk-Theoreme, als klassische Beweisführung in der Mathematik (selbst da kann man schnell Junktheoreme schreiben). <br /> <br />Lean ist zwar sehr nützlich, aber man kann nicht sagen, dass ein Beweis "lückenlos verifiziert ist" nur weil er durch Lean durchgeht. Man kann da auch ziemlichen Unsinn "verifizieren". <br /> <br />Jemand der sich wirklich mit Typentheorie auskennt, kann zwar mit Lean bombenfeste Beweise schreiben, jemand der aber wenig Ahnung hat, kann damit auch ziemlichen Unsinn anstellen. Daher ist das eigentlich ein Tool für Spitzenmathematiker/Logiker/Philosophen und nicht für Physiker und bei KIs muss alles von einem Profi exakt geprüft werden.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Wolkenlicht8934</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 30. Sep 2026 15:13<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Genau das ist der Punkt: Rechenpower draufzuhauen und im Grunde nur hochkomplex zu „brute-forcen“ ist die eine Sache, aber dass ein Tool wie Lean das Ganze mathematisch absolut lückenlos verifiziert, ist das eigentliche Brett. Die KI schaufelt am Ende nur die Varianten heran, aber der formale Beweis im Hintergrund macht die Arbeit – das ist technischer Fortschritt, bei dem der rohen Kraft endlich ein sauberes Korsett verpasst wird. Manchmal verliert man sich so tief in logischen Beweisen und Code, dass der Kopf total brummt; ich muss dann immer kurz abschalten und lenke mich gerne ab, indem ich im Netz nach feinem Körperschmuck stöbere oder <a href="https://www.ohr-piercing-schmuck.de/collections/conch-ring-piercing/" target="_blank" class="postlink">Conch Ring Piercing hier entdecken</a> anklicke, um mal auf andere Gedanken zu kommen.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 26. Sep 2026 15:25<span class="gen"> </span> Titel: Re: Ersetzt KI Physiker, Mathematiker und Ingenieure?</span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Nachdenklich hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">da ja ein KI System anscheinend das Milleniumproblem zu der Navier Stokes Gleichung gelöst hat. <br />... <br />Ich bin erstaunt, dass solch ein Problem durch KI gelöst wurde</td> </tr></table><span class="postbody"> <br />Manchmal bezeichne ich das, was die KI (da) macht als Brute-Forcing. Und der Naviar-Stokes-Beweis(40 Millionen Euro Brute-Forcing) war ja ein Existenz-Beweis und kein All-Beweis, was aber irrelevant sein sollte bezüglich Lean(inherente vollständige Induktion) und genügend Vorarbeit. <br /> <br />Das technisch Geniale daran ist eher Lean, nicht die KI.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 17. Sep 2026 07:06<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>DrStupid hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Beispielsweise hat Demis Hassabis (CEO von Google DeepMind & Chemienobelpreisträger) in einem Podcast gesagt er würde die Modelle gerne testen indem man ihnen das physikalische Wissen bis 1905 gibt und testet ob sie die spezielle Relativitätstheorie entwickeln kann. Ob das bereits ernsthaft versucht wurde, weiß ich nicht.</td> </tr></table><span class="postbody"> <br />Es wurde in anderen Bereichen erfolgreich getestet. <br /> <br />Herleitung der Keplerschen Gesetze aus den Daten von Tycho Brahe: <br /><a href="https://www.nature.com/articles/s41467-023-37236-y" target="_blank">https://www.nature.com/articles/s41467-023-37236-y</a> <br /> <br />Herleitung von Newton aus Kepler: <br /><a href="https://openreview.net/pdf?id=vA9hti-Fi7H" target="_blank">https://openreview.net/pdf?id=vA9hti-Fi7H</a> <br /></td> </tr></table><span class="postbody"> <br />Der Nature-Artikel ist sehr klar: <br /> <br /></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">More specifically, the <span style="font-weight: bold">inputs</span> to our system are … as follows. <br /><span style="font-weight: bold">Background Knowledge</span>: a set of domain-specific axioms expressed as logic formulae. <br /><span style="font-weight: bold">A Hypothesis Class</span>: a set of admissible symbolic models … <br /> <br />Kepler’s law relates the distance d between two bodies (e.g., the sun and a planet in the solar system) and their orbital periods. It can be expressed as … where p is the period, G is the gravitational constant, and m1 and m2 are the two masses. It can be derived <span style="font-weight: bold">using the following axioms</span> of the background theory, describing <br />the center of mass (axiom K1), <br />the distance between bodies (axiom K2), <br />the gravitational force (axiom K3), <br />the centrifugal force (axiom K4), <br />the force balance (axiom K5), <br />and the period (axiom K6)</td> </tr></table><span class="postbody"> <br />Das hat für mich <span style="font-weight: bold">nichts</span> mit Abduktion zu tun, diese würde ja gerade nicht Naturgesetze als Input verwenden sondern sie als Output liefern. <br /> <br />Auch der zweite Artikel ist sehr klar bei der Unterscheidung, was die Maschine tut, und was der Mensch: <br /> <br /></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote"> For example, <span style="font-weight: bold">AI algorithms <br />may discover a new combination of variables</span> that as a whole <br />is particularly useful for predicting and explaining the data <br />(we will discuss with more details in the following). In this <br />case, <span style="font-weight: bold">human experts may try to interpret the physical mean- <br />ing of this combination of variables</span> and leverage it to gain <br />better understandings of the problem. Sometimes, human <br />experts may also need to innovatively create new physical <br />concepts up front or with the assistance of AI during the dis- <br />covery process so as to better interpret the results, enabling <br />a human-AI collaborative science discovery process.</td> </tr></table><span class="postbody"> <br />Auch das ist <span style="font-weight: bold">keine Abduktion</span> seitens der Maschine. Die Methoden zur symbolischen Regression liefern für Menschen interpretierbare Resultate, die diese dann in einem kreativen Prozess verwenden könnten. <br /> <br />Am Ende stünde dann die Hypothese <br /> <br /><img class="latex2png" src="https://www.matheboard.de/latex2png/latex2png.php?F_{m_a, m_b} (r) = - \frac{G m_a m_b}{r}"> <br /> <br />aber gerade das ist ja nicht das Ergebnis der Arbeiten.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 17. Sep 2026 06:42<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"> Solche Ideen werden auf jeden Fall auch schon diskutiert. Beispielsweise hat Demis Hassabis (CEO von Google DeepMind & Chemienobelpreisträger) in einem Podcast gesagt er würde die Modelle gerne testen indem man ihnen das physikalische Wissen bis 1905 gibt und testet ob sie die spezielle Relativitätstheorie entwickeln kann. Ob das bereits ernsthaft versucht wurde, weiß ich nicht.</td> </tr></table><span class="postbody"> <br />Sehr interessant, danke.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>DrStupid</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 16. Sep 2026 14:45<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Beispielsweise hat Demis Hassabis (CEO von Google DeepMind & Chemienobelpreisträger) in einem Podcast gesagt er würde die Modelle gerne testen indem man ihnen das physikalische Wissen bis 1905 gibt und testet ob sie die spezielle Relativitätstheorie entwickeln kann. Ob das bereits ernsthaft versucht wurde, weiß ich nicht.</td> </tr></table><span class="postbody"> <br /> <br />Es wurde in anderen Bereichen erfolgreich getestet. <br /> <br />Herleitung der Keplerschen Gesetze aus den Daten von Tycho Brahe: <br /><a href="https://www.nature.com/articles/s41467-023-37236-y" target="_blank">https://www.nature.com/articles/s41467-023-37236-y</a> <br /> <br />Herleitung von Newton aus Kepler: <br /><a href="https://openreview.net/pdf?id=vA9hti-Fi7H" target="_blank">https://openreview.net/pdf?id=vA9hti-Fi7H</a> <br /> <br />Zumindest mit der speziellen Relativitätstheorie sollte das auch klappen. Bei der allgemeinen Relativitätstheorie wäre ich eher skeptisch.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>antaris</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 16. Sep 2026 13:26<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote"> <br />Ich hätte dazu eine sehr konkrete Idee für ein Experiment: man trainiert ein LLM mit den bewährten Methoden, jedoch etablierten Wissen eingefroren auf einem bestimmten Stand – zum Beispiel 1960 * – und schaut, welche in den darauffolgenden Jahren erfolgten Entdeckungen die KI reproduzieren kann. Ich glaube nur, dass die Firmen an einem derartigen Experiment kein großes Interesse haben, denn wenn man es ernst nimmt und die Ehrlichkeit des Zeithorizont wirklich sicherstellen will, dann bedeutet es großen Aufwand bei der Auswahl der Trainingsdaten, und evtl. stellt sich das Ergebnis eben so dar, dass die Dinger tatsächlich nicht kreativ sind, und dass eigene Entdeckungen über ein paar Monate nicht hinausreichen. Diese vermutete bzw. befürchtete Erkenntnis – zusammen mit dem fehlenden tragfähigen Geschäftsmodell – lässt mich ernsthaft an der Durchführbarkeit bzw. dem Willen dazu zweifeln. <br /> <br />Eventuell hat hier ja jemand eine Idee, wie man einen großen Player zu einem derartigen Experiment unter kontrollierten Bedingungen überreden könnte. <br /></td> </tr></table><span class="postbody"> <br /> <br />Solche Ideen werden auf jeden Fall auch schon diskutiert. Beispielsweise hat Demis Hassabis (CEO von Google DeepMind & Chemienobelpreisträger) in einem Podcast gesagt er würde die Modelle gerne testen indem man ihnen das physikalische Wissen bis 1905 gibt und testet ob sie die spezielle Relativitätstheorie entwickeln kann. Ob das bereits ernsthaft versucht wurde, weiß ich nicht.</td> </tr></table><span class="postbody"> <br /> <br /> <br />Hassabis Idee hat es am 09.09.2026 mit dem Thema in Nature geschafft: <a href="https://www.nature.com/articles/d41586-026-02804-x" target="_blank">https://www.nature.com/articles/d41586-026-02804-x</a> <br /> <br />Im Artikel wird auch ein weiteres Paper benannt von April diesen Jahres "LLMs can't jump": <a href="https://openreview.net/forum?id=klU4737opt" target="_blank">https://openreview.net/forum?id=klU4737opt</a> <br /> <br />Ansonsten Stichwort "Vintage LLM" bei Google.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Corbi</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 16. Sep 2026 10:49<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote"> <br />Ich hätte dazu eine sehr konkrete Idee für ein Experiment: man trainiert ein LLM mit den bewährten Methoden, jedoch etablierten Wissen eingefroren auf einem bestimmten Stand – zum Beispiel 1960 * – und schaut, welche in den darauffolgenden Jahren erfolgten Entdeckungen die KI reproduzieren kann. Ich glaube nur, dass die Firmen an einem derartigen Experiment kein großes Interesse haben, denn wenn man es ernst nimmt und die Ehrlichkeit des Zeithorizont wirklich sicherstellen will, dann bedeutet es großen Aufwand bei der Auswahl der Trainingsdaten, und evtl. stellt sich das Ergebnis eben so dar, dass die Dinger tatsächlich nicht kreativ sind, und dass eigene Entdeckungen über ein paar Monate nicht hinausreichen. Diese vermutete bzw. befürchtete Erkenntnis – zusammen mit dem fehlenden tragfähigen Geschäftsmodell – lässt mich ernsthaft an der Durchführbarkeit bzw. dem Willen dazu zweifeln. <br /> <br />Eventuell hat hier ja jemand eine Idee, wie man einen großen Player zu einem derartigen Experiment unter kontrollierten Bedingungen überreden könnte. <br /></td> </tr></table><span class="postbody"> <br /> <br />Solche Ideen werden auf jeden Fall auch schon diskutiert. Beispielsweise hat Demis Hassabis (CEO von Google DeepMind & Chemienobelpreisträger) in einem Podcast gesagt er würde die Modelle gerne testen indem man ihnen das physikalische Wissen bis 1905 gibt und testet ob sie die spezielle Relativitätstheorie entwickeln kann. Ob das bereits ernsthaft versucht wurde, weiß ich nicht.[/quote]</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 14. Sep 2026 23:00<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Jakito hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Bei der Abduktion scheint ein Interesse Deinerseits durchzuscheinen, wie Menschen überhaupt zu neuem (gesicherten) Wissen kommen. Das ist ein spannendes Thema, mit dem sich Philosophen und Logiker wie Charles Sanders Peirce intensiv auseinandergesetzt haben. Und bei existierenden Experimenten scheint ein einzelnes LLM (mit einem einzelnen Kontextfenster) nicht in der Lage, diese Art von neuem Wissen zu erlangen. Wieso dies erst gelingt, wenn eine Menge von LLMs (mit jeweils eigenem Kontextfenster) von einem weiteren LLM "orchestriert" wird, ist vermutlich noch weitgehend unverstanden.</td> </tr></table><span class="postbody"> <br />Ich habe nochmal etwas nachgedacht. <br /> <br />Abduktion ist wohl nicht scharf von Induktion zu trennen. Letztlich ist ersteres oft nur auf die Spitze getriebene Induktion, also die Vermutung eines nicht gerade naheliegenden Bildungsgesetzes – Bsp. SU(3) flavor / <span style="font-style: italic">the eightfold way. </span> War denn Newton's Idee des Gravitationsgesetzes wirklich etwas völlig Neuartiges? Und wenn ja, kann man dass das objektiv bewerten? <br /> <br />Ein Ausgangspunkt war ja die Frage, ob bei qualitativ neue Fähigkeiten entwickeln. Sowas erschien aber schon immer ziemlich subjektiv. Ist der Sprung von Logarithmentafeln zu FORTRAN und später zu symbolischer Verarbeitung wirklich qualitativ ein anderer als jetzt zu LLMs? Oder ist es nicht einfach nur so, dass die extrem schnellen Entwicklung der letzten paar Jahre uns zu überfordern scheint, während wir völlig entspannt auf die vergangenen Jahrhunderte zurückblicken können? <br /> <br /><span style="font-style: italic">Any sufficiently advanced technology is indistinguishable from magic.</span> <br />(Arthur C. Clarke) <br /> <br />Was soll ich sagen, ich weiß es auch nicht.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Jakito</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 14. Sep 2026 17:37<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Letztlich geht es um den Unterschied zwischen Induktion, Deduktion und Abduktion. Induktion ist klar, das ist letztlich Mustererkennung plus einfache Verallgemeinerung. Deduktion ist auch klar, das erledigt (in den bekannten Fällen) nie das LLM selbst. Letzteres ist der eigentlich kreative Teil, also ausgehend von induktiv gewonnenem und deduktiv abgesichertem Wissen die Idee des "was wäre, wenn?" zu formulieren.</td> </tr></table><span class="postbody">Ich wage zu bezweifeln, dass die LLMs signifikant weniger Deduktion können oder machen, als Menschen. Die Tools verifizieren nur, dass dem LLM bei der Deduktion keine Fehler unterlaufen sind. Solche Fehler machen Menschen genauso, selbst wenn die Art der Fehler vielleicht ein wenig anders gelagert ist. <br /> <br />Bei der Abduktion scheint ein Interesse Deinerseits durchzuscheinen, wie Menschen überhaupt zu neuem (gesicherten) Wissen kommen. Das ist ein spannendes Thema, mit dem sich Philosophen und Logiker wie Charles Sanders Peirce intensiv auseinandergesetzt haben. Und bei existierenden Experimenten scheint ein einzelnes LLM (mit einem einzelnen Kontextfenster) nicht in der Lage, diese Art von neuem Wissen zu erlangen. Wieso dies erst gelingt, wenn eine Menge von LLMs (mit jeweils eigenem Kontextfenster) von einem weiteren LLM "orchestriert" wird, ist vermutlich noch weitgehend unverstanden. <br /> <br /></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">… allerdings wird aus den Diskussionen der letzten Tage nach meinem Dafürhalten klar, das wieder menschliche Mathematiker die kreativen Ideen generiert haben, die KI hingegen die (anspruchsvolle) Fleißarbeit erledigt hat.</td> </tr></table><span class="postbody">Und ursprünglich hatte die KI es auch versäumt, die Vorarbeiten von Cordoba und Martinez-Zoroa zu zitieren. Das wurde aber sehr zeitnah geflickt. Das ist bei der KI leider immer sehr ärgerlich, dass die sich mit ihren Quellen so schwertut. <br /> <br />Mich persönlich stört aber der "Tokens für $15 Millionen" verbraucht Teil am meisten. Das ist nicht nachhaltig, auf diese Weise kann man zwar Werbung für die Fähigkeiten des Models machen, aber nicht wirklich echten Mathematikern in der Spitzenforschung bei ihren Herausforderungen helfen. So blöd das klingt, aber wenn es nur $500 000 oder $1 Millionen gewesen wären, dann hätte ich damit viel besser leben können. Solche Geldbeträge kann man im Zweifelsfalle noch auftreiben, wenn es wirklich wichtig ist.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 12. Sep 2026 12:07<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Die Frage nach einer möglichen Schummelei hat natürlich nichts mit der Frage dieses Threads zu tun …</td> </tr></table><span class="postbody"> <br />… allerdings wird aus den Diskussionen der letzten Tage nach meinem Dafürhalten klar, das wieder menschliche Mathematiker die kreativen Ideen generiert haben, die KI hingegen die (anspruchsvolle) Fleißarbeit erledigt hat.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 11. Sep 2026 22:34<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Die Frage nach einer möglichen Schummelei hat natürlich nichts mit der Frage dieses Threads zu tun.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Qubit</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 11. Sep 2026 16:26<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Qubit hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Telefonmann hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Was mich wirklich interessieren würde, wäre eine ehrliche und umfassende Analyse durch Mathematiker bzgl. der Fragestellung, wieviel tatsächlich neuartige Ideen, Konstruktionen, Definitionen, Vermutungen und dann bewiesene Theoreme die KI tatsächlich eigenständig hervorgebracht hat, und wie weit entfernt von etablierten Wissen dies jeweils anzusiedeln ist. Letzteres kann man natürlich quantitativ nur schwer fassen.</td> </tr></table><span class="postbody"> <br /><a href="https://www.youtube.com/watch?v=eR2q8s4VB1w" target="_blank" class="postlink">Sabine Hossenfelder</a> gibt in dem verlinkten Clip ab 02:00 ein paar Insights. Diese lese und werte ich weniger als neue Ideen und mehr als ziemlich gut ausgewählte Verknüpfung vorhandener Ideen. Sabine sagt auch ganz klar, dass es für Korrektheit der Schlussfolgerungen nur eine abgeschätzte, hohe Wahrscheinlichkeit um die 90% gibt und verweist auf die Möglichkeit versteckter Zirkelschlüsse, was ich wiederum als ein sehr schwerwiegendes Argument bewerte. <br /> <br />Kurz: Man könnte OpenAI damit auch als exzellenten "Verkäufer" bezeichnen, der Argumente verwendet, die nur sehr schwer zu überprüfen sind.</td> </tr></table><span class="postbody"> <br /> <br />Da geht ja das Thema eigentlich etwas weiter, weil zwei Experten auf diesem Gebiet, Buckmaster und Alpöge, selbst die KI genutzt haben, um Grundlagen für diesen Beweis zu schaffen. Hat der Anbieter dieser KI dieses Expertenwissen nun ausgnutzt, um selbst daraus eine Publikation zu machen?.. <br /> <br /><a href="https://www.mathematik.de/dmv-blog/5338-navier-stokes-problem-gel%C3%B6st" target="_blank">https://www.mathematik.de/dmv-blog/5338-navier-stokes-problem-gel%C3%B6st</a></td> </tr></table><span class="postbody"> <br /> <br />PS: die Anbieter der KI-Modelle haben freilich interne Entwicklungen von KI-Modellen, die besser sind und nicht der Allgemeinheit zur Verfügung stehen. <br />Eine Herausforderung sind da auch die "Millenium-Probleme", eine Heuristik zu haben, welche Probleme davon gelöst werden könnten. Hier war dann das "Navier-Stokes-Problem" im Fokus..</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Qubit</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 11. Sep 2026 15:50<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Telefonmann hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Was mich wirklich interessieren würde, wäre eine ehrliche und umfassende Analyse durch Mathematiker bzgl. der Fragestellung, wieviel tatsächlich neuartige Ideen, Konstruktionen, Definitionen, Vermutungen und dann bewiesene Theoreme die KI tatsächlich eigenständig hervorgebracht hat, und wie weit entfernt von etablierten Wissen dies jeweils anzusiedeln ist. Letzteres kann man natürlich quantitativ nur schwer fassen.</td> </tr></table><span class="postbody"> <br /><a href="https://www.youtube.com/watch?v=eR2q8s4VB1w" target="_blank" class="postlink">Sabine Hossenfelder</a> gibt in dem verlinkten Clip ab 02:00 ein paar Insights. Diese lese und werte ich weniger als neue Ideen und mehr als ziemlich gut ausgewählte Verknüpfung vorhandener Ideen. Sabine sagt auch ganz klar, dass es für Korrektheit der Schlussfolgerungen nur eine abgeschätzte, hohe Wahrscheinlichkeit um die 90% gibt und verweist auf die Möglichkeit versteckter Zirkelschlüsse, was ich wiederum als ein sehr schwerwiegendes Argument bewerte. <br /> <br />Kurz: Man könnte OpenAI damit auch als exzellenten "Verkäufer" bezeichnen, der Argumente verwendet, die nur sehr schwer zu überprüfen sind.</td> </tr></table><span class="postbody"> <br /> <br />Da geht ja das Thema eigentlich etwas weiter, weil zwei Experten auf diesem Gebiet, Buckmaster und Alpöge, selbst die KI genutzt haben, um Grundlagen für diesen Beweis zu schaffen. Hat der Anbieter dieser KI dieses Expertenwissen nun ausgnutzt, um selbst daraus eine Publikation zu machen?.. <br /> <br /><a href="https://www.mathematik.de/dmv-blog/5338-navier-stokes-problem-gel%C3%B6st" target="_blank">https://www.mathematik.de/dmv-blog/5338-navier-stokes-problem-gel%C3%B6st</a></span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>MBastieK</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 11. Sep 2026 01:08<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>ML hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">ist eigentlich bekannt, welche Mathematiker in welchem Ausmaß an dem Problem mitgelöst haben? </td> </tr></table><span class="postbody"> <br />Beim Durchzappen sieht man einige Namen <br /><a href="https://www.youtube.com/watch?v=Cn6F1wAhjyo#t=23m01s" target="_blank">https://www.youtube.com/watch?v=Cn6F1wAhjyo#t=23m01s</a> <br /><a href="https://www.youtube.com/watch?v=Cn6F1wAhjyo#t=19m13s" target="_blank">https://www.youtube.com/watch?v=Cn6F1wAhjyo#t=19m13s</a> <br /> <br />Teilweise kann man auch über Untertitel suchen bzw. überschauen.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Telefonmann</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 22:25<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Was mich wirklich interessieren würde, wäre eine ehrliche und umfassende Analyse durch Mathematiker bzgl. der Fragestellung, wieviel tatsächlich neuartige Ideen, Konstruktionen, Definitionen, Vermutungen und dann bewiesene Theoreme die KI tatsächlich eigenständig hervorgebracht hat, und wie weit entfernt von etablierten Wissen dies jeweils anzusiedeln ist. Letzteres kann man natürlich quantitativ nur schwer fassen.</td> </tr></table><span class="postbody"> <br /><a href="https://www.youtube.com/watch?v=eR2q8s4VB1w" target="_blank" class="postlink">Sabine Hossenfelder</a> gibt in dem verlinkten Clip ab 02:00 ein paar Insights. Diese lese und werte ich weniger als neue Ideen und mehr als ziemlich gut ausgewählte Verknüpfung vorhandener Ideen. Sabine sagt auch ganz klar, dass es für Korrektheit der Schlussfolgerungen nur eine abgeschätzte, hohe Wahrscheinlichkeit um die 90% gibt und verweist auf die Möglichkeit versteckter Zirkelschlüsse, was ich wiederum als ein sehr schwerwiegendes Argument bewerte. <br /> <br />Kurz: Man könnte OpenAI damit auch als exzellenten "Verkäufer" bezeichnen, der Argumente verwendet, die nur sehr schwer zu überprüfen sind.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>ML</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 22:14<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Hallo, <br /> <br />ist eigentlich bekannt, welche Mathematiker in welchem Ausmaß an dem Problem mitgelöst haben? Das ist wohl das Paper, um das es geht. Dort steht kein Autorenname: <br /><a href="https://openai.com/index/navier-stokes-solution/" target="_blank">https://openai.com/index/navier-stokes-solution/</a> <br /><a href="https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf" target="_blank">https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf</a> <br /> <br />Viele Grüße <br />Michael</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 19:26<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Aber ist das nicht ein Verdrängungsmechanismus, selbst jetzt wo scheinbar eines der größten Probleme der Mathematik durch KI gelöst wurde, ihre Fähigkeiten herunterzuspielen? <br /> <br />Oder kannst du das näher erläutern warum es sich nur um "ein Zusammenfügen loser enden" handeln soll?</td> </tr></table><span class="postbody"> <br />Letztlich geht es um den Unterschied zwischen Induktion, Deduktion und Abduktion. Induktion ist klar, das ist letztlich Mustererkennung plus einfache Verallgemeinerung. Deduktion ist auch klar, das erledigt (in den bekannten Fällen) nie das LLM selbst. Letzteres ist der eigentlich kreative Teil, also ausgehend von induktiv gewonnenem und deduktiv abgesichertem Wissen die Idee des "was wäre, wenn?" zu formulieren. <br /> <br />Ich bin natürlich weit davon entfernt, diese Beweise vollständig gelesen zu haben, aber was ich so mitbekomme, handelt es sich eben um Verknüpfen von verschiedenen losen Enden, die im LLM sozusagen präsent sind, plus eine Zusammenarbeit mit bzw. Unterstützung durch Mathematica, Lean etc., sowie natürlich enge Leitplanken durch die Prompts. <br /> <br />Was mich wirklich interessieren würde, wäre eine ehrliche und umfassende Analyse durch Mathematiker bzgl. der Fragestellung, wieviel tatsächlich neuartige Ideen, Konstruktionen, Definitionen, Vermutungen und dann bewiesene Theoreme die KI tatsächlich eigenständig hervorgebracht hat, und wie weit entfernt von etablierten Wissen dies jeweils anzusiedeln ist. Letzteres kann man natürlich quantitativ nur schwer fassen. <br /> <br />Ich hätte dazu eine sehr konkrete Idee für ein Experiment: man trainiert ein LLM mit den bewährten Methoden, jedoch etablierten Wissen eingefroren auf einem bestimmten Stand – zum Beispiel 1960 * – und schaut, welche in den darauffolgenden Jahren erfolgten Entdeckungen die KI reproduzieren kann. Ich glaube nur, dass die Firmen an einem derartigen Experiment kein großes Interesse haben, denn wenn man es ernst nimmt und die Ehrlichkeit des Zeithorizont wirklich sicherstellen will, dann bedeutet es großen Aufwand bei der Auswahl der Trainingsdaten, und evtl. stellt sich das Ergebnis eben so dar, dass die Dinger tatsächlich nicht kreativ sind, und dass eigene Entdeckungen über ein paar Monate nicht hinausreichen. Diese vermutete bzw. befürchtete Erkenntnis – zusammen mit dem fehlenden tragfähigen Geschäftsmodell – lässt mich ernsthaft an der Durchführbarkeit bzw. dem Willen dazu zweifeln. <br /> <br />Eventuell hat hier ja jemand eine Idee, wie man einen großen Player zu einem derartigen Experiment unter kontrollierten Bedingungen überreden könnte. <br /> <br />* in der Physik kenne ich mich besser aus, da gäbe es ein paar knackige Benchmarks: die Lichtquantenhypothese, die spezielle und die allgemeine Relativitätstheorie, die Heisenbergsche und die Schrödingersche Formulierung der Quantenmechanik … die Ausgangssituation und die experimentellen Befunde sind bekannt, mit Ausnahme der ART ist das mathematische Rüstzeug extrem überschaubar, die Arbeiten auf ein paar dutzend Seiten zu Papier gebracht, entscheidend sind jeweils nur ein paar kreative Ideen.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Qubit</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 16:36<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Corbi hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote"> <br />Oder kannst du das näher erläutern warum es sich nur um "ein Zusammenfügen loser enden" handeln soll?</td> </tr></table><span class="postbody"> <br /> <br />Informationstheoretisch kann da eine KI, ein LLM, nicht mehr schaffen, als in den riesigen "Trainingsdaten" enthalten ist. Aber das eben sehr effektiv, also "lose Enden" miteinander verbinden. <br />Im Prinzip haben das auch viele grosse Denker schon so getan, zB. Leibniz, der eine wahnsinnige grosse Korrespondenz mit anderen grossen Denkern hatte und meinte, dass man auch in jeder noch so schlechten Idee etwas Nützliches (resp. "Wahres") finden könnte.. <br />Aber eben mehr Information auch nicht [was "Kunst" (Musik, Malerei,..) angeht, sind sogar Variationen neben diesen Informationen sehr nützlich..]</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Nachdenklich</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 15:41<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>Zitat:</b></span></td> </tr> <tr> <td class="quote">Oder kannst du das näher erläutern warum es sich nur um "ein Zusammenfügen loser enden" handeln soll?</td> </tr></table><span class="postbody"> <br /> <br />Das würde mich auch interessieren.</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Corbi</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 01:20<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Ich fand diesen Artikel hier von Terence Tao zum Thema sehr interessant, indem er argumentiert, dass KI vermutlich dazu führt dass wir Ziele und Werte von Mathematik völlig neu definieren müssen. <br /> <br /><a href="https://arxiv.org/abs/2608.16753" target="_blank">https://arxiv.org/abs/2608.16753</a></span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Corbi</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 10. Sep 2026 01:17<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"></span><table width="90%" cellspacing="1" cellpadding="3" border="0" align="center"><tr> <td><span class="genmed"><b>TomS hat Folgendes geschrieben:</b></span></td> </tr> <tr> <td class="quote">Ich sehe immer nicht nicht, dass KI mehr kann als lose Enden zusammenzufügen, die ihm über das Training und den Prompt bekannt werden. Insofern hilft sie uns bei den einfacheren Sachen, damit wir mehr Zeit für die wirklich schwierigen haben (ich habe das in den 90ern mitgemacht, als man Mathematica etc. eingeführt hat; das hilft, niemand ist darüber traurig)</td> </tr></table><span class="postbody"> <br /> <br />Aber ist das nicht ein Verdrängungsmechanismus, selbst jetzt wo scheinbar eines der größten Probleme der Mathematik durch KI gelöst wurde, ihre Fähigkeiten herunterzuspielen? <br /> <br />Oder kannst du das näher erläutern warum es sich nur um "ein Zusammenfügen loser enden" handeln soll?</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>TomS</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 09. Sep 2026 16:23<span class="gen"> </span> Titel: </span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Ich sehe immer nicht nicht, dass KI mehr kann als lose Enden zusammenzufügen, die ihm über das Training und den Prompt bekannt werden. Insofern hilft sie uns bei den einfacheren Sachen, damit wir mehr Zeit für die wirklich schwierigen haben (ich habe das in den 90ern mitgemacht, als man Mathematica etc. eingeführt hat; das hilft, niemand ist darüber traurig)</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row2"><span class="name"><a name=""></a><b>Werkzeuge</b></span></td> <td class="row2" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 09. Sep 2026 15:33<span class="gen"> </span> Titel: Re: Ersetzt KI Physiker, Mathematiker und Ingenieure?</span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody">Vor dem Buchdruck konnte schon die physische Reproduktion eines komplizierten Textes erhebliche menschliche Arbeit erfordern. Danach wurde diese Arbeit billig, ohne dass deshalb Autoren, Theologen oder Gelehrte verschwanden. Ihr relativer Wert verschob sich. <br /> <br />Bei Computern geschah dasselbe mit dem Rechnen. Niemand würde heute argumentieren, ein Physiker sei „nur noch Kontrollorgan“, weil Mathematica eine Ableitung berechnet, ein FEM-Programm Millionen Gleichungen löst oder ein Compiler Maschinenbefehle erzeugt. Ein Ingenieur berechnet eine Tragstruktur schließlich auch nicht deshalb weniger ingenieurmäßig, weil er keine Steifigkeitsmatrix mit Papier und Bleistift invertiert. <br /> <br />Und bei produktionsnahen Berufen ist diese Entwicklung tatsächlich viel älter. Werkzeugmaschinen, NC/CNC, SPS, industrielle Regelungstechnik, CAD/CAM, Roboter usw. haben ganze Klassen manueller Tätigkeiten automatisiert. Dort hat man längst gelernt, dass Automatisierung nicht dasselbe ist wie Abschaffung der Disziplin. <br /> <br />Das Interessante am jetzigen Schritt ist nur, dass Automatisierung erstmals sehr weit in den Bereich vordringt, den akademische Berufe lange für ihr eigentliches Alleinstellungsmerkmal hielten: kognitive Sucharbeit. <br /> <br />Deshalb würde ich auf "der Ingenieur verkommt zum Kontrollorgan" sogar ziemlich entschieden widersprechen. Kontrolle ist nur dann eine Dequalifizierung, wenn der Mensch nichts anderes mehr entscheidet. Ein guter Ingenieur entscheidet aber Anforderungen, Randbedingungen, Sicherheitsmargen, Modellgültigkeit, Zielkonflikte und letztlich, ob überhaupt das richtige Problem gerechnet wurde. Ein perfekter Solver löst auch ein falsch formuliertes Problem perfekt. <br /> <br />Das Navier–Stokes-Ereignis illustriert gerade diesen Unterschied sehr schön. OpenAI hat am 8. September 2026 einen KI-generierten Lösungsanspruch einschließlich Lean-Formalisierung veröffentlicht. Trotzdem führt Clay Navier–Stokes am 9. September weiterhin unter den ungelösten Millenniumproblemen. Das Ergebnis muss also erst unabhängig mathematisch geprüft werden. <br /> <br />Und selbst wenn es vollständig korrekt ist, hat die KI etwas ganz Bestimmtes geleistet: <span style="font-weight: bold">Menschen hatten ihr bereits ein extrem präzises Problem gegeben.</span></span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> <tr> <td width="22%" align="left" valign="top" class="row1"><span class="name"><a name=""></a><b>Nachdenklich</b></span></td> <td class="row1" height="28" valign="top"><table width="95%" border="0" cellspacing="0" cellpadding="0"> <tr> <td width="95%"><img src="templates/subSilver/images/icon_minipost.gif" width="12" height="9" alt="Beitrag" title="Beitrag" border="0" /><span class="postdetails">Verfasst am: 09. Sep 2026 12:23<span class="gen"> </span> Titel: Ersetzt KI Physiker, Mathematiker und Ingenieure?</span></td> </tr> <tr> <td colspan="2"><hr /></td> </tr> <tr> <td colspan="2"><span class="postbody"><span style="font-weight: bold">Meine Frage:</span><br />Hallo!<br /><br />Ich hätte mal eine Frage an die Physiker, Mathematiker und Ingenieure hier. <br />Und zwar: wie motiviert ihr euch noch im Zeitalter von Ki und co., interessiert und motiviert bei euren Wissenschaften zu bleiben bzw. wie geht ihr damit um, in Konkurrenz zu diesen Systemen zu stehen?<br /><br />Die Frage kam bei mir auf, da ja ein KI System anscheinend das Milleniumproblem zu der Navier Stokes Gleichung gelöst hat.<br /><br /><span style="font-weight: bold">Meine Ideen:</span><br />Ich persönlich finde es interessant und frustrierend zugleich.<br />Ich bin erstaunt, dass solch ein Problem durch KI gelöst wurde, ich hätte es nicht gedacht, dass es so kommt. Auf der anderen Seite ist es doch einfach traurig, dass der Mensch durch die Maschine auch in diesen Bereichen ersetzt wird.<br />Ich persönlich bin "nur" Ingenieur, aber auch in diesem Bereich finde ich es traurig, dass der Ingenieur zum Kontrollorgan verkommt und die Entwicklungsarbeit immer mehr durch KI Tools erfolgt.<br /><br />Wie ergeht es euch?</span></td> </tr> </table></td> </tr> <tr> <td colspan="2" height="1" class="spaceRow"><img src="templates/subSilver/images/spacer.gif" alt="" width="1" height="1" /></td> </tr> </table>
Registrieren
Login
FAQ
Suchen
