Geometrista päättelyä Eukleideen tapaan laskentaohjelmalla

Kaupallisista tietokoneohjelmista ilmestyy ajoittain uusi versio, jossa vähäisten paikkailujen lisäksi täytyy olla jotakin oleellisesti uutta. Tämä tarvitaan uuden version markkinointiin, mutta uutuuksien merkitys ja kohtalo ilmenee vasta myöhemmin. Ne saattavat olla uusia aluevaltauksia, joita kukaan ei ehkä osannut edes kaivata, mutta ne muuttavat työskentelytapojamme ja näkökulmiamme joko hyvään tai huonoon suuntaan. Toisaalta ne saattavat osoittautua tarpeettomiksi ja jäädä olemattomalle käytölle.

Laskentaohjelma Mathematica on jokaisessa kokonaislukuversiossaan pyrkinyt tuomaan jotakin uutta.  Usein kyse on ollut merkittävistä uusista mahdollisuuksista, mutta joukossa on myös unohduksiin painuneita ideoita. Versio 12 tuo Eukleideen geometrian, ei laskennallisena analyyttisena geometriana, vaan eräänlaisena päättelynä.

Olkoon esimerkkinä kolmioiden yhtenevyysteoreema KSK. Aluksi määritellään lähtötilanne oletuksineen: kaksi kolmiota, $ABC$ ja $PQR$, sekä näiden yhtä suuret vastinosat, yksi sivupari ja kaksi kulmaparia.

Konfiguraatiosta voidaan piirtää haluttu määrä kuvioita, joissa kärkipisteiden koordinaatit valitaan satunnaisesti, mutta oletusehdot toteutuvat.

Mielenkiintoisin on kolmas vaihe, jossa pyritään etsimään kuvion uusia ominaisuuksia, ts. mitä voitaisiin yrittää todistaa lähtötilanteen pohjalta. Alla olevan tuloksen kaksi ensimmäistä riviä väittävät, että kolmiot ovat yhteneviä ja että ne ovat yhdenmuotoisia. Loput rivit tarkoittavat vastinosien yhtäsuuruutta.

En tiedä, millaista algoritmia tässä käytetään, ts. miten uudet ominaisuudet itse asiassa etsitään.

Vastaavalla tavalla käy, jos määritellään lähtötilanteeksi kolmio keskijanoineen, jolloin uudeksi ominaisuudeksi löydetään keskijanojen kulkeminen saman pisteen kautta (ovat concurrent).

Kyseessä ilmeisesti on uusi kokeellinen innovaatio tekoälysovellusten kehittelyssä. Taustatiedot ovat tässä suhteessa aika niukkoja. Tilanne tietenkin houkuttelee kokeilemaan erilaisia konfiguraatioita, eikä uusia ominaisuuksia aina löydykään. Jos keskijanat korvataan kulmanpuolittajilla tai keskinormaaleilla, mitään uusia ominaisuuksia ei löydy. Sovelluksen kehittely näyttää olevan vielä kesken, minkä avoin kertominen olisi paikallaan.

Kaikenlaista voidaan kehitellä, ja tuloksena saattaa olla ideoita, joista saatava hyöty on jossakin kokonaan muualla. Jään kuitenkin ihmettelemään, mikä hyöty laskentaohjelman käyttäjälle olisi kuvatunkaltaisesta euklidisesta geometriasta. Jos sovellus alkaa toimia edes lähes moitteetta, kyseessä on eräänlainen geometrinen laskin: syötteeksi annetaan jokin konfiguraatio, ja tulokseksi saadaan luettelo siitä, mikä tässä konfiguraatiossa on totta. Eräänlainen teoreemalaskuri siis. Mutta tarvitsemmeko me tällaista?

Euklidisen geometrian todistamista ei varsinaisesti opeteta sen takia, että tiedettäisiin, mikä on totta, vaan sen takia, että opitaan päättelyn metodi. Tämän näkökulman sovellus ainakin nykymuodossaan ohittaa. Toisaalta voidaan tietysti ajatella, että riittävän pitkälle kehittyessään sovellus alkaa löytää ennen tuntemattomia tuloksia ja ehkä jopa kykenee raportoimaan menettelyn näiden todistamiseen. Tähän on kuitenkin melkoinen matka.

Minkälaiseen käyttöön ja minkälaiseen tehtävään sovellus sitten olisi tarkoitettu?