Cập nhật về các bài viết nghiên cứu và khảo luận, thảo luận về các bài toán mở cùng các chủ đề toán học khác. Bài viết của Terence Tao ngày 9 tháng 10 năm 2026 trong mục math.GM, quan điểm | Thẻ: AI, Lean, Thomas Hales | Tác giả: Terence Tao [Đây là bài khách mời của Thomas Hales. Bài viết này ban đầu được soạn ở định dạng khác và chuyển đổi bằng sự hỗ trợ của AI. — T.] Các nhà toán học đã chia sẻ góc nhìn về những giá trị họ trân trọng trong toán học. Với tôi, điều quan trọng là tính nhất quán của toán học và độ tin cậy tuyệt đối trong việc hỗ trợ khoa học cũng như văn minh nhân loại. Một chứng minh hình thức là chứng minh toán học đã được kiểm tra cẩn thận ở cấp độ nền tảng toán học và các quy tắc logic cơ bản. Về lý thuyết, việc này có thể thực hiện thủ công, nhưng do số lượng các bước quá lớn, công việc này thường được xử lý bằng máy tính thông qua phần mềm chuyên dụng. Các định lý từng được hình thức hóa bao gồm định lý bốn màu, định lý Feit-Thompson (bậc lẻ), phỏng đoán Kepler, phép nghịch đảo mặt cầu, bài toán xếp cầu trong không gian 8 và 24 chiều, hiện tượng bùng nổ cưỡng bức Navier-Stokes và định lý lớn Fermat. Ba dự án hình thức hóa cuối cùng đã hoàn thành trong năm nay và thu hút sự chú ý rộng rãi về tiềm năng của phương pháp này.
Nguồn chính
- THẢO LUẬNmatt_dnews.ycombinator.com