Máy tính có thể chứng minh định lí được không?

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.

Bao lâu nay con người vẫn đang luôn tìm kiếm phương pháp chứng minh định lí tự động, hi vọng có một ngày đưa vào máy tính một định lí toán cần chứng minh, vận hành hệ thống chứng minh định lí của máy, và rồi rất nhanh đã nhận được lời chứng minh định lí.

Chứng minh định lí tự động cũng gọi là "chứng minh bằng máy tính".

Máy tính sở dĩ có chứng minh định lí là vì các chuyên gia trước hết đã kí hiệu hóa một số công thức và quy tắc, lưu trữ vào máy tính. Rồi lại lập trình cho nó. Những chương trình này có thể mô phỏng phương thức suy lí của con người. Khi bạn đã đưa vào máy tính các tiền đề và kết luận của định lí bằng hình thức kí hiệu quy định, chương trình sẽ không ngừng tiến hành công việc tìm kiếm và kết luận với việc thử nghiệm các công thức, quy tắc và tiền đề, cho đến khi được kết quả phù hợp với kết luận. Khả năng chứng minh định lí của máy là mạnh hay yếu, chủ yếu quyết định bởi chất lượng hay dở của chương trình và số lượng công thức, quy tắc được lưu trữ trong máy. Chương trình thiết kế càng tốt, công thức và quy tắc lưu trữ càng nhiều thì khả năng chứng minh định lí của máy càng mạnh. Đương nhiên khi đã lưu trữ nhiều công thức và quy tắc thì hiệu quả của chương trình sẽ bị hạn chế.

Sau đây sẽ quan sát một ví dụ đơn giản.

Xem xét hình vẽ 1 đã cho, giả thiết máy tính đã lưu trữ công thức về hình 1:

Công thức 1: Với hình thang được tạo thành bởi bốn điểm X; Y; U; V bất kì, trong đó X là điểm đỉnh trái bên trên, Y là điểm đỉnh phải bên trên, U là điểm đỉnh phải bên dưới, VY là đường chéo nối hai đỉnh đối nhau. Nếu XYUV là một hình thang thì đoạn thẳng XY song song với đoạn UV.

Công thức 2: Nếu XY song song với đoạn UV thì ∠ XYV và ∠ UVY bằng nhau.

Cho một hình thang ABCD như hình 2. Đoạn thẳng DB là đường nối hai đỉnh đối nhau. Chứng minh 2 góc so le trong ∠ ABD và ∠ BDC bằng nhau. Tức là phải chứng minh: nếu ABCD là hình thang thì ∠ ABD và ∠ BDC bằng nhau.

Tiền đề đưa vào máy tính là: một hình thang tạo thành bởi bốn đỉnh điểm ABCD. Trong đó A là điểm đỉnh trái bên trên, B là điểm đỉnh phải bên trên, C là điểm đỉnh phải ở dưới, D là điểm đỉnh trái ở dưới, BD là đường nối hai đỉnh đối nhau. ABCD là hình thang. Kết luận: ∠ ABD và ∠ BDC bằng nhau.

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.

Do vậy có thể thấy rằng người ta có thể làm cho máy tính có khả năng chứng minh. Mục đích của việc nghiên cứu chứng minh định lí bằng máy tính là để máy tính trực tiếp can dự vào quá trình hoạt động tư duy của con người, nâng cao khả năng và hiệu quả sáng tạo khoa học của loài người. ý nghĩa thật là to lớn và sâu xa. Về mặt này còn có nhiều việc phải làm nữa.