Peter Scholze haluaa rakentaa uudelleen suuren osan modernista matematiikasta alkaen yhdestä sen kulmakivistä. Nyt hän on saanut vahvistuksen todisteelle hänen etsintänsä ytimessä epätodennäköisestä lähteestä: tietokoneesta.
Vaikka useimmat matemaatikot epäilevät, että koneet korvaavat heidän ammattinsa luovia puolia lähiaikoina, jotkut myöntävät, että tekniikalla tulee olemaan yhä tärkeämpi rooli heidän tutkimuksessaan – ja tämä saavutus voi olla käännekohta sen hyväksymisessä.
Scholze, lukuteoreetikko, esitti kunnianhimoisen suunnitelman – jonka hän loi yhdessä yhteistyökumppaninsa Dustin Clausenin kanssa Kööpenhaminan yliopistosta – luentosarjassa vuonna 2019 Bonnin yliopistossa Saksassa, jossa hän sijaitsee. . Kaksi tutkijaa kutsuivat sitä "tiivistetyksi matematiikaksi", ja he sanovat, että se lupaa tuoda uusia oivalluksia ja yhteyksiä kenttien välille geometriasta lukuteoriaan.
Muut tutkijat kiinnittävät huomiota: Scholzea pidetään yhtenä matematiikan kirkkaimmista tähdistä, ja hänellä on kokemusta vallankumouksellisten käsitteiden käyttöönotosta. Emily Riehl, matemaatikko Johns Hopkins Universitystä Baltimoressa, Marylandissa, sanoo, että jos Scholzen ja Clausenin visio toteutuu, tapa, jolla matematiikkaa opetetaan jatko-opiskelijoille 50 vuoden kuluttua, voi olla hyvin erilainen kuin nykyään. "On monia matematiikan alueita, joihin uskon hänen ideoidensa vaikuttavan tulevaisuudessa", hän sanoo.
Tähän asti suuri osa tästä visiosta perustui tekniseen näyttöön, joka oli niin sekava, että edes Scholze ja Clausen eivät voineet olla varmoja sen oikeellisuudesta. Mutta aiemmin tässä kuussa Scholze ilmoitti, että projekti todisteen ytimen tarkistamiseksi erikoistuneen tietokoneohjelmiston avulla oli onnistunut.
Tietokone-apu
Matemaatikot ovat pitkään käyttäneet tietokoneita numeeristen laskelmien tekemiseen tai monimutkaisten kaavojen käsittelyyn. Joissakin tapauksissa ne ovat osoittautuneet merkittäviksi tuloksiksi saamalla tietokoneet tekemään valtavia määriä toistuvaa työtä – tunnetuin on todiste 1970-luvulla siitä, että mikä tahansa kartta voidaan värittää vain neljällä eri värillä ja täyttämättä kahta vierekkäistä maata samalla värillä. väri.
Lukuteorian ihmelapsi halutuimman matematiikan palkinnon voittajien joukossa
Mutta järjestelmät, jotka tunnetaan nimellä proof assistant, menevät syvemmälle. Käyttäjä syöttää järjestelmään lauseita opettaakseen sille matemaattisen käsitteen — objektin — määritelmän, joka perustuu yksinkertaisempiin objekteihin, joista kone jo tietää. Väite voi myös viitata vain tunnettuihin objekteihin, ja todistusavustaja vastaa nykyisen tietämyksensä perusteella, onko tosiasia "ilmeisesti" totta vai tarua. Jos vastaus ei ole ilmeinen, käyttäjän on syötettävä lisätietoja. Todistusavustajat pakottavat siten käyttäjän esittämään argumenttinsa logiikan tiukasti ja täyttävät yksinkertaisemmat vaiheet, jotka ihmismatemaatikot olivat tietoisesti tai tiedostamatta jättäneet väliin.
Kun tutkijat ovat tehneet kovan työn kääntääkseen joukon matemaattisia käsitteitä todistusavustajaksi, ohjelma luo tietokonekoodikirjaston, jota muut tutkijat voivat rakentaa ja käyttää korkeamman tason matemaattisten objektien määrittämiseen. Näin todistusavustajat voivat auttaa todentamaan matemaattisia todisteita, jotka muutoin olisivat aikaa vieviä ja vaikeasti, ehkä jopa käytännössä mahdottomia ihmisen tarkastaa.
Proof-assistenteilla on ollut fanejaan pitkään, mutta tämä on ensimmäinen kerta, kun heillä on ollut merkittävä rooli alan kärjessä, sanoo Kevin Buzzard, matemaatikko Imperial College Londonista, joka osallistui yhteistyöhön, joka tarkasti Scholzen ja Clausenin tulos. "Suuri jäljellä oleva kysymys oli: pystyvätkö he käsittelemään monimutkaista matematiikkaa?" sanoo Buzzard. "Näytimme, että he voivat."
Ja kaikki tapahtui paljon nopeammin kuin kukaan oli kuvitellut. Scholze esitti haasteensa todistusapuasiantuntijoille joulukuussa 2020, ja sen otti vastaan joukko vapaaehtoisia, joita johti Johan Commelin, matemaatikko Freiburgin yliopistosta Saksasta. Kesäkuun 5. päivänä – alle kuusi kuukautta myöhemmin – Scholze julkaisi Buzzardin blogiin, että suurin osa kokeesta oli onnistunut. "Minusta on täysin hullua, että interaktiiviset todistusavustajat ovat nyt sellaisella tasolla, että he voivat hyvin kohtuullisessa ajassa varmentaa muodollisesti vaikean alkuperäisen tutkimuksen", Scholze kirjoitti.
Tekoälyn matematiikassa syntyy uusia vaikeita ongelmia ihmisten ratkaistavaksi
Scholzen ja Clausenin mukaan tiivistetyn matematiikan ratkaiseva pointti on määritellä uudelleen topologian käsite, joka on yksi modernin matematiikan kulmakivistä. Monilla matemaatikoiden tutkimilla objekteilla on topologia - eräänlainen rakenne, joka määrittää, mitkä objektin osista ovat lähellä toisiaan ja mitkä eivät. Topologia antaa käsityksen muodosta, mutta sellaisen, joka on muokattavampi kuin tutun koulutason geometrian: topologiassa kaikki muunnos, joka ei repeä objektia, ovat sallittuja. Esimerkiksi mikä tahansa kolmio vastaa topologisesti mitä tahansa muuta kolmiota - tai jopa ympyrää - mutta ei suoraa.
Topologialla on ratkaiseva rooli geometrian lisäksi myös funktionaalisessa analyysissä, funktioiden tutkimuksessa. Funktiot tyypillisesti "elävät" tilassa, jossa on ääretön määrä ulottuvuuksia (kuten aaltofunktiot, jotka ovat kvanttimekaniikan perusta). Se on tärkeä myös p-adic-luvuiksi kutsutuille numerojärjestelmille, joilla on eksoottinen, "fraktaali" topologia.
Upea yhdistyminen
Vuonna 2018 Scholze ja Clausen alkoivat ymmärtää, että perinteinen lähestymistapa topologian käsitteeseen johti yhteensopimattomuuteen näiden kolmen matemaattisen universumin – geometrian, funktionaalisen analyysin ja p-adic-lukujen – välillä. mutta vaihtoehtoiset perustat voisivat kuroa umpeen nämä aukot. Monilla tuloksilla kullakin alalla näyttää olevan analogeja muilla, vaikka ne ilmeisesti käsittelevät täysin erilaisia käsitteitä. Mutta kun topologia on määritelty "oikealla" tavalla, teorioiden väliset analogiat paljastuvat olevan saman "tiivistetyn matematiikan" esimerkkejä, kaksi tutkijaa ehdottivat. "Se on eräänlainen suurenmoinen yhdistäminen" kolmesta kentästä, Clausen sanoo.
Scholze ja Clausen sanovat jo löytäneensä yksinkertaisempia, "tiivistettyjä" todisteita useille syvällisille geometrian tosiasioille ja että he voivat nyt todistaa lauseita, jotka olivat aiemmin tuntemattomia. He eivät ole vielä julkistaneet näitä.
Yksi salaisuus kuitenkin oli: osoittaakseen, että geometria sopii tähän kuvaan, Scholzen ja Clausenin oli todistettava yksi erittäin tekninen lause tavallisten reaalilukujen joukosta, jolla on suoran topologia. "Se on kuin peruslause, jonka avulla todelliset luvut pääsevät tähän uuteen kehykseen", Commelin selittää.
Clausen muistelee, kuinka Scholze työskenteli hellittämättä todisteen parissa, kunnes se valmistui "tahdon voimalla", mikä tuotti prosessissa monia alkuperäisiä ideoita. "Se oli hämmästyttävin matemaattinen saavutus, jonka olen koskaan nähnyt", Clausen muistelee. Mutta väite oli niin monimutkainen, että Scholze itsekin huolestui, että siellä voisi olla jokin hienovarainen aukko, joka mitätöi koko yrityksen. "Se näytti vakuuttavalta, mutta se oli yksinkertaisesti liian uusi", Clausen sanoo.
Scholze pyysi apua tämän työn tarkistamisessa Buzzardilta, lukuteoreetikotoverilta, joka on Leanin, todistusavustajan ohjelmistopaketin, asiantuntija. Leanin loi alun perin tietokonetieteilijä Microsoft Researchissa Redmondissa, Washingtonissa, tarkoituksenaan tarkistaa tietokonekoodi tiukasti virheiden varalta.
Buzzard oli ajanut monivuotista ohjelmaa koodatakseen koko Imperialin matematiikan perustutkinto-opetussuunnitelman Leaniksi. Hän oli myös kokeillut edistyneemmän matematiikan sisällyttämistä järjestelmään, mukaan lukien perfektoidisten tilojen käsite, mikä auttoi ansaitsemaan Scholzelle Fields-mitalin vuonna 2018.
Commelin, joka on myös lukuteoreetikko, otti johdon Scholzen ja Clausenin todisteiden tarkistamisessa. Commelin ja Scholze päättivät kutsua Lean-projektiaan Liquid Tensor Experimentiksi kunnianosoituksena progressiivisen rockin yhtyeelle Liquid Tension Experiment, jota molemmat matemaatikot ovat faneja.
Siitä tuli kuumeinen verkkoyhteistyö. Kymmeniä lean-kokemusta omaavaa matemaatikkoa liittyi mukaan, ja tutkijat saivat apua tietotekniikan tutkijoilta. Kesäkuun alkuun mennessä tiimi oli kääntänyt Scholzen todisteen ytimen – häntä eniten huolestuneen osan – leaniksi. Ja kaikki selvisi – ohjelmisto pystyi tarkistamaan tämän osan todisteesta.
Parempi ymmärrys
Scholzen todistuksen Lean-versio sisältää kymmeniä tuhansia koodirivejä, jotka ovat 100 kertaa pidempiä kuin alkuperäinen versio, Commelin sanoo. "Jos katsot vain Lean-koodia, sinun on erittäin vaikea ymmärtää todistetta, varsinkin sellaisena kuin se on nyt." Mutta tutkijat sanovat, että pyrkimys saada todiste toimimaan tietokoneessa on auttanut heitä ymmärtämään sitä paremmin.
LINKKI AI Copernicus "löytää", että maa kiertää aurinkoa
Riehl on yksi niistä matemaatikoista, jotka ovat kokeilleet todistusapulaisia ja jopa opettaneet niitä joissakin perustutkinto-opintojaan. Hän sanoo, että vaikka hän ei käytä niitä systemaattisesti tutkimuksessaan, ne ovat alkaneet muuttaa hänen tapaansa muodostaa matemaattisia käsitteitä ja esittää ja todistaa niitä koskevia lauseita. "Aiemmin ajattelin todistaa ja rakentaa kahdeksi eri asiasta, ja nyt ajattelen niitä samana."
Monet tutkijat sanovat, että matemaatikoita ei todennäköisesti korvata koneilla lähiaikoina. Todistusavustajat eivät osaa lukea matematiikan oppikirjaa, he tarvitsevat jatkuvaa panosta ihmisiltä, eivätkä he voi päättää, onko matemaattinen lausunto mielenkiintoinen vai syvällinen – vain onko se oikein, Buzzard sanoo. Silti tietokoneet saattavat pian kyetä osoittamaan seuraukset tunnetuista tosiseikoista, joita matemaatikot eivät olleet huomanneet, hän lisää.
Scholze sanoo olevansa yllättynyt siitä, kuinka pitkälle todistusavustajat voivat mennä, mutta hän ei ole varma, ovatko he jatkossakin tärkeässä roolissa hänen tutkimuksessaan. "Tällä hetkellä en todellakaan ymmärrä, kuinka he auttaisivat minua luovassa työssäni matemaatikona."
