Ti fremskridt inden for matematik og teoretisk datalogi

Vi vil give forskere og matematikere værktøjer, der sætter fart på nye opdagelser. Derfor annoncerede vi for nylig ChatGPT til akademiske forskere⁠, et initiativ, der giver 100.000 forskere og matematikere gratis adgang til vores bedste ChatGPT‑modeller. Vi fortsætter også med at evaluere vores modeller på uløste forskningsproblemer under udviklingen.

I maj offentliggjorde vi et AI-genereret modbevis⁠ af Erdős' formodning om enhedsafstande, som blev fundet under evalueringen af en endnu ikke udgivet model. Dette arbejde har allerede inspireret til yderligere fremskridt inden for matematik og teoretisk datalogi¹. I dag præsenterer vi ti udvalgte resultater, som hver især løser eller skaber væsentlige fremskridt med et uløst problem, der har bestået i mange år. Problemerne spænder over højdimensionel geometri, kodningsteori, aritmetisk kredsløbskompleksitet, gruppeteori, operatoralgebraer, kvantekompleksitet, gitterkryptografi og ekstremal kombinatorik. Alle problemerne har stor betydning for deres respektive matematiske fagmiljøer, og flere af dem har bred interesse på tværs af matematikken som helhed.

Vi fremlægger nye resultater for følgende problemer. Resultaterne blev opnået af en intern version af Astra, vores næste store model. Det samlede antal tokens, der skulle bruges til at finde løsninger på disse problemer, ville koste omkring 2.000 USD til Sol API's priser. Derefter udarbejdede mennesker argumenterne som manuskripter ved hjælp af den samme model. Efterfølgende formaliserede modellen hvert argument i et Lean-certifikat⁠(åbner i et nyt vindue). For hver løsning offentliggør vi også en models redegørelse for sin tankeproces.

1. Pakning af kugler i høje dimensioner. Nye øvre grænser for kuglepakningstæthed helt ned til Cohn-Elkies-tærsklen.
2. Binære og sfæriske koder: Eksponentielt forbedrede grænser for den maksimale størrelse af binære koder ved enhver foreskrevet minimumsafstand med tilsvarende resultater for højdimensionelle sfæriske koder.
3. Ikke-sofiske grupper. En konstruktion, der fastslår eksistensen af ikke-sofiske grupper og dermed behandler et centralt uløst spørgsmål i gruppeteorien.
4. Connes' rigiditetsformodning. Modbevis af en mangeårig formodning om, at bestemte grupper entydigt bestemmes af deres von Neumann-algebraer.
5. Aritmetisk kredsløbskompleksitet. Nye nedre grænser for beregning af permanenten ved hjælp af aritmetiske kredsløb og formler, herunder en nedre grænse for aritmetiske formler af størrelsesordenen n⁴/log n.
6. Parallel kvantegentagelse. En sætning om eksponentiel parallel gentagelse for generelle kvantespil med to spillere, som udvider et grundlæggende princip fra klassisk kompleksitetsteori.
7. Problemet med den nærmeste vektor. Approksimationshårdhed med en polynomiel faktor for problemet med den nærmeste vektor, et grundlæggende gitterproblem med relation til postkvantekryptografi.
8. Ehrharts volumenformodning. Bestemmelse i enhver dimension af det størst mulige volumen for et konvekst legeme, hvis tyngdepunkt er dets eneste indre gitterpunkt.
9. Flerfarvede Ramsey-tal. En supereksponentiel nedre grænse for flerfarvede trekant-Ramsey-tal, som løser Erdős-problem 183.
10. Formodninger om ekstremaltal. Resultater om kompaktheds- og degenerationsformodningerne i ekstremal grafteori, som løser Erdős-problem 146 og 180.

Fremkomsten af systemer, der kan bidrage til matematisk forskning, rejser spørgsmål, som en teknologivirksomhed ikke kan besvare alene. Der er mange holdninger til AI's rolle i matematikken, og vi har stor respekt og forståelse for dem, der er bekymrede over dens konsekvenser, herunder underskriverne af Leiden-erklæringen om AI og matematik⁠(åbner i et nyt vindue). Vi mener, at krediteringen ærligt bør afspejle, hvordan et resultat er frembragt: At hævde menneskeligt forfatterskab til et bevis, der udelukkende er genereret af et AI-system, ville give et forkert billede af både systemets bidrag og karakteren af ægte menneskeligt intellektuelt arbejde. Vi bidrog til at udarbejde manuskripterne og formalisere beviserne i Lean og tager ansvar for deres korrekthed, mens de matematiske argumenter selv blev genereret af vores system. Vi håber, at det matematiske fagmiljø vil gå grundigt ind i disse resultater, sætte dem i perspektiv og give idéerne bag dem liv gennem ny forskning og nye opdagelser.

I takt med at AI-systemer udvikler sig til mere avancerede forskningspartnere, er bred adgang afgørende for at støtte forskere og matematikere, mens de navigerer i og former fremtiden for deres fagområder i denne omvæltende tid.