poprawne podejście. tak, jestem sceptyczny co do tego, że LLM-y stworzą nową, wnikliwą matematykę, ponieważ to wymaga myślenia poza schematami, w czym są słabe. ale LLM-y potrafią rozwiązywać bardzo trudne *problemy* matematyczne (to coś innego), co jest naprawdę fajne - pod warunkiem, że nie wymagają "nowych, wnikliwych definicji". niektóre problemy matematyczne wymagają "nowych, wnikliwych definicji", a są trudne właśnie z tego powodu. nigdy nie jest tak, że są one z natury "ciężkie" w jakimś obliczeniowym sensie, ale że wymagają "wyobraźni" i "kreatywności", aby skonceptualizować wspaniałe struktury, które nikt wcześniej nie badał. na przykład dowód ostatniego twierdzenia Fermata wymagał opracowania całkowicie nowego aparatu matematycznego - krzywych eliptycznych, form modularnych i hipotezy Taniyama-Shimura - koncepcji, które nie istniały, gdy problem został po raz pierwszy postawiony. więc, gdybyśmy mieli LLM-y w 1650 roku, niezależnie od tego, jak bardzo starałyby się rozwiązać FLT - nawet jeśli pozwolilibyśmy im obliczać przez wieki - nigdy by im się to nie udało, ponieważ myślałyby w ramach matematycznych struktur, które istniały wówczas, a dosłownie nie ma drogi do rozwiązania. teraz, w dniu, w którym LLM-y zaczną wynajdować naprawdę nowe struktury matematyczne, wtedy będą mogły udowodnić "trudne" twierdzenia. to jedyna rzecz, która je od tego dzieli. teraz, to stawia najtrudniejsze pytanie: cóż, co to w ogóle jest "nowa, wnikliwa koncepcja matematyczna"? wiele rzeczy liczy się jako "nowa koncepcja". Mogę łatwo napisać kilka losowych słów w Lean, a stworzę całkowicie nową koncepcję matematyczną, której nikt wcześniej nie stworzył. i LLM-y mogą to zrobić również. to wystarczająco łatwe. to "wnikliwa" część jest tutaj najważniejsza. co sprawia, że coś jest "wnikliwego" lub "interesującego"? dlaczego liczby zespolone są bardziej interesujące niż losowe definicje? jak obiektywnie mierzymy, jak wnikliwa jest definicja w Lean?