Proof assistant (interaktywny dowodzący twierdzeń) to narzędzie programistyczne wspomagające proces tworzenia sformalizowanych dowodów matematycznych poprzez współpracę człowieka z maszyną. Oprogramowanie to udostępnia specjalistyczny język do zapisu definicji i twierdzeń oraz wykorzystuje rygorystyczne jądro logiczne do automatycznej weryfikacji poprawności każdego kroku wnioskowania. Pozwala to na wyeliminowanie błędów ludzkich i zapewnienie najwyższego stopnia pewności co do poprawności przeprowadzonych dowodów lub weryfikacji kodu źródłowego.
proof assistant
