| Metamath | |
|---|---|
| Tyyppi | verkkosivusto |
| Kehittäjä | Norman Megill |
| Sisään kirjoitettu | ANSI C |
| Käyttöjärjestelmä | Linux , Windows , macOS |
| uusin versio |
|
| Lisenssi | GNU yleinen julkinen lisenssi ( Creative Commons Public Domain Dedication tietokantoihin) |
| Verkkosivusto | metamath.org github.com/metamath/metamath-exe |
Metamath ( venäjäksi Metamat ; tulee sanasta " metamuuttuja matematiikka " [2] , venäjäksi "matematiikka metamuuttujilla ") on hyvin yksinkertainen muodollinen kieli ja sitä vastaava kompakti tietokoneohjelma ( interaktiivinen lauseiden todistamistyökalu ) formalisointiin, joka kerätään arkistoon vastaava sivusto , matemaattisten todisteiden vahvistus ja tutkimus [3] . On olemassa useita tietokantoja todistetuista lauseista, jotka on kehitetty käyttämällä Metamathia, ja ne vaihtelevat klassisista tuloksista logiikassa , joukkoteoriassa , lukuteoriassa , algebrassa , topologiassa , analyysissä ja muilla matematiikan aloilla. [4] Tämä projekti on ensimmäinen laatuaan, jonka avulla voit kätevästi ja interaktiivisesti tutkia formalisoitujen lauseiden tietokantaa tavallisen sivuston muodossa. [5]
Kesäkuussa 2022 kaikkien Metamathilla todistettujen lauseiden kokoelmalla on yli 23 000 todistetta [6] , ja se on yksi formalisoidun matematiikan maailman suurimmista. Erityisesti tämä kokoelma sisältää todisteita 74: stä [7] Formalizing 100 Theorems -haasteen 100 lauseesta , mikä sijoittuu kolmanneksi HOL Lightin ja Isabellen jälkeen, mutta ennen Coqia , Mizaria, ProofPoweria , Leania , Nqthmia, ACL2 :ta ja Nuprlia . Metamath-muotoa käyttäviä interaktiivisia lauseiden todistamistyökaluja on ainakin 17. [kahdeksan]