Các nhà toán học con người bị AI vượt mặt trong việc tìm phản ví dụ

• Các mô hình thuộc dòng ChatGPT và Claude chỉ trong vài tuần đã tạo ra phản ví dụ cho giả thuyết khoảng cách đơn vị của Erdős, câu hỏi về lược đồ nhóm của Grothendieck và Jacobian Conjecture; một số đã được kiểm chứng bằng Lean
• Sol của OpenAI đã hình thức hóa phản ví dụ Erdős cùng kết quả lý thuyết trường lớp toàn cục cần thiết trong 3 tuần thành 1,2 triệu dòng mã Lean, quy mô hơn một nửa 2,3 triệu dòng của mathlib được viết trong 9 năm
• Với câu hỏi 60 năm tuổi của Grothendieck, Sol tìm ra phản ví dụ dài 12 trang và Fable hình thức hóa thành 1.076 dòng trong 4 giờ, xác nhận sự tồn tại của một lược đồ nhóm có cấp 4 nhưng không bị triệt tiêu bởi 4
• Tự động hình thức hóa cũng tăng mạnh tốc độ nghiên cứu: Andrew Yang viết khoảng 250.000 dòng mã Lean trong chừng 2 tuần, gần như hoàn tất dự án về định lý nâng tính mô-đun cần cho Định lý cuối cùng của Fermat
• Không thể tin ngay toán học phi hình thức do AI tạo ra, nhưng nếu biến các giả thuyết thành mệnh đề Lean chính xác thì có thể kiểm tra chứng minh và phản chứng bằng máy; con người cần rút ra trực giác toán học sâu hơn từ các phản ví dụ

---

Giả thuyết khoảng cách đơn vị của Erdős và lý thuyết trường lớp toàn cục

• Ngày 20/5/2026, ChatGPT đã bác bỏ giả thuyết khoảng cách đơn vị của Erdős trong hình học rời rạc
  • Nó xây dựng phản ví dụ bằng cách dùng một định lý số học sâu của Golod và Shafarevich từ thập niên 1960
  • Nhiều nhà toán học đã xem xét lập luận trước và đánh giá là hợp lệ, nhưng tại thời điểm công bố chưa có hình thức hóa Lean
• Ngày 26/5, Mike Freedman, chủ nhân Huy chương Fields và Giám đốc khoa học của Logical Intelligence, thông báo rằng hệ thống của công ty đã tự động hình thức hóa toàn bộ bài báo của ChatGPT sang Lean
  • Phạm vi hình thức hóa là mệnh đề rằng định lý Golod–Shafarevich hàm ý phản ví dụ Erdős
  • Bản thân định lý số học nền tảng cần hơn 100 trang và phụ thuộc vào phần lớn lý thuyết trường lớp toàn cục
• Sau trường hè hình thức hóa lý thuyết trường lớp năm 2025, trong một năm, trường hợp cục bộ gần như đã hoàn tất nhưng trường hợp toàn cục vẫn còn bỏ ngỏ

Bản hình thức hóa hoàn chỉnh 1,2 triệu dòng do Sol tạo ra

• Ngày 26/6, Boris Alexeev của OpenAI công bố trên Lean Zulip rằng ông đã hướng dẫn mô hình mới Sol tạo ra một bản hình thức hóa hoàn chỉnh của phản ví dụ Erdős, không giả định gì ngoài các tiên đề toán học
• Sol đã tạo 1,2 triệu dòng mã Lean trong 3 tuần
  • mathlib, được viết trong 9 năm, có 2,3 triệu dòng
  • Chất lượng mã không đồng đều, nhưng nó thực sự chứng minh các kết quả khó của lý thuyết trường lớp toàn cục và các định lý không tầm thường về đối đồng điều của trường số
• Vì Lean là một ngôn ngữ lập trình có thể chạy lệnh tùy ý, mã được tạo đã được chạy trong sandbox để tính đến khả năng có mã độc
• Quy mô và tốc độ này dẫn tới nhận định rằng phát triển toán học quy mô lớn do AI tạo ra là điều không thể tránh khỏi

Workshop Formalizing Fermat và khả năng tiếp cận công cụ

