The aim was to remove any remaining uncertainty about the validity of the proof by creating a formal proof that can be verified by automated proof checking software such as HOL Light and Isabelle.
Mục tiêu là loại bỏ bất kỳ sự không chắc chắn về khả năng đúng đắn của chứng minh bằng việc xây dựng một chứng minh chính thức có thể được xác minh bằng kiểm tra chứng minh tự động như các phần mêm HOL Light và Isabelle.