Sprawdzanie poprawności dowodów matematycznych często wymaga sporej wiedzy i ogromu nużącej pracy. O ile dochodzenie do zrozumienia istoty dowodu, czyli dlaczego dane twierdzenie matematyczne zachodzi, może sprawiać Czytelnikowi dużo satysfakcji, o tyle weryfikowanie wszystkich szczegółów dowodu jest zajęciem dość niewdzięcznym. Z tego powodu od wielu już lat trwają badania nad zaprzęgnięciem komputerów do tej żmudnej części pracy...

Aktualnie nie istnieją programy, które potrafią rozumieć dowody matematyczne napisane po polsku lub po angielsku (i ogólnie, w żadnym języku naturalnym). Istnieją za to systemy z własnym językiem opisu dowodu, mniej lub bardziej oddalonym od języka naturalnego. Jednym z takich systemów jest Coq, rozwijany głównie we Francji, w instytucie naukowym INRIA. Jest to interaktywny system pozwalający na poszukiwanie dowodów twierdzeń za pomocą zwięzłych komend, nazywanych taktykami.

Każda taktyka odpowiada z grubsza zastosowaniu pewnej reguły dowodzenia zwanej naturalną dedukcją. Coq nie służy do automatycznego dowodzenia twierdzeń, do działania potrzebuje ludzkich podpowiedzi. Każdą podpowiedzianą taktykę stosuje bezbłędnie, uzyskując wszystkie możliwe wnioski i sprawdzając, co jeszcze należy udowodnić, żeby dowód analizowanego twierdzenia był kompletny. W niniejszym artykule zaprezentujemy dowód w Coqu, wykonany z użyciem reguł naturalnej dedukcji, następującego twierdzenia:

Choć twierdzenie brzmi absurdalnie, jednak da się je udowodnić. Przyczyny tego dysonansu omówimy później, a teraz rozważmy dwa dowody.