-
Dự án Xena và Định lý cuối cùng của Fermat
- Dự án Xena nhằm mục tiêu hình thức hóa toán học trên máy tính. Mục đích là để nếu một cuộc cách mạng AI trong toán học xảy ra, máy tính có thể giúp mở rộng biên giới của lý thuyết số hiện đại.
-
Hình thức hóa Định lý cuối cùng của Fermat
- Công việc chứng minh Định lý cuối cùng của Fermat (FLT) trên máy tính đang được tiến hành. Trong quá trình này, nhiệm vụ chính là dạy cho máy tính định lý
R=T.
- Thay vì chứng minh gốc của Wiles, dự án muốn hình thức hóa phiên bản chứng minh hiện đại đã được tổng quát hóa và đơn giản hóa.
-
Đồng điều tinh thể và cấu trúc lũy thừa chia
- Đồng điều tinh thể là một lý thuyết được phát triển trong thập niên 1960–70 và đóng vai trò quan trọng trong việc hình thức hóa toán học.
- Cấu trúc lũy thừa chia là khái niệm cần thiết để dạy đồng điều tinh thể cho máy tính.
-
Vấn đề tài liệu hóa toán học của con người
- Sự thiếu chính xác trong việc tài liệu hóa toán học đang bộc lộ rõ. Đây là điều giới chuyên môn đều biết, nhưng nhiều trường hợp không được ghi chép đầy đủ.
- Công việc hình thức hóa có thể giúp giải quyết những vấn đề này.
-
Tầm quan trọng của hình thức hóa
- Hình thức hóa toán học là một bước quan trọng để máy móc có thể tự thực hiện các lập luận toán học.
- Nhiều nhà toán học chưa cảm nhận được sự cần thiết của hình thức hóa, nhưng đây là điều thiết yếu để giảm sai sót của con người.
-
Kết luận
- Trong một bài trình bày gần đây, vấn đề hình thức hóa lũy thừa chia đã được giải quyết. Điều này có nghĩa là dự án đã quay trở lại đúng quỹ đạo.
1 bình luận
Ý kiến Hacker News
Nhớ lại thời học cao học từng viết mã nhanh để hỗ trợ giả thuyết Birch và Swinnerton-Dyer. Khi nói trong một buổi seminar rằng mình muốn tìm phản ví dụ, các chuyên gia đã nổi giận. Dù khi đó chưa hiểu được chiều sâu của toán học, điều đó đã khơi gợi trí tò mò.
Cảm thấy vui trước sự phát triển của chủ nghĩa hình thức trong toán học. Với tư cách là lập trình viên, điều này giúp toán học trở nên dễ tiếp cận hơn. Sự bất an trước việc thiếu chủ nghĩa hình thức nên được đối diện bằng sự tò mò.
Các nhà toán học thường có xu hướng lược bỏ chi tiết. Nếu muốn có chứng minh chặt chẽ, bạn cần sự giúp đỡ của chuyên gia. Toán học hiện đại đang đứng trên một nền tảng không ổn định.
Nhớ lại quá trình Andrew Wiles chứng minh FLT. Cảm giác như cách chứng minh của thập niên 1990 giờ đã trở nên lỗi thời.
Nhấn mạnh rằng toán học hiện đại đang được ghi chép chưa đầy đủ. Cần giảm lỗi thông qua các hệ thống hình thức. Việc dạy máy móc hiểu các lập luận toán học là rất quan trọng.
Giải thích sự khác biệt vai trò giữa nhà thiết kế UI/UX và lập trình viên. Thiết kế và phát triển đòi hỏi những cách tư duy khác nhau.
Kỳ vọng các trình chứng minh định lý như Lean sẽ trở thành công cụ quan trọng trong toán học.
Việc xem qua mã Lean rất thú vị. Câu lệnh chứng minh cuối cùng đóng vai trò như một bài kiểm thử đơn vị.
Đặt câu hỏi liệu có khả năng những khái niệm toán học đã được sử dụng suốt hàng chục năm thực ra lại sai.
Giới thiệu từ "vitiated", cho rằng đây là từ phù hợp để dùng khi một chứng minh bị sai.
Đề cập khoảng cách giữa các nhà toán học và kỹ sư, đồng thời kỳ vọng rằng khi máy móc giải toán, hiệu năng cũng sẽ cần được cải thiện.
Bày tỏ sự thất vọng về tình trạng của tài liệu toán học. Dự đoán rằng các tài liệu lý thuyết số từ thập niên 1960 đến 1990 có thể có vấn đề. Cộng đồng chuyên gia càng nhỏ thì lỗi càng dễ bị bỏ qua.