Nowy sposób dowodzenia pozwala wyprowadzać wnioski, które nie muszą być wielokrotnie sprawdzane.

Metoda ma być odpowiedzią na coraz bardziej skomplikowane dowody konstruowane przez ludzi i paradoksy logiczne, które pojawiają się w takich dowodach. Matematycy w swoich „ręcznie” pisanych dowodach opierają się na matematycznej teorii zbiorów, opisującej grupy obiektów – zbiory. Komputery natomiast w konstruowaniu dowodów opierają się na teorii typów.

Vladimir Voevodovsky z Uniwersytetu Princeton napisał poradnik, w którym na 600 stronach dokładnie opisuje, jak należy tworzyć dowody matematyczne, by były one zrozumiałe dla komputera. Wcześniej nie było to możliwe z powodu innych podstaw teoretycznych dowodów „ludzkich” i „komputerowych”.

Dzięki nowej metodzie dowody tworzone przez ludzi mogłyby być na bieżąco weryfikowane przez komputer i wszelkie błędy czy paradoksy można byłoby usunąć na wczesnym etapie. Jak udowodniono na przykładzie zamieszczonym w poradniku, jeżeli oprogramowanie do pisania dowodów jest poprawnie skonstruowane, niemożliwe staje się napisanie błędnego dowodu matematycznego.

Potrzeba opracowania takiej metody wyniknęła z narastających problemów ze sprawdzaniem dowodów matematycznych, które stawały się bardzo skomplikowane i niezrozumiałe dla każdego poza twórcą. Na przykład opublikowany w zeszłym roku w Japonii dowód matematyczny dotyczący tzw. Hipotezy ABC, obejmuje 500 stron równań. Po dziewięciu miesiącach analiz nadal nie wiadomo, czy dowód jest poprawny. (PAP)

stm/ ula/