Här är en viktig fråga som vi alltmer måste hantera i takt med att AI-för-matematik-pipelines blir allt vanligare: Varför bryr vi oss om att lösa svåra problem? Nästan alltid är svaret *inte* för att vi särskilt vill att det svåra problemet ska lösas. (1/12)

Frågor som förekomsten av globalt släta lösningar till Navier-Stokes-ekvationerna är av matematiskt intresse inte för att svaret i sig är oerhört viktigt, utan för att vi har anledning att tro att processen att *upptäcka* svaret är mycket sannolik... (2/12)

... för att ge djupa nya insikter inom analys, PDE:er, strömningsdynamik med mera, med nya tekniker att utnyttja. Att lösa Fermat gav oss (indirekt) Langlands-programmet. Att lösa Poincaré gav oss Ricci-flöde. Man hoppas att lösningen av Navier-Stokes ger oss något lika monumentalt. (3/12)

Faktum är att vi identifierar sådana problem som "intressant svåra" just för att vi intuitivt känner att de representerar en "lucka" i vår nuvarande förståelse och metoder. Det är därför galningar som påstår sig lösa (säg) Riemannhypotesen med "trick" eller elementära metoder... (4/12)

... missar något poängen: om ett av dessa stora problem visade sig vara lösbart med endast befintliga matematiska insikter och teknik, skulle det vara en enorm besvikelse: en källa som vi tidigare trodde forsade är faktiskt torr. (5/12)

Vad har detta med AI att göra? Om man accepterar premissen att svåra problem mestadels är intressanta på grund av de nya insikter och förståelser de ger, väcker det frågan (med tanke på AI-utvecklingen): vem är ansvarig för "förståelsen"-delen? (6/12)

Ta bevis genom utmattning (som i fyrfärgssatsen), som länge har betraktats som något kontroversiella, eftersom de levererar "epistemisk säkerhet"-delen av ett bevis, utan att nödvändigtvis ge någon del av "insikts"-delen (vilket vanligtvis är det vi bryr oss om) (7/12)

Som sådan är bevis genom utmattning definitivt inte "fel", men de är på något sätt "fuskande" eller kanske "självdestruktiva": de stänger ner ett potentiellt fruktbart problem, samtidigt som de utelämnar just de aspekter av matematiken som gör det intressant och meningsfullt att göra. (8/12)

Jag anser att AI-genererade bevis, i avsaknad av någon nivå av förståelse eller insikt från den som skapade dem, bör betraktas i ungefär samma anda. Om du autogenererar ett Lean-bevis av en stor sats är det toppen! Men varför gjorde du det? (9/12)

Om du inte förstår de nya insikterna/metoderna som beviset innehåller, har du bara flyttat den intellektuella bördan från dig själv till den som är beredd att läsa och förstå den (och förhoppningsvis kommunicera insikterna till andra). (10/12)

Matematik är i slutändan en mänsklig kulturell artefakt (förmodligen vår djupaste, rikaste och äldsta). Att lösa svåra problem var bara tänkt att vara en *proxy* för att förlänga den artefakten. AI gör det spännande enkelt att skapa nya vägar för matematisk förståelse.. (11/12)

... inom den artefakten, men det gör det också lättare än någonsin att uppnå proxyn (dvs. lösa svåra problem), samtidigt som hela anledningen till varför vi brydde oss från början (dvs. fördjupar vår förståelse). Snälla, gör inte det. (12/12)