poprawne podejście. tak, jestem sceptyczny co do tego, że LLM-y stworzą nową, wnikliwą matematykę, ponieważ wymaga to myślenia poza schematami, w czym są słabe, więc to jest dobry argument moim zdaniem. ale LLM-y potrafią rozwiązywać bardzo trudne *problemy* matematyczne (to coś innego), co jest naprawdę fajne - o ile nie wymagają "nowej, wnikliwej matematyki" niektóre problemy matematyczne wymagają nowych, wnikliwych definicji, i 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 by się starały rozwiązać FLT - nawet jeśli pozwolilibyśmy im obliczać przez wieki - nigdy by tego nie zrobiły, 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 to zrobić. teraz pojawia się najtrudniejsze pytanie: cóż, co to w ogóle jest "nowa, wnikliwa koncepcja matematyczna"? jak to w ogóle można zdefiniować? wiele rzeczy liczy się jako "nowa koncepcja". Mogę łatwo napisać kilka losowych słów w Lean, a stworzę zupełnie nową koncepcję matematyczną, której nikt wcześniej nie stworzył. i LLM-y mogą to zrobić również. to wystarczająco łatwe. część "wnikliwa" jest tutaj najważniejsza. co sprawia, że coś jest "wnikliwym" lub "interesującym"? dlaczego liczby zespolone są bardziej interesujące niż losowe definicje? jak możemy obiektywnie zmierzyć, jak wnikliwa jest definicja w Lean?