• Workshop Formalizing Fermat diễn ra từ ngày 6–10/7 có 25 người tham dự, nhưng hệ thống hình thức hóa tự động của nhà tài trợ Logos Research chỉ cho phép 5 người dùng đồng thời
• Mọi người tham dự được cung cấp gói Claude Max một tháng để dùng Claude Fable, và OpenAI cũng miễn phí quyền truy cập ChatGPT Pro trong một tháng
  • Sol dự kiến ra mắt ngày 9/7
  • Fable dự kiến kết thúc ngày 7/7, nhưng quyền truy cập thực tế vẫn được duy trì
  • Người tham dự có thể dùng Sol và Fable trong 4 trên 5 ngày của workshop, và dùng công cụ Logos trong suốt thời gian
• Để phát triển lý thuyết lược đồ nhóm phẳng hữu hạn cần cho việc hình thức hóa Định lý cuối cùng của Fermat, họ đưa các bài báo kinh điển vào Fable và ChatGPT và yêu cầu viết phần diễn giải bằng ngôn ngữ tự nhiên
  • Logos phát hiện một mệnh đề trong phần diễn giải là sai và đưa ra một phản ví dụ tường minh
  • Khi kiểm tra, tài liệu do LLM tạo mô tả một cấu trúc chuẩn đã sai, và con người đã bỏ sót lỗi trong lúc đọc
  • Điểm khác biệt là thay vì chỉ trả lời rằng nó không hiểu lập luận, hệ thống đã cung cấp chứng minh rằng lập luận sai

Câu hỏi về lược đồ nhóm của Grothendieck

• Giáo sư Akhil Mathew tại UChicago đề xuất cho AI câu hỏi lâu đời của Grothendieck: liệu mọi lược đồ nhóm tự do hữu hạn có cấp (n) đều bị triệt tiêu bởi (n) hay không
  • Deligne đã chứng minh trường hợp giao hoán
  • Grothendieck đã chứng minh trường hợp không gian nền là reduced
  • Rene Schoof đã xử lý thêm nhiều trường hợp, và Emiliano Torti cũng chứng minh trường hợp tổng quát hơn trong bài báo năm trước
• Ngày 11/7, một ngày sau workshop, Sol tìm ra phản ví dụ và tạo một PDF dài 12 trang
  • Khi được yêu cầu bản hình thức hóa Lean đầy đủ thay vì kết quả phi hình thức, Fable đã tự động hình thức hóa thành 1.076 dòng trong 4 giờ
• Trước tiên, họ kiểm tra xem tệp Lean chỉ chứa các định lý, không có lệnh như xóa tệp, rồi biên dịch trên laptop
  • Kiểm tra mệnh đề chỉ dùng các khái niệm của mathlib
  • Kiểm tra mệnh đề có thực sự biểu thị sự tồn tại của phản ví dụ hay không
  • Kiểm tra chứng minh có biên dịch bình thường hay không
  • Toàn bộ quá trình xác minh mất chưa đến 5 phút
• Kết quả xác minh cho thấy tồn tại lược đồ nhóm có cấp 4 nhưng không bị triệt tiêu bởi 4
• Akhil Mathew đã gửi phản ví dụ này dưới dạng PR mathlib
• Trong khi phản ví dụ Erdős khoảng 1 triệu dòng, phản ví dụ Grothendieck đơn giản hơn nhiều, khoảng 1.000 dòng, nhưng vẫn là một trường hợp máy giải quyết một câu hỏi 60 năm tuổi trong hình học đại số

Phản ứng của chuyên gia và định lý nâng tính mô-đun

• Ngày 14/7, một giáo sư tại Imperial College đánh giá rằng việc phản ví dụ Grothendieck được phát hiện dễ dàng chỉ cho thấy con người chưa suy nghĩ đủ lâu về bài toán đó
• Nghiên cứu sinh Andrew Yang đã dùng Sol và Fable khi hình thức hóa bằng Lean định lý nâng tính mô-đun, vốn quan trọng với Định lý cuối cùng của Fermat
  • Anh viết 250.000 dòng mã Lean trong khoảng 2 tuần
  • Nhờ đó, dự án về cơ bản đã hoàn tất
• Một giáo sư khác tại Imperial ban đầu thấy khó hiểu khi các nghiên cứu sinh trả 200 USD mỗi tháng cho Sol và Fable, nhưng sau khi thấy thành quả này thì lại cho rằng nghiên cứu sinh nào không chi 200 USD/tháng cho công cụ mới là thiếu hợp lý
• Harvard đã cung cấp quyền truy cập Fable miễn phí cho toàn bộ nghiên cứu sinh tiến sĩ, nghiên cứu viên sau tiến sĩ và giáo sư

