Axiom Mathin tekoäly vahvistaa 246 alkulukuvälin teoreeman Leanissa

Axiom Math sanoo, että sen AxiomProver-järjestelmä on tuottanut koneellisesti tarkistetun Lean 4 -todistuksen vahvimmasta tunnetusta tuloksesta alkulukujen välisten aukkojen osalta: teoreeman, jonka mukaan äärettömän monia alkulukupareja eroaa enintään 246:lla. Yritys julkaisi tuloksen 17. elokuuta 2026 interaktiivisena formalisaatiopiirustuksena, johon on merkitty 41 nimeä mainittua matemaattista, insinööri- ja päätutkijatoimijaa, ja IEEE Spectrum raportoi ensin tästä virstanpylväästä.

246 raja on nykyinen ihmistiedon raja pitkän hyökkäyksen aikana kaksosalkuluku‑hypoteesia vastaan, 1800‑luvun hypoteesia, jonka mukaan alkuluvut, jotka eroavat täsmälleen kahdella, toistuvat ikuisesti. Axiom Mathin projektisivu kuvaa työtä yhtenäisenä formalisaationa James Maynardin vuonna 2013 julkaistusta artikkelista “Small gaps between primes” sekä Polymath8b‑yhteistyön jatkosta, joka tiivisti Maynardin 600‑rajan 246:een. Koneellisesti tarkistetut todistukset on järjestetty julkiseen Lean‑kirjastoon, PrimeGapsLibiin, jossa 246‑teoreema on sen lippulaivatuloksena.

“Tämä teoreema edustaa tällä hetkellä ihmistiedon kynnystä alkuluvuista,” sanoi Ken Ono, Axiom Mathin perustajamatemaatikko.

Formaalinen varmistus tarkoittaa todistuksen kääntämistä kielelle, jonka pieni, luotettu ohjelma, jota kutsutaan ytimeksi, voi tarkistaa rivi riviltä. Tulosta ei voida pitää absoluuttisena takuutena — väittämän täytyy itse olla käännetty oikein, ja tarkistajan on oltava luotettava — mutta se poistaa ihmisen tuomarin virheellisyyden ketjusta. Tähän mennessä tekoälyjärjestelmiä, jotka kilpailevat matematiikan mittareilla, on enimmäkseen mitattu kilpailuongelmilla, joilla on lyhyet, itsenäiset todistukset; näiden tulosten ja tutkimustason formalisaation välinen kuilu on ollut suuri, mikä näkyy aiemmissa järjestelmissä, jotka menestyivät olympia‑geometriassa samalla kun tutkimusmatematiikka jäi pitkälti koskemattomaksi.

70 miljoonasta 246:een

Itse konjektuuri, jonka Alphonse de Polignac tarkasti muotoili 1800‑luvulla, on edelleen todistamaton. Ensimmäinen minkä tahansa tyyppinen äärellinen raja saatiin vuonna 2013, kun Yitang Zhang todisti, että äärettömän monta alkulukuparia sijoittuu 70 miljoonan sisään toisiinsa. Muutamaa kuukautta myöhemmin Maynard esitteli tarkennetun suodatusmenetelmän ja leikkasi rajan 600:een — työ, joka osaltaan toi hänelle vuoden 2022 Fields‑medalin — ja Polymath8b‑yhteistyö, johon kuului Maynard ja Terence Tao, työntyi siihen 246:een. Axiom Mathin piirustus esittää tämän kehityksen projektina, jonka se aikoi formalisoida.

Formalisaatio noudattaa putkistoa, jonka yritys kuvaa kolmessa vaiheessa. Tutkijat kirjoittivat ensin todistuksen piirustuksena — jokaiselle määritelmälle, lemmalle ja teoreemalle annettiin tunniste, tarkka väittämä ja luettelo sen riippuvuuksista — tuottaen riippuvuusgraafin, joka järjestää työn. AxiomProver, yrityksen monitoimijajärjestelmä matemaattiseen tutkimukseen formalisoidun todistuksen avulla, loi sitten koneellisesti tarkistettavat Lean 4 -todistukset, jotka perustuvat Mathlibiin, yhteisön matematiikkakirjastoon, sekä PrimeNumberTheoremAnd‑projektiin, joka on Alex Kontorovichin ja Taon johtama olemassa oleva formalisaatiohanke. Axiomin tiimi tarkasteli sitten tuotettua koodia ja järjesteli sen PrimeGapsLibiin.

