Sähköisissä matematiikan oppikirjoissa olisi hyötyä interaktiivisista todistuksista, joiden avulla lukija voisi pyytää tarkentavaa selitystä mihin tahansa kohtaan, jota hän ei ymmärrä. Tällaisen kirjan kirjoittaminen vaatii, että määritelmät, lauseet ja todistukset on kirjoitettu jollain formaalilla kielellä. Tässä diplomityössä tutkitaan sekä käytännön että teorian tasolla interaktiivisia todistuksia sisältävien oppikirjojen kirjoittamiseen liittyviä haasteita.

Koska mikään yksittäinen kieli ei voi olla riittävä kaikkien oppikirjojen tarpeisiin, työssä määritellään kielen laajentamisen käsite. Tämän viitekehyksen sisällä kehitetään määritelmille ja lauseille kolme kieltä, joista kaksi ensimmäistä vastaavat lauselogiikkaa ja ensimmäisen kertaluvun predikaattilogiikkaa. Kolmas kieli, joka on näiden laajennus, on ilmaisuvoimaltaan riittävä monien diskreettiin matematiikkaan keskittyvien oppikirjojen formalisoimiseen. Tämä kieli on käsitteellisesti yksinkertaisempi kuin joukko-opin tai korkeamman kertaluvun predikaattilogiikan kielet, koska siinä ei pysty rajoittamattomasti kvantifioimaan sellaisten joukkojen yli, jotka ovat suurempia kuin reaalilukujen joukko.

Lisäksi työssä esitellään tietokoneohjelma, jonka avulla interaktiivisesti tarkasteltavia formaaleja todistuksia voi lukea, sekä tämän ohjelman avulla kirjoitettu Bertrandin postulaatin todistus. Tässä työssä keskitytään todistuksiin lukijan näkökulmasta, ja tulokset ovat siltä osin lupaavia. Kokonaisen oppikirjan formalisoimiseksi vaaditaan vielä lisätyötä oppikirjan kirjoittajan työn helpottamiseksi.