Phản ví dụ cho Jacobian Conjecture

• Akhil Mathew và Levent Alpöge đã thảo luận cách tìm thêm phản ví dụ trong hình học đại số, và Fable đã tìm ra phản ví dụ cho Jacobian Conjecture, một bài toán nổi tiếng đã mở trong khoảng 100 năm
• Levent Alpöge công bố trên X kết quả có vẻ đã được giải trong lúc diễn ra trận chung kết World Cup 2026
• Khi Akhil Mathew đề xuất một PR mathlib mới, Paul Lezeau đã hình thức hóa thủ công phản ví dụ và gửi PR tới kho Formal Conjectures của DeepMind
• mathlib không có danh sách quy mô lớn các giả thuyết toán học, nhưng kho Formal Conjectures thì có
• Khi con người thống nhất được một mệnh đề Lean phản ánh trung thành ý nghĩa của giả thuyết, việc kiểm tra liệu mã do AI tạo ra chứng minh hay bác bỏ giả thuyết đó trở nên đơn giản

Những việc còn lại cho con người sau kiểm chứng hình thức

• Với Jacobian Conjecture, bước tiếp theo là con người hiểu chính xác điều gì đang xảy ra trong phản ví dụ đó
• Với phản ví dụ Grothendieck, công việc đang tiếp diễn nhằm hiểu sâu hơn, vượt khỏi mức liệt kê các biểu diễn và phép tính trên vành tùy ý
• Giá trị của phản ví dụ không chỉ nằm ở việc khép lại bài toán về mặt hình thức, mà được hoàn thiện trong quá trình rút ra trực giác để con người hiểu toán học tốt hơn

[GN⁺]

Ý kiến Hacker News

