Khi học môn toán, mọi người đều đã đụng tới vấn đề “chứng minh định lí”. Chứng minh định lí có thể nói là một quá trình suy luận lôgic điển hình.

Chương trình căn cứ vào tiền đề và tìm công thức đổi biến lượng X; Y; U; V trong công thức 1 lần lượt là A; B; C; D. Có được một ví dụ thực tế: nếu ABCD là hình thang thì AB song song với CD. Lại vì “ABCD là một hình thang” là tiền đề, thế là có được kết quả trung gian, tức kết luận của ví dụ thực tế thuộc công thức 1: AB song song với CD. Lại từ kết quả trung gian này mà tìm ra công thức 2, lần lượt thay thế lượng X, Y, U, V trong công thức 2 thành A, B, C, D. Sẽ có một ví dụ thực tế của công thức 2: nếu AB song song với CD thì ∠ ABD và ∠ BDC bằng nhau. Lúc này kết quả trung gian “đoạn AB song song với đoạn CD”, nhất trí với tiền đề của ví dụ thực tế trong công thức 2. Thế là có được kết quả, tức kết luận của ví dụ thực tế trong công thức 2: ∠ ABD và ∠ BDC bằng nhau. Đây chính là kết luận cần có. Bởi vậy định lí đã được chứng minh.

Ở đây chúng ta chỉ là miêu tả quá trình chứng minh định lí của máy tính một cách phi hình thức. Trên thực tế thì máy chứng minh định lí hoàn toàn là kí hiệu hóa và hình thức hóa.

Từ những năm 50 của thế kỉ XX, máy tính chứng minh định lí từ giai đoạn thiết tưởng đi tới giai đoạn thực nghiệm, và đã thu được nhiều thành tích đáng mừng. Năm 1956 nhóm Niuơ đã biên soạn chương trình máy tính thể hiện quá trình tư duy suy lí diễn dịch của bộ não con người với các bước giản hóa, kĩ xảo, sách lược, quy tắc. Họ đã chứng minh định lí 38 trong 52 định lí thuộc chương 2 Nguyên lí toán học của Bertrand Russell – Alfred North Whitehead. Năm 1963, chương trình được cải tiến đã chứng minh toàn bộ 52 định lí. Năm 1958 một người Mĩ gốc Hoa là Vương

Hạo đã soạn ba chương trình so với chương trình của Niuơ còn giản đơn và hiệu quả hơn, chỉ năm phút đã chứng minh xong 52 định lí. Năm 1965 Rôbinxơn đã nêu ra nguyên lí quy kết, thúc đẩy sự phát triển của việc chứng minh định lí trên máy tính với hình thức đơn giản cho cơ giới.

Các nhà khoa học Trung Quốc trong công cuộc nghiên cứu chứng minh định lí trên máy tính đã có được bước tiến khiến mọi người phải ngạc nhiên, được giới khoa học trên thế giới coi trọng và đánh giá cao. Trong đó, thành quả nghiên cứu của giáo sư Ngô Văn Tuấn là nổi bật hơn cả. Giữa năm 1976 và 1977 Ngô Văn Tuấn đã tìm ra được phương pháp chứng minh bằng máy tính cho các định lí hình học, và đã chứng minh được hơn 100 định lí bằng máy tính. Về sau ông còn mở rộng phạm vi chứng minh bằng máy tính sang các lĩnh vực khác như hình học xạ ảnh, hình học phi Ơclit.