Có thể dùng máy tính điện tử để chứng minh định lý hình học không?

Có thể dùng máy tính điện tử để chứng minh định lý hình học không?

Để chứng minh các định lý hình học người ta phải tốn công suy nghĩ, không có một khuôn khổ nhất định nào để làm theo. Nó cũng như công việc của một nhà điêu khắc là phải dựa vào sự khéo léo của bàn tay, dựa vào kỷ sảo và linh cảm nghề nghiệp. So với việc giải quyết một phương trình đại số thì việc chứng minh hình học khá xa.

Việc tính toán quả là việc cực nhọc khô khan, nhưng lại có khuôn mẫu để làm theo, dễ nắm được cách thực hiện, còn việc chứng minh thì đòi hỏi phải linh hoạt khéo léo, phải tùy cơ ứng biến.

Vậy có thể tìm cách biến các vấn đề cần chứng minh thành các khuôn thước để tính toán được không? (Đó chính là vấn đề chứng minh một cách máy móc).

Loài người đã sớm có nguyện vọng này. Từ thế kỷ XVII, nhà toán học Pháp Descartes đã phát minh ra phương pháp tọa độ, lập nên môn hình học giải tích, đây là bước đột phá đầu tiên vào nguyện vọng này. Dùng phương pháp tọa độ ta có thể biến một bài toán hình học thành một bài toán đại số, thế nhưng còn có vấn đề biến bài toán chứng minh hình học thành phép tính. Lúc bấy giờ vì còn chưa có công cụ tính toán tiên tiến, nên việc biến bài toán chứng minh thành một phép tính toán là khá phiền phức. Đến những năm 50 của thế kỷ này (thế kỷ XX), thì máy tính điện tử ra đời, nhiều nhà toán học trên thế giới hết sức hứng thú với ý tưởng “cơ giới hóa phương pháp chứng minh”. Trải qua 20 năm nghiên cứu, nhưng vẫn chưa tìm được phương pháp hữu hiệu để cơ giới hóa phương pháp chứng minh.

Nhà toán học nổi tiến Trung Quốc, giáo sư Ngô Văn Tuấn đã khám phá được những nét ưu tú của nền toán học cổ Trung Quốc, dày công nghiên cứu, sáng tạo cái mới, đến năm 1977 đã công bố phương pháp mới để chứng minh máy móc các định lý hình học, phương pháp này ngày nay đã nổi tiếng khắp thế giới và được man tên là phương pháp họ Ngô. Dùng phương pháp họ Ngô (Ngô pháp) có thể dùng máy tính điện tử cở nhỏ để chứng minh các định lý hình học khá phức tạp như định lý Simson, định lý Felbage, định lý Muler một cách nhanh chóng cũng như phát minh các định lý mới cao xa khác. Ngô pháp như là một cục nam châm hấp dẫn nhiều chuyên gia chuyên nghiên cứu vấn đề cơ giới hóa phương pháp chứng minh trên thế giới. Có nhiều chuyên gia về mặt này trên thế giới học tập Ngô pháp, nghiên cứu Ngô pháp. Nhà mỹ học Trung Quốc là tiến sĩ Chu Hoặc Thanh đã công bố một tập chuyên khảo bằng tiếng Anh, nêu lên việc ông đã dùng Ngô pháp để chứng minh 500 định lý hình học. Theo khám phá của Ngô pháp, ông đã dùng phương pháp chứng minh máy móc định lý hình học để áp dụng thành công công cụ đại số Grubas (viết tắt là GB). Tóm lại với sự xuất hiện của Ngô pháp đã mở ra một phương trời mới cho việc nghiên cứu các phương pháp cơ giới hóa để chứng minh các định lý hình học, làm Trung Quốc trở thành nước đi đầu trong lĩnh vực này.

Thế thì bạn sẽ hỏi làm thế nào để chứng minh các định lý hình học bằng máy tính? Muốn biết tường tận xin mời các bạn đọc quyển sách của giáo sư Ngô Văn Tuấn: “Nguyên lý cơ bản của phương pháp chứng minh định lý hình học một cách máy móc” (NXB khoa học Trung Quốc 1984, 280 tr). Tuy nhiên, có thể tóm tắt cơ bản tư tưởng của phương pháp như trình bày ở dưới để các bạn biết một cách vắn tắt làm thế nào để chứng minh định lý hình học một cách máy móc.

Ví dụ cần chứng minh định lý: “Các góc đối trong một hình bình hành bằng nhau”.

Theo hình, ta đã biết rằng điều kiện để AB//CD, AD//BC, E là giao điểm của CD và BD. Cần phải chứng minh AE=EC cũng như BE=DE. Đương nhiên để làm được điều đó ta cần chứng minh AE=CE. Bởi vì cũng tương tự ta sẽ có BE=DE.

image001

Bước thứ nhất để chứng minh định lý là ta hải đại số hóa bài toán hình học. Con đường để đại số hóa là dùng phương pháp tọa độ, cũng như các phương pháp dùng các định lý tam giác. Để các bạn nào chưa học qua phương pháp tọa độ cũng nắm được phương pháp, chúng tôi dùng phương pháp diện tích để đại số hóa.

