Weryfikacja komputerowa W 2005 roku Avigad et al. użyli Isabelle do stworzenia weryfikowalnego komputerowo dowodu twierdzenia o liczbach pierwszych autorstwa Erdősa i Selberga. Była to pierwsza próba komputerowego dowiedzenia twierdzenia o liczbach pierwszych. Avigad wybrał do sformalizowania dowód autorstwa Erdősa i Selberga, a nie analityczny dowód, gdyż co prawda biblioteka Isabelle wtedy potrafiła implementować granice funkcji, pochodne i funkcje przestępne, jednak nie zawierała rachunku całkowego.
W 2009 roku John Harrison wykorzystał HOL Light do sformalizowania dowodu wykorzystującego analizę zespoloną.
Przypisy
Linki zewnętrzne
O Kategoria:Analityczna teoria liczb