Bài toán Erdős #728 được AI giải gần như tự động

• Bài toán Erdős #728 gần đây đã được các công cụ AI giải gần như tự động, đánh dấu một cột mốc mới trong tự động hóa nghiên cứu toán học
• Bài toán ban đầu là một câu hỏi về phân tích thừa số nguyên tố của hệ số nhị thức do Erdős, Graham, Ruzsa, Strauss nêu ra năm 1975, nhưng vì điều kiện diễn đạt mơ hồ nên trong thời gian dài chưa được xử lý rõ ràng
• ChatGPT tạo ra chứng minh dưới các ràng buộc đã được điều chỉnh, còn Aristotle chính thức hóa nó thành chứng minh hình thức Lean và tự động sửa lỗi
• Sau đó, nhiều người tham gia đã dùng ChatGPT để viết lại bằng ngôn ngữ tự nhiên và lặp lại quá trình cải thiện các phiên bản với liên kết tài liệu tham khảo và cấu trúc tường thuật tốt hơn
• Terence Tao đánh giá rằng quá trình này cho thấy khả năng viết và chỉnh sửa chứng minh rất nhanh của AI có thể làm thay đổi chính cách thức viết bài báo nghiên cứu

---

AI đã giải bài toán Erdős #728

• Gần đây, việc áp dụng công cụ AI đã tạo ra tiến triển mới trong giải các bài toán Erdős, và bài toán #728 đã được AI giải gần như tự động
  • Sau nỗ lực ban đầu, phiên bản đã sửa theo phản hồi đã thành công
  • Kết quả không được tái hiện nguyên dạng trong tài liệu hiện có, chỉ có những kết quả tương tự với phương pháp gần giống
• Trường hợp này cho thấy trong vài tháng gần đây, năng lực giải quyết bài toán toán học của AI thực sự đã được cải thiện
  • Trước đây cũng từng có trường hợp AI giải bài toán Erdős, nhưng phần lớn sau đó được xác nhận là lời giải đã tồn tại sẵn trong tài liệu
• Bài toán lần này ban đầu được Erdős mô tả dưới một dạng sai, và chỉ gần đây mới được tái cấu trúc về đúng dạng dự định
  • Điều này được xem là lý do khiến tài liệu hiện có thiếu các nghiên cứu liên quan

Lịch sử bài toán và cách tiếp cận ban đầu

• Năm 1975, Erdős, Graham, Ruzsa, Strauss nghiên cứu phân tích thừa số nguyên tố của hệ số nhị thức (2n choose n) và nêu ra nhiều bài toán liên quan
  • Một trong số đó hỏi liệu có tồn tại vô hạn các bộ a, b, n sao cho thỏa mãn điều kiện a!b! | n!(a+b−n)! và a+b > n + C log n hay không
  • Tuy nhiên, nhiều phần được diễn đạt không rõ ràng, chẳng hạn như độ lớn của C (nhỏ hay lớn)
• Vài tháng trước, nhóm AlphaProof đã tìm ra một lời giải đơn giản cho bài toán, nhưng nó không phù hợp với tinh thần của bài toán như dự định nên đã thêm ràng buộc a,b ≤ (1−ε)n
  • Sau đó, ngay cả khi dùng AI hỗ trợ tra cứu tài liệu, cũng hầu như không tìm thấy nghiên cứu liên quan

Sự phối hợp giữa ChatGPT và Aristotle

• Ngày 4 tháng 1, ChatGPT đã tạo ra một chứng minh cho trường hợp C nhỏ dưới các ràng buộc đã điều chỉnh
  • Chứng minh này được Aristotle chính thức hóa thành chứng minh hình thức Lean
  • Sau khi rà soát lại văn bản gốc, người ta xác nhận rằng bài báo ban đầu đã thực sự xử lý trường hợp C nhỏ
• Một người tham gia khác đã chuyển chứng minh Lean sang văn xuôi tự nhiên bằng ChatGPT, rồi thông qua các cuộc trao đổi bổ sung viết ra phiên bản cải tiến
  • Phiên bản này đã lấp được một số khoảng trống trong chứng minh, nhưng vẫn còn văn phong gượng kiểu AI và thiếu trích dẫn tài liệu
  • Dù vậy, nó đã đạt đến mức đủ dễ đọc để có thể hiểu được ý tưởng cốt lõi

Viết lại quy mô lớn và kết quả được cải thiện

• Thông qua các prompt bổ sung, ChatGPT đã tạo ra chứng minh mở rộng sang cả trường hợp C lớn
  • Có một số lỗi, nhưng Aristotle đã tự động sửa và hoàn thành chứng minh đã được Lean kiểm chứng