Ta dùng kí hiệu:image0021 .

Đầu bài  ta thiết lập các điều kiện liên hệ giữa các đại lượng: image003 với u. Các đại lượng này có mối liên quan đại số sau đây:

(1) x1=u (tức SABD=SABC do AB//CD)

(2) x2=u (tức SBCD=SABC do BC//AD)

(3) x3+x4=u (tức SABE+SBCE=SABC chứng tỏ E nằm trên AC)

(4) x1.x4=x2.x3 (tức image004, chứng tỏ E nằm trên BD)

Điều ta cần chứng minh là AE=EC, tức là SBCD=SABE, tức cũng chính là cần phải có x3=x4, x3=x1-x3

Như vậy từ yêu cầu chứng minh định lý hình học đi đến vấn đề từ các  đẳng thức đại số (1), (2), (3), (4) ta phải chứng minh được đẳng thức x3=x4.

Bước thứ hai của chứng minh máy móc là biến các giả thiết của bài toán thành các tiêu chuẩn hình thức hoặc còn gọi là “chỉnh  lý trật tự”. Trong các đẳng thức (2), (3), (4) có 5 biến là x1, x2, x3, x4, và u. Sở dĩ nói là “chỉnh lý trật tự” là vì ta phải từ các đẳng thức làm xuất hiện một tổ hợp đẳng thức. Trong (1) có các biến x1 và u, trong (2) có thể xem biến x2 theo đúng yêu cầu; trong (3) xuất hiện thêm x3 và x4 không hợp yêu cầu. Như vậy từ đẳng thức này ta cần phải bỏ bớt một biến đã tăng lên. Từ (4) ta rút ra: image005

Sau khi thay vào (3) x4 bị khử mất. Qua biến đổi (khử mẫu số) ta có: x1.x3+x2x3=ux1. Dùng hệ thức này thay vào cho (3) ta có tổ hợp các đẳng thức hình thức:

(a) x1=u

(b) x2=u

(c) x1.x3+x2.x3=x1.u

(d) x1.x4=x2.x3

Trong tổ hợp các đẳng thức này ta thấy: Trong (a) không có x2, x3, x4; trong (b) không xuất hiện x3, x4, trong (a), (b), (c) không xuất hiện x4, trong (d) xuất hiện x4. các biến đổi làm tăng thêm tổ hợp đẳng thức ta gọi đó “dãy số tăng” hoặc “dãy số họ Ngô”.

Bước thứ 3 trong việc chứng minh máy móc được gọi là “ước lược”. Trước hết từ (d) ta tìm x4, sau đó thay giá trị vừa tìm được để chứng minh x3=x4 (nếu trong (d) không phải chứ x4 ở bậc một nên không giải  để tìm x1). Thế nhưng có thể giảm hạng x4 trong hệ thức. Ví dụ: (d) có dạng image006. Ta cần chứng minh image007, thì sau khi ước lược ta có u-x1.x3=x2.x3

Từ (c) giải ra x3 rồi thay vào hệ thức vừa có ta được image008

Từ (b) giải ra x2 : x2=u thay vào ta có: image009

Cuối cùng, từ (a) ta có x1=u thay vào ta có: u3=u3

Đó là một đẳng thức. Từ cách chứng minh này ta thấy x3=x4 tức là đã chứng minh được định lý.

Nếu bây giờ bạn lại dùng (1), (2) thay vào (4) ta sẽ được u.x4=u.x3 nên được ngay x3=x4 chẳng tiện hơn sao? Tại sao phải dùng biện pháp “chỉnh lý thứ tự”, “ước lược”, quá rắc rối. Đó là do máy tính hoạt động theo thứ tự xác định không linh hoạt được như người. Chỉ cần viết quy luật tính toán (thuật toán) chính xác thì máy tính mới giải đáp, chứng minh được định lý được đặt ra.

Phương pháp chưng minh định lý họ Ngô đã cơ bản kết thúc công việc thủ công sơ đẳng có lịch sử mấy ngàn năm. Ngay khi đưa ra các định lý hình học sơ cấp, chỉ cần đưa vào máy tính là được chứng minh. Công việc chủ yếu của người là dự đoán, phát hiện để tìm ra các định lý thú vị nhất để nghiên cứu, cũng như tìm cách chứng minh đơn giản nhất.

Trích: “Chìa khóa vàng Toán Học” NXBĐH QG Hà Nội 1997.

Advertisements

Trả lời

Mời bạn điền thông tin vào ô dưới đây hoặc kích vào một biểu tượng để đăng nhập:

WordPress.com Logo

Bạn đang bình luận bằng tài khoản WordPress.com Đăng xuất / Thay đổi )

Twitter picture

Bạn đang bình luận bằng tài khoản Twitter Đăng xuất / Thay đổi )

Facebook photo

Bạn đang bình luận bằng tài khoản Facebook Đăng xuất / Thay đổi )

Google+ photo

Bạn đang bình luận bằng tài khoản Google+ Đăng xuất / Thay đổi )

Connecting to %s

%d bloggers like this: