@exppiiisneg1@mastodon.social

exppiiisneg1 @exppiiisneg1@mastodon.social

· 9mo ago

Replying to

@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?

arXiv.org

Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof

We resolve a $1000 Erdős prize problem, complete with formal verification generated by a large language model. In over a dozen papers, beginning in 1976 and spanning two decades, Paul Erdős repeatedly posed one of his "favourite" conjectures: every finite Sidon set can be extended to a finite perfect difference set. We establish that {1, 2, 4, 8, 13} is a counterexample to this conjecture. During the preparation of this paper, we discovered that although this problem was presumed to be open

0

1

0

exppiiisneg1 @exppiiisneg1@mastodon.social

· 9mo ago

Replying to

@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.

0

exppiiisneg1 @exppiiisneg1@mastodon.social

· 9mo ago

Replying to

@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.

0

1

0