Đây là một câu hỏi quan trọng mà chúng ta phải đối mặt ngày càng nhiều khi các quy trình AI cho Toán học trở nên phổ biến hơn: Tại sao chúng ta lại quan tâm đến việc giải quyết các vấn đề khó? Hầu như luôn luôn, câu trả lời *không* phải là vì chúng ta đặc biệt muốn vấn đề khó được giải quyết. (1/12)

Các câu hỏi như sự tồn tại của các nghiệm mượt mà toàn cầu cho các phương trình Navier-Stokes là điều thú vị về mặt toán học không phải vì câu trả lời tự nó là rất quan trọng, mà vì chúng ta có lý do để tin rằng quá trình *khám phá* câu trả lời rất có khả năng... (2/12)

...để mang lại những hiểu biết sâu sắc mới về phân tích, PDEs, động lực học chất lỏng, v.v., với những kỹ thuật mới để khai thác. Giải quyết bài toán Fermat đã cho chúng ta (một cách gián tiếp) chương trình Langlands. Giải quyết bài toán Poincaré đã cho chúng ta dòng Ricci. Người ta hy vọng rằng việc giải quyết Navier-Stokes sẽ mang lại điều gì đó cũng vĩ đại như vậy. (3/12)

Thật vậy, chúng tôi xác định những vấn đề như vậy là "khó một cách thú vị" chính vì chúng tôi trực giác rằng chúng đại diện cho một "khoảng trống" trong sự hiểu biết và phương pháp hiện tại của chúng tôi. Đó là lý do tại sao những kẻ điên rồ tuyên bố giải quyết (chẳng hạn) giả thuyết Riemann bằng cách sử dụng "mẹo" hoặc các phương pháp cơ bản... (4/12)

...có phần bỏ lỡ điểm chính: nếu một trong những vấn đề lớn này hóa ra có thể giải quyết chỉ bằng những hiểu biết và công nghệ toán học hiện có, đó sẽ là một sự thất vọng to lớn: một nguồn nước mà chúng ta từng nghĩ là đang tuôn trào, thực ra lại cạn kiệt. (5/12)

Điều này có liên quan gì đến AI? Chà, nếu ai đó chấp nhận giả thuyết rằng những vấn đề khó thường thú vị vì những hiểu biết và sự hiểu biết mới mà chúng mang lại, thì điều này đặt ra câu hỏi (trong bối cảnh phát triển AI): ai là người chịu trách nhiệm cho phần "hiểu biết"?

Lấy các chứng minh bằng cách kiệt sức (như trong định lý bốn màu), vốn đã được coi là có phần gây tranh cãi, vì chúng cung cấp phần "chắc chắn về nhận thức" của một chứng minh, mà không nhất thiết cung cấp bất kỳ phần "sự hiểu biết" nào (thường là điều chúng ta quan tâm) (7/12)

Vì vậy, các chứng minh bằng cách kiệt sức chắc chắn không "sai", nhưng theo một cách nào đó chúng là "gian lận", hoặc có lẽ là "tự đánh bại": chúng ngăn chặn một vấn đề có thể mang lại nhiều kết quả, trong khi bỏ qua chính những khía cạnh của toán học làm cho nó thú vị và đáng giá để thực hiện. (8/12)

Tôi nghĩ rằng các chứng minh được tạo ra bởi AI, trong trường hợp không có bất kỳ mức độ hiểu biết hay cái nhìn nào từ phía con người đã tạo ra chúng, nên được coi là tương tự như vậy. Nếu bạn tự động tạo ra một chứng minh Lean cho một định lý lớn, thì thật tuyệt! Nhưng tại sao bạn lại làm điều đó? (9/12)

Nếu bạn không hiểu những hiểu biết/phương pháp mới mà bằng chứng chứa đựng, thì tất cả những gì bạn đã làm chỉ là chuyển gánh nặng trí tuệ từ bản thân mình sang bất kỳ ai sẵn sàng đọc và hiểu nó (và, hy vọng, truyền đạt những hiểu biết chứa đựng trong đó cho người khác). (10/12)

Toán học cuối cùng là một sản phẩm văn hóa của con người (có lẽ là sâu sắc, phong phú và cổ xưa nhất của chúng ta). Việc giải quyết các vấn đề khó chỉ được coi là một *proxy* để mở rộng sản phẩm văn hóa đó. AI đang làm cho việc tạo ra những con đường mới trong hiểu biết toán học trở nên thú vị và dễ dàng hơn bao giờ hết.. (11/12)

...trong hiện vật đó, nhưng nó cũng đang làm cho việc đạt được proxy (tức là giải quyết các vấn đề khó) dễ dàng hơn bao giờ hết, trong khi lại bỏ qua lý do chính mà chúng ta quan tâm ngay từ đầu (tức là làm sâu sắc thêm sự hiểu biết của chúng ta). Xin đừng làm như vậy. (12/12)