correcte opmerking. ja, ik ben sceptisch dat LLM's nieuwe, inzichtelijke wiskunde zullen creëren, omdat dat OOD-denken vereist, waar ze slecht in zijn. maar LLM's kunnen zeer moeilijke wiskundige *problemen* oplossen (dat is anders), wat echt cool is - zolang ze geen "nieuwe, inzichtelijke definities" vereisen. sommige wiskundige problemen vereisen "nieuwe, inzichtelijke definities", en ze zijn specifiek moeilijk om die reden. het is nooit zo dat ze inherent "zwaar" zijn in een computationele zin, maar dat ze "verbeelding" en "creativiteit" vereisen om wonderlijke structuren te conceptualiseren die nog nooit eerder zijn bekeken. bijvoorbeeld, het bewijs van Fermat's Laatste Stelling vereiste de ontwikkeling van volledig nieuwe wiskundige machines - elliptische krommen, modulaire vormen en de Taniyama-Shimura-conjectuur - concepten die niet bestonden toen het probleem voor het eerst werd gesteld. dus, als we LLM's in 1650 hadden, hoe hard ze ook hun best deden om FLT op te lossen - zelfs als je het eeuwenlang zou laten rekenen - zou het dat nooit kunnen doen, omdat het zou denken binnen de kaders van de wiskundige structuren die toen bestonden, en er is letterlijk geen pad naar een oplossing. nu, de dag dat LLM's echt nieuwe wiskundige structuren beginnen uit te vinden, dat is wanneer ze in staat zullen zijn om "moeilijke" stellingen te bewijzen. dat is het enige en enige ding dat hen scheidt van het kunnen doen. nu, dit stelt de moeilijkste vraag bloot: wat is zelfs een "nieuwe, inzichtelijke wiskundige concept"? hoe kan dat zelfs gedefinieerd worden? veel dingen tellen als een "nieuw concept". Ik kan gemakkelijk wat willekeurige woorden in Lean schrijven, en ik heb een volledig nieuw wiskundig concept gemaakt dat nog nooit eerder is gemaakt. en LLM's kunnen dat ook. dat is eenvoudig genoeg. de "inzichtelijke" kant is wat hier belangrijk is. wat maakt iets "inzichtelijk" of "interessant"? waarom zijn complexe getallen interessanter dan willekeurige definities? hoe meten we objectief hoe inzichtelijk een Lean-definitie is?