• Người tham gia thứ ba sau đó nén chứng minh Lean, rồi một người khác trao đổi lâu dài với ChatGPT để
  • viết lại thành một bài báo hoàn chỉnh hơn với liên kết tài liệu và cấu trúc tường thuật được củng cố
  • Kết quả được đánh giá là bớt cảm giác do AI tạo ra, với chất lượng tiệm cận mức bài báo nghiên cứu
  • Tao cho biết ông đã xem xét văn bản này trên diễn đàn bài toán Erdős

AI đang thay đổi cách viết bài báo nghiên cứu

• Tao cho rằng trong bài báo cuối cùng, những phần cốt lõi vẫn cần do con người viết, nhưng
  • ông đánh giá rằng sự kết hợp giữa AI và Lean đã tăng tốc đột biến việc viết và sửa chứng minh
• Trước đây, để khiến một bài báo trở nên dễ đọc thường tốn rất nhiều thời gian,
  • và các chỉnh sửa theo phản hồi phản biện cũng thường chỉ dừng ở những thay đổi cục bộ
• Nhưng giờ đây, khi khả năng tạo và chỉnh sửa văn bản của AI kết hợp với chức năng kiểm chứng của công cụ chứng minh hình thức,
  • người ta có thể nhanh chóng tạo ra các phiên bản bài báo mới với nhiều mức độ chính xác và cách diễn đạt khác nhau
• Bên cạnh một “bài báo chính thức”, còn có thể tồn tại nhiều phiên bản phụ trợ do AI tạo ra,
  • mở ra khả năng mang lại nhiều góc nhìn và giá trị bổ sung

Phản ứng của cộng đồng

• Một số người dùng mô tả giá trị bổ sung của tài liệu do AI tạo ra là “khả năng nhìn vấn đề từ góc độ khác”
• Các nhà toán học khác nêu ra nhu cầu đo lường mức độ nguyên bản của kết quả AI hoặc đánh giá mức độ tương đồng với tài liệu hiện có
  • Ví dụ, có đề xuất đo độ tương đồng định lượng bằng cách so sánh độ dài của chứng minh hình thức Lean
• Một bình luận khác cho rằng AI có thể viết lại bài báo ở quy mô toàn cục như refactor code,
  • nên các nhà nghiên cứu sẽ cần tập trung hơn vào thiết kế cấu trúc tài liệu ở cấp độ cao hơn
• Một số người tỏ ra hoài nghi về khả năng AI thay thế vai trò của nhà toán học, nhưng
  • những người khác xem đây là cơ hội mới cho hợp tác và mở rộng tư duy

[GN⁺]

Ý kiến trên Hacker News

• Tôi làm việc tại Harmonic, và muốn đính chính một vài hiểu lầm về Aristotle mà chúng tôi tạo ra
  Aristotle tích cực sử dụng các kỹ thuật AI hiện đại, bao gồm cả mô hình ngôn ngữ
  Nếu nhập vào một chứng minh không chính thức bằng tiếng Anh, khi chứng minh đó đúng thì xác suất được dịch sang Lean là khá cao. Nói cách khác, đây là một tín hiệu mạnh cho thấy chứng minh tiếng Anh đó vững chắc
  Một khi đã được hình thức hóa bằng Lean, thì không còn nghi ngờ gì về tính đúng đắn của chứng minh đó. Đây là cách tiếp cận cốt lõi của chúng tôi — nếu tìm ra đáp án thông qua quá trình tìm kiếm do AI dẫn dắt, chúng tôi có thể đảm bảo độ chính xác của kết quả bất kể mức độ phức tạp của nó

  • Tôi tò mò không biết họ xác minh thế nào rằng chứng minh do AI dịch sang Lean thực sự là sự hình thức hóa đúng của bài toán. Trong các lĩnh vực khác, AI tạo sinh rất giỏi tạo ra những lời bịa đặt có vẻ hợp lý, nên tôi muốn biết liệu ở đây cũng có khả năng như vậy không
  • Tôi thắc mắc liệu đã có ai thử áp dụng công nghệ này vào kiểm chứng phần mềm chưa
    Rust dùng một tập quy tắc cố định để đảm bảo an toàn bộ nhớ, nhưng các quy tắc này khá đơn giản và hạn chế. Nếu một hệ thống như Aristotle được tích hợp vào compiler, để mã nào có thể chứng minh tính đúng đắn thì tự động được thông qua, điều đó sẽ thật tuyệt
  • Mỗi khi có một LLM mới, tôi lại băn khoăn không biết đó là tiến bộ thật hay chỉ là hack benchmark, nhưng tôi nghĩ việc hình thức hóa chứng minh toán học là một chỉ dấu cho thấy tiến bộ thực sự
    Tôi tò mò không biết Harmonic sẽ mất bao lâu để có thể hình thức hóa phần lớn toán học do con người viết ra. Đối thủ Christian Szegedy thì nói rằng điều đó có thể làm được ngay trong năm nay
  • Bạn nói rằng nếu chứng minh tiếng Anh là đúng thì xác suất dịch sang Lean sẽ cao, tôi tò mò không biết điều này có thay đổi theo độ khó của từng lĩnh vực toán học hay không. Tôi hiểu là vẫn còn nhiều hướng nghiên cứu mà ngay cả con người cũng khó hình thức hóa
  • Tiền đề “nếu mệnh đề đã được hình thức hóa đúng” nghe như một giả định khá lớn. Như vụ Navier-Stokes gần đây cho thấy, bản thân việc hình thức hóa đã không hề dễ

