Manon Bischoff von Spektrum der Wissenschaft ist zu Gast. Sie hat sich kürzlich an den Endgegner gewagt und zum 1000-seitigen Beweis eines Teils des Langlands-Programms die Titelgeschichte im Spektrum-Heft geschrieben. Wir sprechen über diesen speziellen Beweis und auch mal wieder über die Formalisierung von Mathematik, die den Referees vielleicht irgendwann die mühselige Prüfung der Argumente abnimmt. Und wenn das Prüfen automatisiert ist, kann dann ein LLM ganz viele Beweise schreiben, um vielleicht einen zu finden, der geht?