• Thời học cao học, tôi từng có cơ hội trực tiếp đóng góp cho một bài toán mở trong lớp nghiên cứu của giáo sư hướng dẫn. Một ngày thứ Sáu, giáo sư đưa ra một giả thuyết trơn tru và đẹp đẽ mà ông hy vọng là đúng, nhưng tôi vốn thích những ngoại lệ kỳ quặc và cũng thiếu công cụ để chứng minh, nên tập trung tìm phản ví dụ và tìm ra chỉ trong một giờ
  Giáo sư đã thất bại trong việc chứng minh nó suốt cả cuối tuần; đây là một ví dụ cho thấy khi những người có công cụ, kỳ vọng và động lực khác nhau nhìn vào cùng một vấn đề, họ có thể đóng góp theo những hướng hoàn toàn khác nhau. Tôi không thể sánh với một người hướng dẫn vĩ đại, nhưng ít nhất vào lúc đó tôi có lý do để nhìn theo hướng khác, và điều đó dẫn tới phản ví dụ nhỏ bé duy nhất của tôi trong nghiên cứu toán học

  • Có lẽ đây cũng là lý do máy móc giỏi tìm phản ví dụ. Nó không có sự ám ảnh thẩm mỹ với một giả thuyết, cũng không xấu hổ khi đưa ra một kết quả xấu xí
  • Với tư cách là nhà toán học, cảm nhận của tôi lại ngược lại. Chứng minh thì có thể làm bằng cách biến đổi đôi chút từ những chứng minh mình đã biết, nhưng để tạo ra phản ví dụ thì phải hiểu rất sâu cấu trúc của đối tượng, nên nhiều khi vượt quá khả năng của tôi
    Tuy vậy, có lẽ là vì tôi chủ yếu xử lý các đối tượng trừu tượng khó nắm bắt; với số hay đa thức thì có thể ngược lại
  • Những giáo sư, nhà nghiên cứu, giáo viên công khai các bài toán chưa giải được cho sinh viên và khuyến khích họ tham gia xứng đáng được đánh giá cao hơn. Trong buổi học kỹ thuật đầu tiên ở đại học, khi giảng viên nói với sinh viên năm nhất rằng “đây là những bài toán mà chúng tôi vẫn chưa giải được, nếu có ý tưởng gì hãy cho tôi biết”, tôi cảm thấy được chào đón và là một phần của cộng đồng hơn bao giờ hết, và điều đó đã truyền cảm hứng lớn ở giai đoạn đầu vốn dễ trở nên tẻ nhạt của việc học
  • Trong 《How to Solve It》 cũng có gần như đúng câu chuyện này
  • Có một giai thoại về Zeeman còn cực đoan hơn nhưng theo hướng ngược lại. Ông đã dành nhiều năm để tìm một mặt cầu thắt nút trong không gian 5 chiều, rồi nhận ra điều đó là bất khả và chứng minh được chỉ trong vài giờ
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• Yitang Zhang, nổi tiếng với giả thuyết cặp số nguyên tố sinh đôi, đã nghiên cứu giả thuyết Jacobian suốt 7 năm tại Purdue dưới sự hướng dẫn của Tzuong-Tsieng Moh. Hóa ra bước cốt lõi trong luận án của ông dựa vào một hệ quả sai của Moh, Moh từ chối viết thư giới thiệu, và Zhang không thể tìm được việc giảng dạy hay nghiên cứu nên phải làm ở Subway trong nhiều năm
  Tôi tự hỏi sẽ ra sao nếu khi ông bắt đầu nghiên cứu năm 1986 đã có ChatGPT. Giờ đây nó đã thành một câu chuyện thành công đầy cảm hứng, nhưng cũng gợi lên những cảm xúc phức tạp, như câu thơ “Cuộc đời của Yu Xin vô cùng hiu quạnh, nhưng thơ phú lúc cuối đời đã làm rung động Giang Quan”

  • Tôi từng thấy trong buổi bảo vệ tiến sĩ toán học, một giáo sư trong hội đồng phát hiện ra lỗi trong chứng minh. Khi nghiên cứu sinh hiểu ra và hỏi “giờ thì phải làm sao?”, vị giáo sư đó chỉ nhún vai
  • Về sau ông ấy đã thành công với giả thuyết cặp số nguyên tố sinh đôi, nên có thể gọi là cảm động, nhưng tôi đã mệt mỏi với những câu chuyện kiểu này trong học giới. Có quá nhiều chính trị và quản lý danh tiếng, và Zhang lẽ ra không nên phải chịu khổ như vậy
    Khi mở rộng nghiên cứu sang phía toán học, tôi đã sốc khi thấy khá nhiều mệnh đề trong tài liệu là sai, và còn lan rộng sang cả tài liệu ứng dụng. Ngay cả khi chỉ ra vấn đề, nhiều người vẫn phản ứng bằng phòng thủ và phủ nhận như trong giai thoại về Zhang. LLM hữu ích cho chứng minh nhưng cũng sai rất nặng; nó giống như thêm một người nữa đề xuất hướng tìm kiếm bằng trực giác khác, nên có lẽ cả vào năm 1986 kết quả cũng vẫn vậy
  • Ý câu thơ mà ChatGPT chuyển là: “Cuộc đời của Yu Xin hết sức hiu quạnh, nhưng thơ và phú lúc tuổi già đã làm rung động vùng sông hồ”

• Trong toán học, phản ví dụ rất quan trọng để tinh chỉnh định nghĩa và làm sắc bén chứng minh. Tôi khuyên đọc cuốn 《Proofs and Refutations》 của Imre Lakatos xuất bản năm 1976; trong tô pô, xác suất, giải tích... cũng có khá nhiều sách chỉ chuyên về phản ví dụ
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Nếu tìm được phản ví dụ, ta không lãng phí thời gian cố chứng minh một mệnh đề sai và có thể chuyển sang bài toán khác, nên ít nhất trong toán học nó giúp thời gian của nhân loại được dùng hiệu quả hơn

  • Bác bỏ bằng phản ví dụ thì hiệu quả, nhưng rốt cuộc lại không thật sự thỏa mãn. Nó cho ta câu trả lời, nhưng không giúp hiểu vì sao toán học vận hành như vậy, cũng không dẫn tới những câu hỏi mới
    Chừng nào con người vẫn là bên phán xét chứng minh nào là thanh nhã và sâu sắc, thì nhà toán học con người vẫn còn việc để làm
  • Phản ví dụ cũng hữu ích trong việc tinh chỉnh phát biểu của định lý. Trong nghiên cứu khoa học máy tính lý thuyết, việc cố chứng minh một định lý mà mình mong là đúng, rồi tìm ra phản ví dụ, sửa lại mệnh đề và tiếp tục là chuyện rất thường gặp
    Việc nhiều định lý của khoa học máy tính xử lý định nghĩa quy nạp và đồng quy nạp cũng là một lợi thế
  • Đặc biệt nếu phản ví dụ được kiểm chứng hình thức, thì nó gần như ngay lập tức biến nhiều năm nỗ lực suy đoán thành một câu trả lời dứt khoát
  • Nhưng nhìn tổng thể thì cũng không thể khẳng định thời gian đã được dùng hiệu quả hơn. Dù là chứng minh hay bác bỏ một mệnh đề, cuối cùng đúng hay sai, quá trình đó vẫn có thể tạo ra những hiểu biết mới

