Hơn 50 năm trước, từ khi chiếc máy tính đầu tiên ra đời, máy tính đã trở thành một kỹ thuật tiên tiến không thể thay thế trong cuộc sống, công việc của con người. Tên gọi của máy tính cho chúng ta biết, máy tính ngày trước chính là một công cụ tính toán, nó ra đời để đáp ứng nhu cầu tính toán phức tạp, phiền phức của nhân loại.
Ví dụ, “định lí bốn màu” nổi tiếng nói rằng, bất kỳ một bản đồ nào chỉ cần dùng bốn màu khác nhau là có thể phân biệt được các nước láng giềng. Trong vòng 124 năm, vô số nhà toán học đã đổ biết bao tâm sức mà vẫn chưa đưa ra được chứng minh hoàn chỉnh, bởi vì khi tăng lên 1, 2 nước; quan hệ biên giới giữa các nước khác nhau trở nên vô cùng phức tạp mang đến sự khó khăn rất lớn cho con người trong việc tính toán thủ công. Cho đến năm 1976, chính máy tính đã giúp các nhà toán học giải quyết được vấn đề chứng minh định lí này, gây ra chấn động trong giới toán học, hơn nữa lúc bấy giờ sử dụng ba chiếc máy tính cỡ siêu lớn đã làm hao phí hơn 1200 tiếng đồng hồ; nếu nhà toán học lúc đó dùng sức thủ công để hoàn thành, thì sẽ không thể làm được.
Dùng máy tính chứng minh định lí toán học có tính ưu việt độc đáo của nó: một là không sợ phiền phức, sở trường của máy tính là tiến hành những tính toán phức tạp khối lượng lớn, giúp nhà toán học giải thoát khỏi những tính toán phiền phức, hai là tính toán chuẩn xác, cơ bản không có sai sót gì. Vì máy tính làm việc vừa nhanh vừa tốt, cho nên rất nhiều người đã bắt đầu nghiên cứu làm thế nào để dùng máy tính thay con người chứng minh định lí, gọi là “máy tính chứng minh”, nó đã trở thành một phân nhánh mới của khoa học máy tính.
Nhiều nhà toán học đã nhiều năm dồn sức nghiên cứu máy móc hoá chứng minh định lí. Trên cơ sở hình học giải tích, họ sẽ đại số hoá định lí trong hình học phẳng, từ đó để cho máy tính thực hiện nhiệm vụ của mình.
Trên thế giới, các nhà toán học đã dùng máy tính tìm ra giá trị số Pi chính xác nhất mà mọi người biết đến cho tới ngày nay, số pi được tính chính xác đến 1073740000 đơn vị sau dấu phẩy. Không có sự giúp đỡ của máy tính, những thành tích này thật không thể đạt được.
Tin rằng cùng với sự tăng lên về dung lượng bộ nhớ và tốc độ xử lý máy tính sẽ mang lại những đột phá mới cho việc chứng minh định lí.
