Mange av oss føler intuitivt at matematikken kommer til å endre seg, så la oss pakke ut de sannsynlige utfallene uten å ty til overdrivelser eller doomerisme.

Hypotese #1: Antallet matematiske bevis og den samlede mengden matematiske data vil øke eksponentielt. Denne er kanskje ukontroversiell. AI-modeller, under ledelse av mennesker, lager allerede store mengder matematikk. Nå har flaskehalsen gått fra å lage matematikk til å verifisere dens riktighet. Aristoteles, som bruker @leanprover, løser verifiseringsproblemet ved å gjøre hvert bevis maskinkontrollerbart. Etter hvert som teknologien forbedres, vil lengden og kompleksiteten på de lagde bevisene fortsette å øke.

Hypotese #2. Det vil være dramatisk flere matematikere om 10 år enn det er i dag. Ved å automatisere det slitsomme arbeidet med verifisering og bevise enkle lemmaer, kan Aristoteles ikke bare fremskynde arbeidet til høyt sofistikerte profesjonelle matematikere, men også senke terskelen for andre til å bidra. Blant våre beta-API-brukere er pensjonerte programvareingeniører, advokater, militærpersonell, studenter og mange andre som har matematiske ideer eller oppfinnsomhet, men som trenger hjelp med formalismen og trenger noen til å verifisere ideene deres. Vi bør forvente at disse trendene vil akselerere.

Hypotese #3. Mennesker vil forbli i sentrum for matematisk forskning. Dette er den store. Hvis vi ser tilbake gjennom historien – har vi alltid endret definisjonen av matematikk til å være det maskiner ikke kan automatisere. En stor del av en matematikers arbeid tidlig på 1800-tallet var å løse ligninger. Men tidlige kalkulatorer automatiserte mye av dette rutinemessige arbeidet, noe som frigjorde matematikere til å gjøre mer kreativt/abstrakt arbeid. I overskuelig fremtid tror vi at AI vil være det samme. Matematikere vil bruke mindre tid på å verifisere korrekthet og bevise enkle lemmaer, og verktøy som Aristoteles vil hjelpe dem å bruke tid på å utforske dypere konsepter. Etter hvert, etter hvert som Aristoteles blir mer dyktig, vil matematikere styre Aristoteles, og det vil være som å ha et team av ekstremt talentfulle og grundige matematiske samarbeidspartnere til disposisjon, hvor du kan peke dem i ulike retninger og de kan utforske de matematiske grensene. Uansett er vi forbi tavle- og sofafasen i matematikken. Det er nå fullt digitalt, samarbeidsbasert og AI-basert.