Seitsemänsataa käsikirjoitusta
OpenAI julkaisi 6. lokakuuta 2026 yli seitsemänsataa matemaattista käsikirjoitusta, jotka kaikki oli tuottanut yhtiön julkaisematon sisäinen malli OpenAI2026. Ne kattavat seitsemäntoista matematiikan alaa lukuteoriasta ja kombinatoriikasta algebralliseen geometriaan ja tietojenkäsittelyteoriaan. OpenAI:n mukaan yhden tuloksen tuottaminen vei keskimäärin noin kolme tuntia laskenta-aikaa.
Matematiikka on siirtynyt todistusten yltäkylläisyyden aikaan: todistuksia tuotetaan nopeammin kuin matemaatikot ehtivät niitä lukea. Huomattavaan osaan julkaistuista tuloksista liittyy Lean-nimisen tietokoneohjelman tarkistama formaali todistus (de Moura ja Ullrich 2021), joka poistaa tarpeen käydä todistus läpi rivi riviltä. Jotta ymmärtäisi, miksi tällä on merkitystä, on hyvä palata noin viisikymmentä vuotta ajassa taaksepäin.
Luottamus koneeseen
Nelivärilauseen mukaan minkä tahansa kartan alueet voidaan värittää enintään neljällä värillä niin, että millään kahdella vierekkäisellä alueella ei ole samaa väriä. Kenneth Appel ja Wolfgang Haken todistivat lauseen vuonna 1976 palauttamalla ongelman lähes kahteentuhanteen konfiguraatioon ja tarkistamalla ne tietokoneella. Se oli ensimmäinen merkittävä lause, jonka todistusta yksikään ihminen ei pystynyt tarkistamaan käsin. Todistuksen hyväksyminen merkitsi luottamista ohjelmaan, joka oli kirjoitettu varta vasten tätä yhtä tarkoitusta varten.
Jo vuonna 1962 John McCarthy oli esittänyt tälle vaihtoehdon (McCarthy 1962): kirjoitetaan todistus kielellä, joka on niin täsmällistä, että yksi pieni yleiskäyttöinen ohjelma voi tarkistaa jokaisen askeleen. Tämä ajatus on sittemmin toteutettu monessa järjestelmässä, muun muassa näissä: Automath (1967), LCF (1972), Coq (1988) sekä nyt käytetty Lean (2013).
Vuonna 2005 Georges Gonthier sai Benjamin Wernerin avustamana valmiiksi nelivärilauseen formaalin todistuksen Coq-järjestelmässä. Formaalin todistuksen oikeellisuuden tarkistus ei riipu mistään erityisesti neliväriongelmaa varten kirjoitetusta koodista. Luottamus lepää yhden todistustarkistimen varassa, jolla on tuhansia käyttäjiä ja jonka toiminta on varmistettu lukuisissa yhteyksissä.
Todistukset ovat ohjelmia
Miten tietokone ylipäätään voi tarkistaa todistuksen? Avain tähän on Curryn-Howardin vastaavuus, joka on nimetty loogikkojen Haskell Curryn ja William Howardin mukaan (Curry 1934, Howard 1980): lauseen todistamisen ja ohjelman kirjoittamisen voidaan tulkita olevan sama asia.
Ohjelmointikielessä jokaisella arvolla on tyyppi. Luvun $3$ tyyppi on ”kokonaisluku”, ja funktion, joka kuvaa kokonaisluvut totuusarvoiksi, tyyppi on
”kokonaisluku –> totuusarvo”.
Kääntäjä tarkistaa, että tyypit sopivat yhteen: se kieltäytyy soveltamasta tällaista funktiota merkkijonoon. Curryn-Howardin vastaavuuden mukaan jokainen väite luetaan tyyppinä ja väitteen todistus tämän tyypin arvona. Esimerkiksi väitteen
A:sta seuraa B
todistus on funktio, joka muuntaa minkä tahansa A:n todistuksen B:n todistukseksi, ja väitteen
A ja B
todistus on pari, joka koostuu A:n todistuksesta ja B:n todistuksesta. Niinpä todistuksen sille, että väitteestä ”A ja B” seuraa ”B ja A”, antaa funktio
(a,b) –> (b,a).
Todistuksen tarkistaminen vastaa sen varmistamista, että ohjelmalla on se tyyppi, joka sillä väitetään olevan. Kääntäjät ovat tehneet tätä mekaanisesti vuosikymmeniä, ja Leanin ytimessä oleva tyyppitarkistin on tällainen ohjelma.
Varmuuden hinta
Formaali todistaminen oli ennen hyvin kallista. Gonthier kirjoitti nelivärilauseesta, että konfiguraatioiden käsittelyn formalisointi oli työn helppo osa, joka valmistui osa-aikaisesti muutamassa kuukaudessa, kun taas eräiden verkkoteoreettisten päättelyjen selvittäminen ”vei muutaman vuoden”.
Esimerkki Lean-ohjelmasta: todistus sille, että alkulukuja on ääretön määrä.
Luonnollisella kielellä kirjoitettu todistus ohittaa askelia itsestään selvinä, ja näiden askelten kirjoittaminen auki on formalisoinnin työläs osuus. Vuosikymmenien ajan tämä työläys ratkaisi, mitkä lauseet kannatti formalisoida. Tekoälyagentit ovat muuttaneet tämän. Ne ovat väsymättömiä pikkutarkassa työssä, ja todistustarkistin kertoo niille heti, jos jokin menee pieleen. Laajamittainen formalisointi on yhä alkutaipaleellaan, mutta tekoälyjärjestelmät pystyvät jo tuottamaan tuloksia samanaikaisesti niiden Lean-formalisointien kanssa. •
Linkki: OpenAI, Sharing AI progress in mathematics, 6 October 2026. https://openai.com/index/sharing-ai-progress-in-mathematics. Viitattu 17. lokakuuta 2026.
Kirjallisuutta
H. B. Curry. Functionality in combinatory logic. Proc. Nat. Acad. Sci. U.S.A. 20 (1934), 584–590.
G. Gonthier. Formal proof – the four-color theorem. Notices Amer. Math. Soc. 55 (2008), 1382–1393.
W. A. Howard. The formulae-as-types notion of construction. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980, 479–490.
J. McCarthy. Computer programs for checking mathematical proofs. Recursive Function Theory. Proc. Sympos. Pure Math. 5, Amer. Math. Soc., 1962, 219–227.
L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. Automated Deduction – CADE 28. Lecture Notes in Comput. Sci. 12699, Springer, 2021, 625–635.
Lauri Oksanen, Sovelletun matematiikan professori, Helsingin yliopisto