Trong nhiều thế kỷ qua, các nhà toán học đã bị cuốn hút bởi một tính chất hình học kỳ lạ: khả năng cắt một lỗ hổng trong một hình dạng đủ lớn để một bản sao giống hệt hình dạng đó có thể đi qua. Khái niệm phản trực giác này, được gọi là tính chất Rupert, đã được chứng minh tồn tại trong các khối lập phương, bát diện và nhiều khối đa diện lồi khác. Nhưng cho đến tuần này, chưa có ai chứng minh một cách dứt khoát rằng bất kỳ khối đa diện lồi nào thiếu tính chất đáng chú ý này.
Thông tin về Khối lập phương Prince Rupert:
- Câu hỏi ban đầu: thế kỷ 17 bởi Prince Rupert of the Rhine
- Kích thước xuyên qua khối lập phương: ~1.06 lần khối lập phương gốc (lớn hơn 6%)
- Câu trả lời tích cực đầu tiên: John Wallis
- Giải pháp tối ưu được tìm thấy: ~100 năm sau đó bởi Pieter Nieuwland
Noperthedron phá vỡ quy luật
Các nhà nghiên cứu Jakob Steininger và Sergey Yurkevich cuối cùng đã giải quyết được câu đố toán học lâu đời này bằng cách phát hiện ra một khối đa diện lồi hoàn toàn không thể có một lỗ hổng được cắt xuyên qua đủ lớn để chính nó đi qua. Sáng tạo của họ, được đặt tên một cách vui nhộn là noperthedron, có 90 đỉnh, 240 cạnh và 152 mặt. Cái tên này dường như là một sự tri ân đến công trình trước đó của nhà nghiên cứu Tom7, người đã đặt ra thuật ngữ Nopert cho các hình dạng được nghi ngờ thiếu tính chất Rupert.
Khối đa diện lồi: Một hình 3D trong đó tất cả các mặt đều phẳng và hình dạng phình ra ngoài - hãy tưởng tượng thổi phồng một quả bóng bay bên trong một khung dây.
Thông số kỹ thuật của Noperthedron:
- Đỉnh: 90
- Cạnh: 240
- Mặt: 152
- Tính chất: Đa diện lồi đầu tiên được chứng minh không có tính chất Rupert
Chứng minh tính toán đòi hỏi tìm kiếm quy mô lớn
Việc chứng minh rằng khối đa diện này thiếu tính chất Rupert đòi hỏi một phương pháp tính toán toàn diện. Các nhà nghiên cứu phải kiểm tra 18 triệu lỗ hổng tiềm năng khác nhau, tạo ra một chứng chỉ chứng minh 2.5GB mất 30 giờ để xác thực bằng phần mềm toán học. Phương pháp vũ phu này, mặc dù dứt khoát, nhưng đặt ra những thách thức thú vị cho các hệ thống xác minh toán học chính thức.
Cộng đồng toán học đã thảo luận về cách chính thức hóa chứng minh này trong các hệ thống như Lean, yêu cầu mọi bước phải được xác minh một cách nghiêm ngặt. Một nhà nghiên cứu đã lưu ý những khó khăn kỹ thuật đáng kể liên quan đến việc xử lý hàng triệu ô tính toán trong một định lý chính thức duy nhất, mặc dù các phương pháp thay thế liên quan đến xác thực bên ngoài đang được xem xét.
Yêu cầu chứng minh tính toán:
- Các lỗ hổng được kiểm tra: 18 triệu
- Kích thước chứng chỉ chứng minh: 2.5GB
- Thời gian xác thực: 30 giờ (sử dụng SageMath )
- Phương pháp: Tìm kiếm toàn diện bằng máy tính với xác minh toán học
Bối cảnh lịch sử và ý nghĩa tương lai
Tính chất Prince Rupert có tên từ một câu hỏi thế kỷ 17 do Prince Rupert of the Rhine đặt ra, người đã tự hỏi liệu một khối lập phương có thể đi qua một lỗ hổng trong một khối lập phương khác cùng kích thước hay không. Câu trả lời hóa ra là có - đáng chú ý là một khối lập phương có các cạnh lớn hơn khoảng 6% có thể vừa vặn qua một lỗ hổng được định vị phù hợp trong một khối lập phương đơn vị.
Khám phá này mở ra những con đường mới cho nghiên cứu hình học. Trong khi ví dụ hiện tại có 152 mặt, các nhà toán học tò mò liệu các khối đa diện đơn giản hơn có thể cũng thiếu tính chất Rupert hay không. Phát hiện này cũng làm nổi bật cách một số tính chất toán học có vẻ như phổ quát có thể có những ngoại lệ đáng ngạc nhiên, ngay cả khi những ngoại lệ đó đòi hỏi các phương pháp tính toán tinh vi để khám phá.
Đột phá này đại diện cho một ví dụ hoàn hảo của toán học hiện đại, nơi trực giác hình học truyền thống kết hợp với sức mạnh tính toán khổng lồ để giải quyết các vấn đề đã làm bối rối các nhà nghiên cứu trong nhiều thế hệ.
Tham khảo: Rupert's Property