Vì sao dùng máy tính điện tử lại có thể chứng minh được định lí toán học?

Vào năm 1976 từ trường đại học Ilinoi ở nước Mỹ đã truyền đi một nguồn tin làm kinh động mọi người. Hai nhà toán học Abel và Hakan đã chứng minh được một bài toán mà đã hơn 100 năm qua chưa có lời giải: “Dự đoán bốn màu”. Điều hết sức thú vị là họ đã dựa vào máy tính để chứng minh dự đoán này.

Chúng ta biết máy tính có điểm mạnh là có thể lặp đi, lặp lại các thao tác đơn giản, nếu đem biến các chứng minh toán học phức tạp thành các thao tác máy móc rồi giao cho máy tính thì sẽ giải phóng cho các nhà toán học khỏi nhiều công việc rắc rối.

Nhà toán học Giáo sư Ngô Tuấn của Trung Quốc cùng các cộng sự đã nghiên cứu cách cơ giới hoá các chứng minh định lí toán học. Trên cơ sở của hình học giải tích ông đã đại số hoá các định lí, tiến hành cơ giới hoá để máy tính có thể tiếp nhận giải quyết, chứng minh các định lí trong hình học phẳng.

Đến năm 1978, Ngô Tuấn cùng các đồng nghiệp đã hoàn thành việc chứng minh các định lí hình học sơ cấp cũng như nhiều bài toán hình học vi phân bằng chứng minh cơ giới hoá bằng máy tính điện tử. Từ đó đã mở ra con đường dùng máy tính điện tử để chứng minh nhiều định lí toán học phức tạp.

Như vậy nhờ một công việc chưa có tiền lệ, nghiên cứu thành công mà đã có thể dùng máy tính để thay thế cho lao động trí não cực nhọc giải quyết một bộ phận công tác trong toán học, mở ra con đường mới cho toán học phát triển.