exppiiisneg1

@tomkalei Entschuldige, wenn das bei dir so angekommen ist. Mir gehts tatsächlich um die Sache, mich hätte es sehr interessiert, wenn du inhaltliche Gründe hättest - z.B. "ITP+LLM wird Matheforschung nicht gross verändern, weil ..., deshalb habe ich es im podcast nicht erwähnt". Jetzt habe ich verstanden, dass es dir um das adressierte Publikum ging, das du nicht überfordern wolltest. Danke, das wollte ich wissen und dafür habe ich einen Account angelegt, ja.

@tomkalei In 1 1/2 h podcast kommt das Thema gar nicht vor. Das offenbart für mich schon, dass das für dich, den Mathematiker der Runde, nicht so wichtig sein kann. Und bei 500 Zeichen hatte ich dann keinen Platz mehr für eine differenziertere Einordnung als "keine Rolle". Die Kombination mit ITP könnte der Gamechanger für LLMs in der math. Forschung sein, das sollte bei einem Podcast zu LLMs in den Wissenschaften mit einem Mathematiker als Gast imho nicht fehlen.

@tomkalei Beweisprüfer (kurz ITP, insb. Lean) sind immer mehr im kommen. Es gibt einige namhafte Mathematiker:innen, die gerade Lean auch in ihrer Forschung einsetzen. Terance Tao macht das und er prophezeit, dass Lean im Zusammenhang mit LLMs zu einer Art "vibe coding" mathematischer Beweise führt. Erst letzten Oktober wurde so ein formaler Beweis mit ChatGPT für ein 1000$-Erdős-Problem gefunden und auf arXiv gestellt: https://arxiv.org/abs/2510.19804v1 Wieso spielt ITP+LLM für dich offenbar keine Rolle?