• Có lẽ cả phiên bản toán học của 《Ballad of John Henry》 cũng sẽ do AI viết. Tôi tò mò không biết nhà vô địch con người cuối cùng nào sẽ đưa ra được một chứng minh “xứng đáng có mặt trong THE BOOK” mà ngay cả máy móc cũng không thể vượt qua
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Đây là một góc nhìn không lành mạnh, xem toán học như cạnh tranh kiểu người hâm mộ bóng đá. Điều có giá trị nhất trong toán học không chỉ là những chứng minh đẹp mà còn là định nghĩa hữu ích, và việc tạo ra những định nghĩa tốt cùng các giả thuyết tốt từ đó vẫn là lĩnh vực mà LLM chưa thật sự chinh phục
  • Dù chưa đến mức kịch tính như vậy, nhưng có thể sớm đạt đến giai đoạn đó. Không có cơ sở mang tính cấu trúc để dự đoán liệu năng lực AI sẽ tiến bộ tiệm cận hay tăng tốc, và cả hai khả năng về việc những bài toán nào sẽ được giải bằng phương pháp mới đều còn bỏ ngỏ
    Chúng ta không hiểu rõ nội tại và đường cong tăng trưởng của năng lực AI, thậm chí cũng không biết chính xác liệu nó có đang cố tình tỏ ra kém hơn thực lực hay không. Nó có thể là một hiện tượng trồi hiện chống lại việc đo lường, hoặc vài năm nữa lại trở nên dự đoán được như đồng hồ. Không ai biết; và nếu có người biết thì họ cũng không nói, còn những người lớn tiếng thì cũng chẳng biết gì

• Nếu có thể đẩy nhanh đáng kể những thành quả có ý nghĩa của nghiên cứu sinh, thì không có lý do gì để không đầu tư 2.400 USD/năm cho mỗi sinh viên. Xét trên tổng chi phí thì gần như chỉ là tiền lẻ

  • Một số nghiên cứu sinh không xem mình là một “cỗ máy tạo ra kết quả có ý nghĩa” mà là một chủ thể đạo đức. Ai cũng biết rằng ngay cả các LLM hữu ích cũng khó được biện minh vì dữ liệu huấn luyện bị chiếm dụng và tác động môi trường khổng lồ
  • Học bổng sinh hoạt cho nghiên cứu sinh EPSRC vào khoảng 20.000 bảng Anh, nên con số này tương đương khoảng 10% chi phí hằng năm. Với cá nhân sinh viên, đây là gánh nặng lớn

• Hồi còn học đại học, giá mà đã có các bản hình thức hóa Lean do LLM tạo ra. Toán trong slide bài giảng có rất nhiều lỗi, và một số giáo sư còn từ chối giải thích khi bị yêu cầu làm rõ với câu “chứng minh nằm trong slide”, đồng thời lại rất miễn cưỡng thừa nhận sai sót
  Bản thân chứng minh Lean thường không phù hợp để hiểu trực tiếp, nhưng vẫn hy vọng có thể dùng nó làm nền để tạo ra các lập luận dễ hiểu hơn cho con người

  • Khó đồng ý với nhận định đầu tiên. Đường cong học tập tuy dốc, nhưng một bản hình thức hóa Lean·Agda·Rocq được viết tốt lại cực kỳ xuất sắc trong việc giúp hiểu chứng minh. Một bản hình thức hóa tốt cho thấy cấu trúc của đề cương và lập luận cốt lõi, đồng thời khác với chứng minh trên giấy ở chỗ cho phép kiểm tra chi tiết của mọi bước đến bất kỳ độ sâu nào mong muốn
    Kho lưu trữ Agda TypeTopology của Martín Escardó là một ví dụ hay. Ngược lại, các bản hình thức hóa do LLM tạo ra hiện nay có thể rất lộn xộn, nên dù có chứng thực được mệnh đề và chứa lập luận thú vị thì vẫn cần khá nhiều công sức để gọt giũa thành dạng có thể nâng cao hiểu biết toán học. Hướng dẫn Agda tương tác có tại lets-play-agda.quasicoherent.io
  • Hình thức hóa cũng có thể được dùng cho cách tiếp cận kiểu Leibniz nhằm chấm dứt tranh cãi và loại bỏ hoàn toàn nghi ngờ

