corretto. sì, sono scettico sul fatto che gli LLM possano creare nuova matematica perspicace, perché ciò richiede un pensiero OOD, in cui sono scarsi. ma gli LLM possono risolvere problemi matematici molto difficili (questo è diverso), il che è davvero interessante - purché non richiedano "nuove definizioni perspicaci". alcuni problemi matematici richiedono "nuove definizioni perspicaci", e sono difficili proprio per questo. non è mai che siano intrinsecamente "pesanti" in un certo senso computazionale, ma che richiedono "immaginazione" e "creatività" per concettualizzare strutture meravigliose che nessuno ha mai esaminato prima. ad esempio, la dimostrazione dell'Ultimo Teorema di Fermat ha richiesto lo sviluppo di un'intera nuova macchina matematica - curve ellittiche, forme modulari e la congettura di Taniyama-Shimura - concetti che non esistevano quando il problema fu posto per la prima volta. quindi, se avessimo avuto LLM nel 1650, non importa quanto duramente cercassero di risolvere FLT - anche se li lasciassi calcolare per secoli - non sarebbero mai stati in grado di farlo, perché penserebbero all'interno delle strutture matematiche che esistevano all'epoca, e non c'è letteralmente alcun percorso verso una soluzione. ora, il giorno in cui gli LLM inizieranno a inventare strutture matematiche genuinamente nuove, è allora che saranno in grado di dimostrare teoremi "difficili". questa è l'unica cosa che li separa dalla possibilità di farlo. ora, questo espone la domanda più difficile: che cos'è anche un "nuovo concetto matematico perspicace"? molte cose contano come un "nuovo concetto". posso facilmente scrivere alcune parole a caso in Lean, e avrei creato un concetto matematico completamente nuovo che nessuno ha mai creato prima. e anche gli LLM possono farlo. è abbastanza facile. la parte "perspicace" è ciò che conta qui. cosa rende qualcosa "perspicace" o "interessante"? perché i numeri complessi sono più interessanti di definizioni casuali? come possiamo misurare oggettivamente quanto sia perspicace una definizione in Lean?