• Theo cách Terence Tao mô tả, có vẻ như con người đã chuyển qua lại kết quả giữa hai công cụ AI, còn AI thì lấp những chỗ trống mà con người tìm ra
  Điều này gần với hợp tác giữa con người và AI hơn là một lời giải hoàn toàn tự động. Tức là chuyên gia dẫn dắt còn AI đóng vai trò hỗ trợ

  • Đúng vậy, tôi hiểu là thực tế đã diễn ra dưới dạng tương tác giữa Aristotle, ChatGPT và một người dùng cực kỳ xuất sắc
  • Tôi nghe rằng không phải Tao hay cộng đồng trực tiếp tìm ra chỗ hổng, mà họ dùng một trình kiểm chứng chứng minh tự động. Nếu vậy thì có vẻ tỷ lệ là khoảng AI 90% / con người 10%
  • Có phần giải thích chi tiết của tác giả trên Reddit — bài đăng Reddit
  • Để hiểu mức độ chuyên môn và công sức của con người, tôi khuyên nên đọc thread trên diễn đàn bài toán Erdős
  • Nhân tiện, trang này do nhà toán học Thomas Bloom tạo ra, và ChatGPT đã giúp thiết lập kỹ thuật (trích FAQ)

• Việc tái cấu trúc các chứng minh sẵn có hoặc kết hợp chúng theo cách mới là một quá trình nhàm chán hoặc phức tạp với con người, nhưng AI có thể làm việc này với tốc độ siêu phàm
  Cách tiếp cận như vậy sẽ mở ra tiềm năng rất lớn ngay cả trước giai đoạn AGI. Có lẽ sắp tới sẽ là thời đại các nhà toán học dùng AI như công cụ để xử lý những bài toán cực khó như Millennium Problems

  • Tôi nghĩ không có ranh giới rõ ràng giữa việc tái cấu trúc chứng minh hiện có và việc tạo ra toán học hoàn toàn mới
  • Vì toán học có tính logic, chắc hẳn đã có nhiều thuật toán cho kiểu tìm kiếm này, nên có vẻ không chỉ đơn giản là một bài toán tìm kiếm
  • Tôi cũng đồng ý về phần tái cấu trúc chứng minh cũ. Việc kiểm chứng kết quả do LLM đưa ra vẫn là công việc nhàm chán, nhưng ít nhất vẫn tốt hơn việc con người phải tự làm từ đầu
    Giá trị thực sự của LLM nằm ở khả năng đưa ra góc nhìn mới trong những chủ đề có thể diễn đạt bằng ngôn ngữ
  • Tôi gọi hiện tượng này là “refactoring khoa học”. Ví dụ như AI có thể tự động thử nghiệm kiểu thay đổi một hằng số rồi triển khai lại toàn bộ lập luận
  • Nếu một AI có thể chứng minh các định lý phức tạp mà vẫn chưa được xem là AGI, thì tôi thật sự không biết thế nào mới là AGI

• Nếu đọc bài viết giải thích của người thực sự giải bài toán, điều gây ấn tượng là họ đạt được kết quả chỉ với vài prompt, không cần một pipeline khổng lồ
  Các mô hình gần đây dùng nhiều tài nguyên tính toán hơn rất nhiều, nên điều này thậm chí còn có vẻ như một mức sàn thành tích

• Terence Tao đã tạo một trang wiki có tên “AI contributions to Erdős problems”
  Theo trang GitHub và bài trên Mathstodon, kết quả lần này (bài toán 728) là “mục màu xanh lá” đầu tiên trên trang đó, tức là trường hợp đầu tiên AI thực sự giải được

  • Điều thú vị là phần lớn các chứng minh được AI hình thức hóa trong mục 6 của wiki đều mới được hoàn thành trong vài tháng gần đây. Rất đáng mong chờ những gì sẽ tới

