Hỗ trợ AI đang dần trở thành chuyện thường ngày trên website Bài toán Erdős

• Trong quá trình giải Bài toán Erdős #367, các công cụ AI đóng vai trò then chốt, và đã xuất hiện một trường hợp cộng tác giữa nhà toán học con người với AI
• Wouter van Doorn đã đưa ra phản ví dụ do con người tạo ra cho phần thứ hai của bài toán, sau đó Gemini Deepthink tạo ra chứng minh đầy đủ cho đồng dư thức liên quan
• Terence Tao đã chuyển đổi chứng minh dựa trên lý thuyết số đại số p-adic của Gemini sang dạng đơn giản hơn để đăng tải, và sau đó nhắc đến khả năng hình thức hóa bằng Lean
• Boris Alexeev đã hoàn tất hình thức hóa bằng Lean với công cụ Aristotle của Harmonic, đồng thời tự kiểm chứng mệnh đề cuối cùng bằng tay để ngăn việc lạm dụng AI
• Chuỗi sự việc này cho thấy việc AI hỗ trợ trong nghiên cứu toán học đang dần trở thành một quy trình tiêu chuẩn

---

Trường hợp cộng tác AI trong Bài toán Erdős #367

• Ngày 20 tháng 11, Wouter van Doorn đã đưa ra phản ví dụ cho phần thứ hai của bài toán, và điều này phụ thuộc vào giả định rằng một đồng dư thức cụ thể là đúng
  • Ông đã đề nghị những người tham gia khác xác minh tính hợp lệ của đồng dư thức đó
• Vài giờ sau, Terence Tao đã đưa bài toán này cho Gemini Deepthink, và sau khoảng 10 phút đã nhận được chứng minh đầy đủ của đồng dư thức cùng xác nhận cho toàn bộ lập luận
  • Chứng minh của Gemini sử dụng lý thuyết số đại số p-adic, và Tao đã chuyển nó thành một chứng minh sơ cấp đơn giản hơn rồi đăng lên trang web
  • Tao cho biết chứng minh này có thể “vibe formalizing” trong Lean

Hình thức hóa và kiểm chứng bằng Lean

• Hai ngày sau, Boris Alexeev đã hoàn tất việc hình thức hóa bằng Lean bằng công cụ Aristotle của Harmonic
  • Để ngăn việc lạm dụng AI, mệnh đề cuối cùng được tự tay hình thức hóa trực tiếp
  • Toàn bộ quá trình mất khoảng 2~3 giờ, và kết quả đã được công bố trực tuyến
• Sau đó Tao đã dùng AI để tìm kiếm tài liệu, nhưng dù có một số nghiên cứu liên quan, ông không tìm thấy gì liên quan trực tiếp tới bài toán #367

Phản ứng và thảo luận trong cộng đồng

• Một số người dùng theo dõi với sự thích thú qua cập nhật của Tao về tình hình ứng dụng AI trong toán học học thuật
• Một người dùng khác đưa ra quan điểm phê phán đối với cách tiếp cận hình thức chủ nghĩa của Lean, cho rằng hiểu biết toán học là nén (compression), còn Lean thì phân rã nó thành các chi tiết mức thấp (decompression)
  • Tài liệu liên quan “Against Lean: Why Proof Assistants Formalize the Wrong Thing” lập luận rằng Lean và các trợ lý chứng minh tương tự đang nắm bắt sai bản chất của toán học
• Một người dùng khác nhắc đến vấn đề độ chính xác trong đối thoại với AI, đồng thời đánh giá rằng dù cần tinh chỉnh kỹ nhưng vẫn rất thú vị khi sử dụng

[GN⁺]

Ý kiến trên Hacker News

• Thật đáng kinh ngạc khi có thể đưa các bài báo ML thiên về toán cho trợ lý AI và nhận lại phần giải thích ngắn gọn hoặc mã giả
  Với tôi, người đã hơn 25 năm không hề dùng lại những gì học ở đại học, điều này thực sự giúp ích rất nhiều

  • Tôi tự hỏi làm sao để kiểm chứng xem phần giải thích đó có chính xác hay không. Các định nghĩa toán học có rất nhiều điểm cực kỳ tinh tế
  • Tôi nghĩ đây chính là điểm mà LLM tỏa sáng trong việc học tập
    Có thể đưa bài báo vào Claude, nhận phần tổng quan rồi tiếp tục đặt câu hỏi
    Ngay cả ở những lĩnh vực như sinh học mà tôi chưa từng học ở bậc cử nhân hay thạc sĩ, tôi vẫn có thể đào sâu như đang trò chuyện với một gia sư hiểu biết
  • Ký hiệu toán học có tính phụ thuộc ngữ cảnh rất cao, nên nếu nhờ LLM chuyển nó sang một ngôn ngữ ít ngữ cảnh như Lisp thì có thể nắm cấu trúc nhanh hơn nhiều

• Mong rằng các nhà nghiên cứu và doanh nghiệp sẽ đạt được nhiều cải thiện năng suất hơn trong nghiên cứu khoa học
  Ngay cả một trợ lý chưa hoàn hảo cũng đủ để tăng đòn bẩy rất nhiều

  • Có bản beta của ứng dụng formalization cho iOS mà Tao đã nhắc tới → Aristotle
    Nghe nói đây là startup do CEO của Robin Hood sáng lập

