Kymmenen edistysaskelta matematiikassa ja teoreettisessa tietojenkäsittelytieteessä

Haluamme tarjota tutkijoille ja matemaatikoille työkaluja, jotka nopeuttavat uusien löytöjen tekemistä. Siksi julkistimme hiljattain ChatGPT:n akateemisille tutkijoille⁠. Aloite tarjoaa 100 000 tutkijalle ja matemaatikolle maksuttoman pääsyn parhaisiin ChatGPT‑malleihimme. Arvioimme mallejamme myös niiden kehityksen aikana avoimilla tutkimusongelmilla.

Toukokuussa julkaisimme tekoälyn tuottaman vastaesimerkin⁠ Erdősin yksikköetäisyyskonjektuurille. Se löydettiin arvioitaessa julkaisematonta mallia. Tämä työ on jo innoittanut jatkokehitystä matematiikassa ja teoreettisessa tietojenkäsittelytieteessä¹. Julkaisemme tänään kymmenen tulosta, joista jokainen ratkaisee pitkään avoimena olleen ongelman tai edistää merkittävästi sen ratkaisemista. Ongelmat liittyvät korkeaulotteiseen geometriaan, koodausteoriaan, aritmeettisten piirien vaativuuteen, ryhmäteoriaan, operaattorialgebroihin, kvanttivaativuuteen, hilakryptografiaan ja ekstremaaliseen kombinatoriikkaan. Kaikki nämä ongelmat ovat erittäin merkittäviä omille matematiikan tutkimusyhteisöilleen, ja useat niistä kiinnostavat laajasti koko matematiikan alaa.

Esittelemme uusia tuloksia seuraaviin ongelmiin. Tulokset saavutti seuraavan merkittävän mallimme Astran sisäinen versio. Näiden ongelmien ratkaisujen löytämiseen tarvittu tokenien kokonaismäärä maksaisi Sol API:n hinnoilla noin 2 000 dollaria. Sen jälkeen ihmiset muokkasivat perustelut käsikirjoituksiksi saman mallin avulla. Tämän jälkeen malli formalisoi jokaisen perustelun Lean-varmenteeksi⁠(avautuu uudessa ikkunassa). Julkaisemme kustakin ratkaisusta myös mallin kuvauksen omasta ajatteluprosessistaan.

1. Korkeaulotteinen pallopakkaus. Uusia ylärajoja pallopakkauksen tiheydelle aina Cohnin–Elkiesin kynnykseen asti.
2. Binääriset ja pallokoodit: Eksponentiaalisesti paremmat rajat binäärikoodien enimmäiskoolle millä tahansa määrätyllä vähimmäisetäisyydellä sekä vastaavat tulokset korkeaulotteisille pallokoodeille.
3. Ei-sofiset ryhmät. Konstruktio, joka osoittaa ei-sofisten ryhmien olemassaolon ja vastaa ryhmäteorian keskeiseen avoimeen kysymykseen.
4. Connesin jäykkyyskonjektuuri. Vastaesimerkki pitkään avoimena olleelle konjektuurille, jonka mukaan tietyt ryhmät määräytyvät yksikäsitteisesti von Neumannin algebrojensa perusteella.
5. Aritmeettisten piirien vaativuus. Uusia alarajoja permanentin laskemiselle aritmeettisilla piireillä ja kaavoilla, mukaan lukien kertalukua n⁴/log n oleva aritmeettisten kaavojen alaraja.
6. Kvanttirinnakkaistoisto. Eksponentiaalinen rinnakkaistoistolause yleisille kahden pelaajan kvanttipeleille. Se laajentaa klassisen vaativuusteorian keskeistä periaatetta.
7. Lähimmän vektorin ongelma. Polynomikertoiminen approksimoinnin vaikeustulos lähimmän vektorin ongelmalle, joka on kvanttien jälkeiseen kryptografiaan liittyvä keskeinen hilaongelma.
8. Ehrhartin tilavuuskonjektuuri. Sellaisen konveksin kappaleen suurimman mahdollisen tilavuuden määrittäminen kaikissa ulottuvuuksissa, jonka ainoa sisäinen hilapiste on sen painopiste.
9. Moniväriset Ramseyn luvut. Ylieksponentiaalinen alaraja monivärisille kolmioiden Ramseyn luvuille, mikä ratkaisee Erdősin ongelman 183.
10. Ekstremaalilukuja koskevat konjektuurit. Tuloksia ekstremaalisen graafiteorian kompaktisuus- ja degeneroituneisuuskonjektuureista, jotka ratkaisevat Erdősin ongelmat 146 ja 180.

Matemaattiseen tutkimukseen osallistumaan kykenevien järjestelmien ilmaantuminen herättää kysymyksiä, joihin teknologiayritys ei voi vastata yksin. Tekoälyn roolista matematiikassa on monia näkemyksiä. Arvostamme syvästi niitä, jotka ovat huolissaan sen vaikutuksista, ja ymmärrämme heidän näkökantojaan. Heihin lukeutuvat myös tekoälyä ja matematiikkaa koskevan Leidenin julistuksen⁠(avautuu uudessa ikkunassa) allekirjoittajat. Tekijätietojen tulisi mielestämme kuvata rehellisesti, miten tulos on tuotettu. Kokonaan tekoälyjärjestelmän tuottaman todistuksen ilmoittaminen ihmisen laatimaksi antaisi väärän kuvan sekä järjestelmän panoksesta että aidon inhimillisen ajattelutyön luonteesta. Autoimme käsikirjoitusten valmistelussa ja todistusten formalisoinnissa Leanilla ja vastaamme niiden oikeellisuudesta. Matemaattiset perustelut tuotti kuitenkin järjestelmämme. Toivomme matematiikan tutkimusyhteisön perehtyvän tuloksiin perusteellisesti, asettavan ne oikeaan yhteyteen ja kehittävän niiden taustalla olevia ideoita edelleen uuden tutkimuksen ja uusien löytöjen avulla.

Kun tekoälyjärjestelmistä kehittyy yhä edistyneempiä tutkimuskumppaneita, niiden laajan saatavuuden varmistaminen on olennaisen tärkeää. Näin voimme tukea tutkijoita ja matemaatikkoja, kun he suunnistavat tällä mullistavalla aikakaudella ja määrittelevät alojensa tulevaisuutta.