Các nhà toán học bắt tay vào chứng minh bằng máy tính cho bài toán 350 năm tuổi 'Định lý cuối cùng của Fermat'

Chứng minh lại Định lý cuối cùng của Fermat bằng ngôn ngữ máy tính

• Giáo sư Kevin Buzzard của Imperial College London dự kiến sẽ bắt đầu viết chứng minh hình thức cho Định lý cuối cùng của Fermat (FLT) bằng trình chứng minh định lý Lean từ tháng 10 năm 2024.
• [Hội đồng Nghiên cứu Khoa học Vật lý và Kỹ thuật Anh quốc EPSRC]EPSRC đã quyết định tài trợ cho giáo sư Buzzard trong 5 năm kể từ tháng đó.
• Bản kế hoạch dự án được tạo bằng plugin Lean blueprints của plasTeX dự kiến sẽ được công bố vào cuối tháng 4 năm 2024.

Định lý cuối cùng của Fermat chẳng phải đã được chứng minh rồi sao?

Đúng là đã được chứng minh. Nhà toán học người Anh Andrew Wiles đã công bố chứng minh vào năm 1994, và chứng minh này được xuất bản chính thức vào năm 1995. Tuy nhiên, hiện vẫn chưa có chứng minh hình thức nào được viết bằng ngôn ngữ của [trình chứng minh định lý tương tác ITP]itp.

Trình chứng minh định lý tương tác? Chứng minh hình thức? Đó là gì?

• [Trình chứng minh định lý tương tác ITP]itp: chương trình máy tính giúp con người viết chứng minh hình thức. Cũng được gọi là [proof assistant].
• Chứng minh hình thức: chứng minh có thể được kiểm chứng bằng một chương trình máy tính gọi là [proof verifier]. Trình chứng minh định lý thường cũng đồng thời đóng vai trò proof verifier.

Trình chứng minh định lý có phải là trí tuệ nhân tạo không?

Có thể xem [trình chứng minh định lý thần kinh NTP]ntp là như vậy, nhưng nhiều trình chứng minh định lý tương tác như Lean không phải là chương trình dựa trên machine learning.

Hãy giới thiệu về trình chứng minh định lý Lean.

• Vừa là trình chứng minh định lý tương tác, vừa là ngôn ngữ lập trình hàm thuần túy.
• Dựa trên lý thuyết kiểu phụ thuộc.
• Có các tính năng như type class, cú pháp mở rộng, macro và metaprogramming.
• So với các proof assistant khác, cộng đồng người dùng Lean có đặc biệt nhiều nhà toán học (nghiên cứu ngoài lĩnh vực nền tảng toán học).

Vì sao lại muốn viết chứng minh hình thức cho Định lý cuối cùng của Fermat?

Trích bài đăng của giáo sư Kevin Buzzard trên X: "Mục tiêu là giúp máy tính hiểu được số học hiện đại, và cuối cùng có thể hỗ trợ các nhà số học."

Liên kết

• Tin nhắn giáo sư Kevin Buzzard đăng trên chat Zulip của Lean vào ngày 3 tháng 10 năm 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
• Thư viện toán học của Lean: https://github.com/leanprover-community/mathlib4
• Bài viết của New Scientist: https://institutions.newscientist.com/article/…
• Bài viết của Popular Mechanics: https://popularmechanics.com/science/math/…

[calofmijuck]

Tôi ủng hộ. Với những ai quan tâm đến formal proof, tôi cũng khuyên nên nghe bài giảng Machine Assisted Proofs của giáo sư Terrence Tao (https://www.youtube.com/watch?v=AayZuuDDKP0).