• “Vibe formalizing” tạo cảm giác như phần mở rộng hợp lý của “vibe engineering” và “vibe coding”
  Khi các mảnh ghép của bài toán không khớp với nhau, cách tiếp cận kiểu “Move 37 as a Service” kết hợp phương pháp phi hình thức với tính chặt chẽ toán học khá thú vị

  • Trước đây tôi từng bị mắc ở một đoạn khi đọc bài báo về polyhedral compilation, và ChatGPT đã dẫn dắt quá trình reasoning khá tốt
    Tất nhiên vẫn có chỗ sai, nhưng tôi có thể phản chiếu sự bối rối của mình vào cuộc đối thoại để đào sâu hiểu biết
    AI đặc biệt giỏi trong việc xác định điểm gây bối rối cho người dùng

• Tôi đã nghe câu chuyện về cách phát âm tên của nhà toán học Hungary Erdős
  Tiếng Hungary gần như đọc đúng theo mặt chữ, nhưng tên riêng thì có ngoại lệ
  Theo kiểu tiếng Anh, nó nghe đại khái như “airdish”

  • Ő đơn giản là âm œ(oe). Chữ -y trong tên người Hungary là dấu tích của đuôi -i từng biểu thị dòng dõi quý tộc
    Ví dụ: Görgey, Széchényi, Lánczos, v.v.
    Thứ tự tên của người Hungary giống tiếng Nhật, theo kiểu họ-tên (big endian). Ví dụ: “Erdős Pál”, “Neumann János”
  • Có một bài thơ đùa mà tôi thấy trên bảng tin khoa toán năm 1960 — đùa rằng một bài báo do Erdos viết đã bác bỏ định lý ‘hình tròn thì tròn’
  • Vì ý nghĩa của dấu phát âm khác nhau giữa các ngôn ngữ, tôi thấy việc giữ nguyên dấu kiểu Hungary trong câu tiếng Anh là hơi gượng gạo
  • Lúc đầu cách phát âm “airdish” nghe lạ thật, nhưng khi thử vòm hóa (palatalize) phần đuôi “os” thì lại thấy khá hợp lý
  • Có lẽ vì tôi không phải người Mỹ nên dường như chẳng ai bận tâm đến những vấn đề phát âm kiểu này

• Điều thú vị là trong phần bình luận có phản ứng mang xu hướng anti-Lean

  • Tôi không phải nhà toán học, nhưng tò mò không biết các tài liệu phản Lean đó có đáng tin không
    Không rõ đó chỉ là quảng bá cho một cách tiếp cận khác, hay là phản đối Lean về mặt triết học
  • Những nhân vật nổi tiếng như Tao vốn dễ thu hút sự chú ý của những người lập dị hoặc theo thuyết âm mưu

• Kết quả dùng AI trong toán học nghiên cứu của tôi là pha trộn cả tốt lẫn xấu
  Có lúc nó tự động hoàn thiện được các lập luận không tầm thường, nhưng ở một số mảng thì lại lạc đường hoàn toàn
  Tôi vẫn nghĩ hiện tại AI chỉ hữu ích như một công cụ hỗ trợ, chứ chưa thể thay thế nhà toán học

  • Tôi cũng có trải nghiệm tương tự. Tôi từng giao cho nó một bài toán tính hoán vị đơn giản trong một bài báo, nhưng còn mất thời gian hơn cả tự giải
    Trong lập trình cũng có lúc nó không bắt được lỗi vặt, nhưng với các tác vụ phức tạp thì lại giúp rất nhiều
    Cuối cùng thì những công cụ này vẫn còn rất xa mới thay thế được chuyên gia, và việc thổi phồng quá mức có thể làm hại lòng tin
    Như câu nói “nếu đã hứa mặt trăng thì phải đưa được mặt trăng”, mức kỳ vọng thực tế là điều quan trọng

• Tôi không thể tin rằng trong đời mình lại được sống tới thời kỳ kiểu Star Trek nơi có thể nói “máy tính, hãy phác họa chứng minh cho bài toán này”
  Ước gì “Beam me up Scotty” cũng làm được

  • Nhưng mỗi lần như vậy có thể lại chết mất, nên chắc cái đó hơi khó chấp nhận

• Tối nay khi đang lái xe, tôi đã trò chuyện với ChatGPT về cấu trúc chi tiết của trình lập lịch pipeline trong LLVM và GCC
  Nhờ vậy năng suất tăng lên đáng kể, và nó còn tự động sắp xếp lại các ghi chú về trình biên dịch mà tôi đang thử nghiệm
  Trước đây chuyện này là điều không thể tưởng tượng nổi

  • Theo kinh nghiệm của tôi, rất có thể LLM đã sai ở một số chi tiết
    Tất nhiên kết quả có thể khác nhau tùy người

• Nếu đặt tên AI là Erdos, có lẽ Erdos number của tất cả chúng ta sẽ là 1

  • Hoặc nghe như bản kế nhiệm của DR-DOS
  • Thực ra đã có một sản phẩm tên Erdos, là IDE tích hợp AI

• Tôi ấn tượng với việc ông ấy đã tận dụng tốt các công cụ frontier hiện có để tạo ra một môi trường nghiên cứu toán học mang tính cộng tác

  • May mắn là toán học là lĩnh vực mà sự sùng bái cá nhân hay cuộc đua độ nổi tiếng không quyết định tính đúng sai của kết quả
    Vì lý do đó, tôi vẫn nghĩ toán học là một trong số ít ngành học hiếm hoi còn tương đối miễn nhiễm với ảnh hưởng ngụy khoa học