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?
Năm 1976, từ Đại học Illinois ở Mỹ truyền đi một tin làm chấn động giới khoa học. Hai nhà toán học Abel và Hakan đã chứng minh được một bài toán hơn 100 năm chưa có lời giải: “dự đoán bốn màu”. Điều đặc biệt 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 những thao tác đơn giản với tốc độ nhanh. Nếu biến các chứng minh toán học phức tạp thành những thao tác máy móc rồi giao cho máy tính, các nhà toán học có thể được giải phóng khỏi nhiều công việc rắc rối.
Giáo sư Ngô Tuấn, nhà toán học Trung Quốc, cùng các cộng sự đã nghiên cứu cách cơ giới hóa chứng minh định lý toán học. Trên cơ sở hình học giải tích, ông đại số hóa các định lý, đưa chúng về dạng mà máy tính có thể tiếp nhận và xử lý, từ đó chứng minh các định lý trong hình học phẳng.
Đến năm 1978, Ngô Tuấn và các đồng nghiệp đã hoàn thành việc chứng minh nhiều định lý hình học sơ cấp cũng như một số bài toán hình học vi phân bằng phương pháp chứng minh cơ giới hóa trên máy tính điện tử. Thành quả này 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ờ một công việc nghiên cứu chưa từng có tiền lệ, máy tính có thể thay thế một phần lao động trí óc nặng nhọc trong toán học, đồng thời mở ra hướng phát triển mới cho ngành toán.