• Tò mò không biết với các nhà toán học, phản ví dụ có giống như một kết quả bất ngờ trong khoa học vật lý — trước mắt thì phiền phức nhưng cực kỳ quan trọng vì phơi bày sự thiếu chính xác của mô hình — hay giống như báo cáo lỗi trong lập trình, tức chỉ là chi tiết nhỏ nhặt và gây khó chịu

  • Phản ví dụ giúp làm rõ vai trò của các điều kiện. Nếu có những phản ví dụ đơn giản và dễ nhớ nhất cho thấy điều gì thất bại khi vi phạm từng điều kiện trong chứng minh thì sẽ rất hữu ích
    Các nhà toán học có xu hướng mang theo trong đầu một vườn thú phản ví dụ. Ngay cả khi khôi phục lại một định lý, họ cũng có thể nhớ đến những phản ví dụ sắc bén và đáng nhớ đó để thu hẹp miền xác định và các điều kiện nhằm loại chúng ra
  • Có những sách giáo khoa dùng phản ví dụ để dạy các khác biệt tinh tế của một lĩnh vực, như 《Counterexamples in Topology》 và 《Counterexamples in Analysis》. Chúng rất được ưa chuộng vì việc học chi tiết qua các ví dụ bệnh lý hoặc suy biến thường dễ hơn là chỉ học các đối tượng chuẩn tắc như dự định

• Phần lớn toán học này khá khó hiểu, nhưng nhìn chung có vẻ đang nói về chứng minh định lý. Nếu toán học AI tiếp tục tăng tốc, không biết sau này nó có phát hiện ra toán học mới để ứng dụng vào kỹ thuật hay y sinh hay không, liệu nhân loại có đang ở ngay trước một bước đột phá lớn, hay nó sẽ chỉ dừng ở việc chứng minh những điều đã biết

  • Có khả năng. Compressed sensing có thể được xem là một ví dụ về toán học mới được ứng dụng trong y sinh, và nó có thể rút ngắn đáng kể thời gian chụp MRI, cải thiện trải nghiệm của bệnh nhân và giúp nhiều người được kiểm tra hơn
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Dù có được ứng dụng vào kỹ thuật và y sinh thì có lẽ cũng là chuyện dài hạn, nhưng sự phát triển của các phương pháp toán học mới có thể trở nên quan trọng với nghiên cứu vật lý cơ bản sớm hơn. Đã nhiều lần mô hình được cải thiện lớn nhờ sự xuất hiện của các công cụ toán học cho phép biểu diễn hoặc kiểm chứng các mô hình vũ trụ
  • Dù có thể đi nữa thì cũng sẽ mất rất lâu. Trong hầu hết các lĩnh vực ứng dụng, ngay cả toán học từ vài trăm năm trước cũng chỉ mới bắt đầu được khai thác đúng mức

• Một ngày nào đó, các nhà toán học có thể bị chôn vùi trong những chứng minh cần phải rà soát, và các mệnh đề sai do quá tự tin có thể lọt vào giới toán học. Các nhà toán học tương lai có lẽ sẽ giống các kỹ sư phần mềm dùng AI, phải kiểm tra hàng nghìn dòng chứng minh do AI tạo ra để tìm những lỗi tinh vi

  • Thời điểm đó thực ra đã đến từ lâu. Tài liệu học thuật ngày nay đồ sộ và đầy rẫy những chứng minh sai, và ngay cả trong các kết quả đã xuất bản cũng có một số lượng kết quả sai không thể biết chính xác, nhưng chắc chắn không phải là 0