🎀 Terence Tao samarbetar med Math, Inc. 🎀 som den första Veritas Fellow — för att formalisera uppskattningar inom talteori. Inom analytisk talteori innehåller litteraturen ett stort nätverk av explicita uppskattningar. Men det nätet är inte omedelbart interoperabelt. I praktiken kommer resultaten i tre lager: Primära skattningar: Dessa är grundläggande indata såsom nollfria regioner för Riemanns zetafunktion. De är ofta beroende av omfattande beräkningar och noggrann numerisk optimering. Sekundära skattningar: Många artiklar tar en primär input (t.ex. ett nollfritt område) och omvandlar den till återanvändbara konsekvenser, såsom att räkna primtal i korta intervall. Dessa blir grundläggande byggstenar som används i hela ämnet. Tertiära skattningar: Vidare arbete tillämpar sedan dessa sekundära byggstenar på gränstalteoretiska problem, t.ex. genom att representera heltal som summor av tre primtal. Problemet är att dessa lager inte uppdateras rent över tid. En tertiär artikel kan förlita sig på den bästa primära uppskattningen som finns tillgänglig vid tillfället. Men år senare förfinar förbättrade beräkningar primärindatan, utan att systematiskt spridas genom sekundär- och tertiärkedjan. Som ett resultat är "samma sats med uppdaterade konstanter" ofta okänd. Målet är att formalisera nyckelartiklar över dessa lager och sedan abstrahera dem så att deras beroenden blir explicita, komponerbara och maskinkontrollerbara. Den långsiktiga visionen är att skapa ett levande nätverk av konsekvenser: när en primär uppskattning förbättras uppgraderas varje nedströms implikation automatiskt. Detta kommer att omvandla den matematiska litteraturen till modulär mjukvara. Talteori är ett starkt testfall eftersom dess uppskattningar har en relativt tydlig struktur och en gemensam uppsättning standardindata och utdata. Men inom många områden som PDE:er lägger forskare ständigt ner arbete på modifiering: att anpassa lemmor och hypoteser, översätta mellan inkompatibla ramverk, "passa fyrkantiga pinnar i runda hål." Ett komponerbart, maskinverifierat implikationsnätverk riktar sig direkt mot denna friktion. Samma infrastruktur är redo att skalas till andra områden och möjliggöra storskaliga, crowdsourcade projekt som för närvarande är svåra att samordna. Ett klassiskt exempel är klassificeringen av ändliga enkla grupper: en decennielång insats fördelad på många bidragsgivare, med oundviklig komplexitet kring bokföring, integration och förtroende för fullständighet. Med moderna verktyg föreställer vi oss att ta itu med månbanor av liknande omfattning: många bidragsgivare som hanterar olika fall och automatiserade system som binder ihop bitarna. Fältet blir en live-framstegsdashboard som registrerar vad som bevisas, vad som återstår och exakt vilka beroenden varje komponent kräver. Detta öppnar upp för ett mycket snabbare och engagerande sätt att göra matematik. Titta på Taos översikt på YouTube:

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)

🚨 HELA SAMTALET Fields-medaljören Terry Tao sätter sig ner med Math Inc:s @jessemhan och @jdlichtman för ett samtal om matematikens framtid. "Jag blev övertygad om att detta var matematikens framtid [...] Det är en annan stil att skriva bevis som faktiskt på vissa sätt är lättare att läsa – svårare att kontrollera för människor, men man ser tydligare in- och utdata i ett bevis, vilket traditionellt skrivande ofta döljer [...] Jag tror att definitionen av matematiker kommer att breddas."