• Tôi tò mò không biết các chuyên gia trong những lĩnh vực phức tạp như vật lý hay toán học có đang trò chuyện với AI để nhận trợ giúp hay không

  • Tôi là tiến sĩ toán thuần rồi chuyển sang làm data scientist. AI rất hữu ích khi rà soát tài liệu hoặc ôn lại nhanh những phần toán mình không quen
    Xét theo từng lĩnh vực, mức độ hữu ích giảm dần theo thứ tự: lập trình > ML ứng dụng > thống kê/toán ứng dụng > toán thuần
  • Tôi không học vật lý chuyên sâu, nhưng nhờ AI mà thời gian tìm công thức hay bài báo mình cần đã giảm đi rất nhiều. Dù vậy vẫn luôn phải kiểm chứng kết quả
  • Với góc nhìn của người nghiên cứu mô hình deep learning và các cấu trúc attention mới, ChatGPT cực kỳ hữu ích cho việc tìm bài báo và khám phá các ý tưởng liên quan
  • Với tư cách là người học toán như một sở thích, LLM cho tôi phản hồi về các thử nghiệm của mình hoặc dẫn tôi đến những lời giải sẵn có. Với toán học như một trò chơi, đây là một công cụ khá thú vị
  • Tôi nghiên cứu hình học đại số, và ngoài tìm tài liệu thì đến giờ vẫn chưa nhận được nhiều trợ giúp. Sự khác biệt giữa các model là khá lớn

• Hiện giờ bạn có thể trực tiếp thử Aristotle — https://aristotle.harmonic.fun/

  • Tôi cũng tò mò không biết họ có thử nghiệm AI trên bộ dữ liệu formal-conjectures của DeepMind hay không
  • Trong tài liệu ghi “uvx aristotlelib@latest aristotle” nhưng thực ra phải là “uvx --from aristotlelib@latest aristotle”
    Ngoài ra, liên kết đến trang cá nhân Stanford đang bị sai (cần bỏ www)
  • Chuyện này đủ thú vị để có một thread HN riêng. Nếu là CEO thì có lẽ nên tự đăng một bài giới thiệu (liên kết tham khảo)

• Kết quả lần này là một định lý về số nguyên, tức thuộc phạm vi mà hạ tầng Mathlib hỗ trợ rất tốt
  Các định nghĩa được dùng cũng không phức tạp, nên loại chứng minh này có xác suất thành công cao. Dù vậy đây vẫn là một thành tựu thực sự đáng kinh ngạc

• Đây là một ví dụ cho thấy tiềm năng của các cách tiếp cận AI chuyên biệt vượt ra ngoài LLM
  Bài báo về Aristotle có trên arXiv:2510.01346
  Không phải cứ dùng kiến trúc Transformer thì đều là LLM — nếu không được huấn luyện trên dữ liệu ngôn ngữ thì không thể gọi là LLM

  • Có lẽ sự nhầm lẫn xuất phát từ việc nhiều người dùng “LLM” thay cho “GenAI”
  • Bạn nói là “cách tiếp cận không phải LLM”, nhưng chẳng phải thực tế đã dùng ChatGPT sao?
  • Đúng vậy, trên thực tế có dùng ChatGPT
  • Đọc bài báo thì thấy cả ba giai đoạn đều có sự tham gia của LLM lớn dựa trên Transformer
    1. Trong Monte Carlo Graph Search, nó đảm nhiệm hàm chính sách/giá trị
    2. Hệ thống suy luận không chính thức dùng chain of thought
    3. AlphaGeometry cũng dùng mô hình ngôn ngữ neuro-symbolic
       Nói cách khác, mọi giai đoạn đều dựa trên LLM

• Có vẻ đến năm 2026, AI sẽ xử lý ngày càng nhiều bài toán chưa giải trong toán học
  Trường hợp lần này tuy chưa hoàn toàn tự động, nhưng cũng đã ở mức sau khi có phản hồi từ con người thì AI gần như tự giải được
  Theo tôi, tranh cãi kiểu “LLM chỉ là con vẹt xác suất” giờ đã kết thúc. Từ nay trọng tâm thật sự sẽ là làm sao đưa vào ứng dụng thực tế

  • Năm 2026 có lẽ sẽ chứng kiến bước tiến bùng nổ trong lĩnh vực toán học
  • Kết quả lần này nhiều khả năng là một bản remix từ các chứng minh tương tự đã có trong dữ liệu huấn luyện, nhưng chính năng lực remix đó cũng đã rất mạnh
  • Vẫn cần có kiểm chứng độc lập. Chỉ dựa vào tuyên bố của doanh nghiệp thì khó mà tin tưởng hoàn toàn