Många av oss känner intuitivt att matematikens område kommer att förändras, så låt oss analysera de sannolika utfallen utan att ta till överdrifter eller domedagstänk.

Hypotes #1: Antalet matematiska bevis och den totala mängden matematiska data kommer att öka exponentiellt. Den här är kanske okontroversiell. AI-modeller, under ledning av människor, skapar redan stora mängder matematik. Nu har flaskhalsen gått från att skapa matematik till att verifiera dess korrekthet. Aristoteles, som använder @leanprover, löser verifieringsproblemet genom att göra varje bevis maskinkontrollerbart. När teknologin förbättras kommer längden och komplexiteten på de skapade bevisen att fortsätta öka.

Hypotes #2. Det kommer att finnas dramatiskt fler matematiker om tio år än det är idag. Genom att automatisera det tråkiga arbetet med verifiering och bevisa enkla lemman kan Aristoteles inte bara påskynda arbetet för högt sofistikerade professionella matematiker, utan också sänka tröskeln för andra att bidra. Bland våra beta-API-användare finns pensionerade mjukvaruingenjörer, jurister, militärer, studenter och många andra som har matematiska idéer eller uppfinningsrikedom men behöver hjälp med formalismen och behöver någon som verifierar deras idéer. Vi bör förvänta oss att dessa trender accelererar.

Hypotes #3. Människor kommer att förbli i centrum för matematikforskningen. Det här är den stora. Om vi ser tillbaka genom historien – har vi alltid ändrat definitionen av matematik till att vara det som maskiner inte kan automatisera. En stor del av en matematikers arbete i början av 1800-talet var att lösa ekvationer. Men tidiga kalkylatorer automatiserade mycket av detta rutinarbete, vilket frigjorde matematiker att göra mer kreativt/abstrakt arbete. Under överskådlig framtid tror vi att AI kommer att vara likadant. Matematiker kommer att lägga mindre tid på att verifiera korrekthet och bevisa enkla lemma, och verktyg som Aristoteles hjälper dem att ägna sin tid åt att utforska djupare koncept. Så småningom, när Aristoteles blir mer kompetent, kommer matematiker att styra Aristoteles och det kommer att vara som att ha ett team av extremt talangfulla och rigorösa matematiska samarbetspartners till ditt förfogande, där du kan peka dem i olika riktningar och de kan utforska de matematiska gränserna. Hur som helst är vi förbi matematikens fasen med griffeltavla och soffa. Det är nu helt digitalt, samarbetsinriktat och AI-kompatibelt.