Kirjaston ilmoitetut päätulokset menevät hieman otsikkoteoreeman ohi. 246‑rajan lisäksi se formalisoituu Maynardin 600‑rajan, ja se sisältää itsenäisen tarkistushaasteen — rakennettu ainoastaan Mathlibiin, ja todistuksen paikka on jätetty tyhjäksi — jonka avulla kuka tahansa Lean‑vertailutyökalun käyttäjä voi itsenäisesti vahvistaa, että kirjaston todistukset vastaavat ilmoitettuja teoreemoja. Yritys varoittaa, että täysi tarkistus voi kestää tunteja; supistettu versio, joka kattaa kaksi muuta tulosta, suoritetaan minuuteissa.

Missä tämä sijoittuu AI‑formalisaatioiden väitteisiin

Tulos sijoittuu vuoteen, jolloin AI‑järjestelmien väitteet tutkimustason matematiikasta kasvavat, ja suurin osa niistä perustuu kilpailupisteisiin tai lyhyisiin todistuksiin. Axiom Math on ollut yksi aggressiivisimmista väittäjistä: AxiomProverille annetaan ansioita aiemmin avoimien ongelmien ratkaisemisesta, mukaan lukien työ, jonka yritys on julkaissut vertaisarvioiduissa lehdissä, ja AI‑järjestelmät ovat nyt ratkaisseet useita pitkään avoimia Erdős‑ongelmia. 246‑formalisaatio on erilaista — se ei ole uusi teoreema, vaan koneellisesti tarkistettu uudelleenrakennus yhdestä nykyaikaisen lukuteorian teknisesti vaativimmista todistuksista.

Lähin vertailu on aiemmin tänä vuonna, kun Math, Inc. käytti Gauss‑agenttiaan muodostaakseen muodollisen todistuksen Maryna Viazovskan Fields‑medalin voittamasta pallopaketointituloksesta dimensioissa 8 ja 24. Sidharth Hariharan, Carnegie Mellon -tohtorintutkija, joka johti ihmisen piirustusponnistuksen kyseisessä formalisaatiossa ja on nyt Axiom Mathin harjoittelija sekä 246‑projektin nimetty matemaattinen avustaja, väittää, että uusi tulos on kattavampi saavutus. Hänen perustelunsa, kuten hän kuvailee, on että Axiom on rakennettu uudelleenkäyttöön: sen sijaan että se olisi kertaluonteinen yhden todistuksen formalisaatio, PrimeGapsLib on ylläpidetty kirjasto alkulukujen aukkojen tuloksista, jonka tarkoitus on tukea tulevaa formalisaatiotyötä ja tutkimusta.

Tämä eroavaisuus vaikuttaa siihen, miten tulosta tulisi lukea. Kertaluonteinen tarkistus osoittaa, että järjestelmä voi selviytyä yhdestä vaikeasta todistuksesta. Kirjasto puolestaan osoittaa jotain lähempänä infrastruktuuria — uudelleenkäytettävää formalisoitua konetta, johon muut tulokset voivat nojata — mikä on suunta, johon formalisoivat todistamisjärjestelmät ovat siirtyneet siirtyessään harjoitusten ratkaisemisesta todellisen matematiikan tarkistamiseen. Kyvykkyysväite perustuu julkisiin ja uudelleenkäytettäviin artefakteihin, ei mittaripisteeseen: piirustukseen, Lean‑koodiin ja vertailuhaasteeseen, jonka on suunniteltu niin, että ulkopuoliset tutkijat voivat itse tarkistaa todistukset.

Ono asettaa matematiikan suuremman pyrkimyksen testialustaksi. Jos ohjelmiston ominaisuudet — kuten ohjelman päättyminen tai sen tulosteen oikeellisuus jokaiselle syötteelle — voidaan ilmaista tarkkoina matemaattisina väitteinä, niin AxiomProverista johdetut järjestelmät voisivat formalisoida ne, hän väittää, osoittaen suuntaa kohti AI‑luodun koodin varmistamista, kun se alkaa ohjata infrastruktuuri-, rahoitus- ja turvallisuusjärjestelmiä.

“Maailma on siirtymässä toimimaan tietokonekoodilla, jota kukaan ei ole lukenut,” sanoi Ono. “AI on täällä, emmekä enää voi sulkea silmiämme — todistusten formalisaatio on testialusta ratkaista, mitä pidän tärkeimpänä AI:n aiheuttamana haasteena, jonka kohtaamme.”

Toistaiseksi toimitus on kapeampi ja tarkistettavissa: 41 tekijän piirustus, julkinen Lean‑kirjasto ja koneellisesti vahvistettu todistus, jonka mukaan 246:n sisällä olevat alkuluvut eivät koskaan loppu – kaksosalkuluku‑konjektuurin lähin vahvistettu naapuri, ja syvin tutkimusmatematiikan osa, jonka AI‑järjestelmä on tähän mennessä tarkistanut alusta loppuun.