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

Khi học toán, mọi người đều từng gặp 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 logic điển hình.

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

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 có thể 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, rồi lưu trữ chúng vào máy tính. Sau đó, họ lại lập trình cho máy. 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 tìm kiếm, thử nghiệm các công thức, quy tắc và tiền đề, cho đến khi thu đượ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 mạnh hay yếu chủ yếu phụ thuộc vào chất lượng chương trình và số lượng công thức, quy tắc được lưu 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ữ quá nhiều công thức và quy tắc, hiệu quả của chương trình cũng sẽ bị hạn chế.

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

Xem xét hình vẽ 1 đã cho, giả sử 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 bởi bốn điểm X, Y, U, V bất kỳ, trong đó X là đỉnh trái bên trên, Y là đỉnh phải bên trên, U là đỉ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. Hãy chứng minh hai 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 được tạo thành bởi bốn đỉnh A, B, C, D; trong đó A là đỉnh trái bên trên, B là đỉnh phải bên trên, C là đỉnh phải bên dưới, D là đỉnh trái bên 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 đề, tìm công thức và thay các biến X, Y, U, V trong công thức 1 lần lượt bằng A, B, C, D. Ta 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 đề, nên thu đượ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. Từ kết quả trung gian này, chương trình tiếp tục tìm công thức 2, lần lượt thay X, Y, U, V trong công thức 2 bằng A, B, C, D. Khi đó 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. Vì thế, ta thu được kết quả, tức kết luận của công thức 2: ∠ABD và ∠BDC bằng nhau. Đây chính là kết luận cần chứng minh. Bởi vậy định lý đã được chứng minh.

Ở đây, chúng ta chỉ mô 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ế, máy chứng minh định lý hoàn toàn bằng ký hiệu hóa và hình thức hóa.

Từ những năm 50 của thế kỷ XX, chứng minh định lý bằng máy tính từ giai đoạn ý tưởng đi vào giai đoạn thực nghiệm và đã thu được nhiều thành tích đáng mừng. Năm 1956, nhóm Newell đã 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 và quy tắc. Họ đã chứng minh được 38 trong 52 định lý thuộc chương 2 của “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 đơn giản và hiệu quả hơn chương trình của Newell, chỉ trong năm phút đã chứng minh xong 52 định lý. Năm 1965, Robinson nêu ra nguyên lý quy kết, thúc đẩy sự phát triển của chứng minh định lý trên máy tính theo hình thức đơn giản hơn cho cơ giới.

Các nhà khoa học Trung Quốc trong nghiên cứu chứng minh định lý bằng máy tính đã đạt được bước tiến khiến mọi người kinh ngạc, được giới khoa học 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ả. Trong các năm 1976 và 1977, Ngô Văn Tuấn tìm ra 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 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 Euclid.

Do vậy, có thể thấy con người 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 tham gia vào quá trình 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 của nó thật to lớn và sâu xa. Trong lĩnh vực này vẫn còn rất nhiều việc phải làm.