1 bình luận

 
Các ý kiến trên Hacker News
  • Tách khỏi thành quả hay bản thân chứng minh, điều thú vị là ngay cả với các mô hình mới nhất, một phần đáng kể của prompt thực chất vẫn được dùng để chỉ thị mô hình thực sự giải bài toán
    Chẳng hạn những cụm như “từ chối báo cáo trạng thái, sự lạc quan mơ hồ, và các tuyên bố rằng mệnh đề tương thích toàn cục chưa được chứng minh là ‘thường lệ’”, và phần nhồi cho mô hình khá nhiều chiến lược cũng rất đáng chú ý
    Những chiến lược như vậy rốt cuộc khiến ta có cảm giác rằng mô hình phải tự suy luận; không phải tôi muốn hạ thấp kết quả, mà nó gợi nhớ đến cách chuỗi suy nghĩ ban đầu khi prompt GPT-4 bằng câu “hãy nghĩ từng bước”

    • Tôi nghĩ điều này liên quan nhiều đến kiểu hậu huấn luyện mà các mô hình thường nhận được
      Chúng được thiết kế để trả lời các câu hỏi cơ bản bằng những bản tóm tắt ngắn gọn, thẳng vào vấn đề, nên dù có khả năng suy luận sâu, nếu không có prompt thì chúng không nghiêng về hướng đó
      Mô hình ngôn ngữ lớn năm 2026 rất có năng lực nhưng cũng giống một kiểu ảo thuật trong phòng khách; không phải có ý thức, mà gần với một cỗ máy lăn xuống dốc khi ta thiết lập ngữ cảnh cho nó
      Nếu có đầu vào đúng, nó có thể đi tới những câu trả lời thực sự mới, nhưng ở chỗ không có ý chí và phụ thuộc vào sự dẫn dắt của con người, nó vừa kỳ diệu vừa là máy móc
    • Mô hình ngôn ngữ lớn có suy luận cơ bản và khả năng ghi nhớ khổng lồ
      Kết hợp suy luận cơ bản đó với tìm kiếm đã được tỉa nhánh và lượng tính toán cực lớn thì có thể chứng minh được nhiều thứ, nhưng ký ức về việc con người từng thất bại lại cắt bỏ trước các khả năng
      Vì vậy cần nỗ lực thuyết phục mô hình đừng tỉa nhánh quá sớm dựa trên các thất bại trước đây của con người
    • Tôi đã thấy đúng hiện tượng tương tự khi hỏi về P=NP, nên khá buồn cười
      Các mô hình công khai từ chối thử vì nói rằng quá khó, và phải đấu tranh khá nhiều mới khiến chúng đề xuất dù chỉ là một hướng tiếp cận có triển vọng
    • Có lẽ cũng cần một mô hình được tinh chỉnh riêng cho nghiên cứu toán học, kiểu như “gpt-5.3-codex”
      Tôi bắt đầu mong chờ “gpt-5.6-mathx”
    • Tôi cũng nhìn nhận như vậy, và prompt đầy các metaheuristic
      Nó làm tôi nhớ đến thời vài năm trước khi người ta nói prompt engineering là một kỹ năng
      Nếu đoán thì lý do mô hình không tự làm được việc này là vì trong đa số bài toán, phần lớn lời khuyên kiểu này là lời khuyên tệ
      Trong tối ưu hóa tìm kiếm, thường có sự đánh đổi giữa thời gian và chất lượng; tìm kiếm rất rộng sẽ trả về kết quả rất tệ trong thời gian dài, còn tìm kiếm thiên về chiều sâu kèm heuristic có xu hướng nhanh chóng cho kết quả khá tốt
      Mô hình có lẽ sẽ tự nhiên cố tìm điểm trung gian tốt nhất trong đa số trường hợp, nhưng với những bài toán cực khó mà các nỗ lực vừa phải là chưa đủ, cần một tìm kiếm rộng hơn rất nhiều và không bị giới hạn thời gian
      Phần lớn prompt cũng có vẻ hướng tới việc mở rộng tìm kiếm, ngăn hội tụ sớm và loại bỏ áp lực thời gian
  • Nếu tóm lại khá chắc chắn, tiêu chí cho những việc dễ tự động hóa bằng AI agent là: mức độ có thể dễ dàng chỉ rõ và kiểm chứng tính đúng đắn của lời giải, mức độ có thể hiện thực hóa lời giải ứng viên mới bằng văn bản, và mức độ tồn tại nghiên cứu trước đó trên mạng
    Về cơ bản, điều này tương ứng với kỹ nghệ phần mềm và toán học
    Tôi nghĩ một phần khá lớn sự thổi phồng về AI đến từ việc công việc của chính những người thiết kế AI lại là nghề dễ được AI tự động hóa nhất
    Họ nghĩ “nếu công việc của mình được AI cải thiện nhiều như vậy thì mọi nghề khác cũng sẽ thế”, nhưng trớ trêu là thực tế gần như ngược lại, và các dự đoán về sự biến mất lao động trên diện rộng cũng vậy

    • Một góc nhìn thú vị, nhưng tôi nghĩ 2 điểm trong đó hơi bị phóng đại
      Tôi cho rằng phần lớn phần mềm không giống việc giải một bài toán hay một tập hợp bài toán toán học
      Các bài toán thuật toán có thể gần với điều này hơn, vì đó là một miền hẹp đã có sẵn oracle để kiểm chứng đáp án đúng hay sai
      Trong phần lớn phần mềm, hàm đúng đắn là người dùng dùng nó bao nhiêu và muốn trả tiền đến mức nào, mà đây là một vấn đề khá mơ hồ
      Vì chi phí sao chép phần mềm gần như bằng 0, các hệ thống cũng có xu hướng trở nên độc đáo và phân kỳ thay vì trở nên giống hệt nhau hay hội tụ về hệ thống khác
      Phần nghiên cứu trước đó cũng thú vị
      Ít nhất nếu xét toàn bộ ứng dụng, phần lớn vấn đề và đánh đổi mà phần mềm phi tầm thường ở quy mô có ý nghĩa chứa đựng thực ra không có nghiên cứu trước đó
      Nếu là dự án làm ứng dụng danh sách việc cần làm hay mạng xã hội thì có nhiều tiền lệ đủ để hệ thống mô hình ngôn ngữ lớn tạo ra, nhưng đa số ứng dụng có lẽ không như vậy
    • Hãy giả sử AI chỉ giỏi phần mềm và toán học
      Nếu nhờ AI mà có thể tạo nhiều phần mềm tốt với chi phí rẻ, thì chính phần mềm đó có thể tự động hóa nhiều công việc
      Vì vậy AI không nhất thiết phải trực tiếp lấy đi việc làm; phần mềm do AI viết có thể làm điều đó
      Đặc biệt nếu điều đó cũng trở nên khả thi với phần mềm cho robot thì càng đúng
    • Bạn có thể giải thích câu “thực tế thì ngược lại, và các dự đoán về sự biến mất lao động trên diện rộng cũng vậy” ở đây nghĩa là gì không?
      Một nhóm công việc có thể kiểm chứng được, tức lập trình, toán học, v.v., có vẻ rõ ràng là AI sẽ trở nên giỏi
      Một nhóm lớn khác như pháp lý, kế toán, phân tích tài chính, tôi không thấy lý do gì khiến AI không thể đạt mức siêu nhân, chỉ là có vẻ cần thêm việc đưa chuyên môn lĩnh vực vào harness và phần mềm
      Về dài hạn, bạn có cho rằng có những khía cạnh của lao động tri thức mà AI sẽ không giỏi không?
    • Nhiều vị trí cổ cồn trắng có thể kiểm chứng được
      Nếu tạo ra robot, các công việc trong thế giới thực cũng đột nhiên trở nên có thể kiểm chứng
    • Theo Dwarkesh, tính lặp lại trong huấn luyện cũng quan trọng
  • Khác với bài toán khoảng cách đơn vị, điều ấn tượng ở đây không phải là phản ví dụ mà là chứng minh
    Tuy nhiên chứng minh cực kỳ súc tích, trông như đã tận dụng một mẹo thông minh mà mọi chuyên gia đều bỏ lỡ
    Không phải tôi muốn hạ thấp kết quả đáng kinh ngạc này hay dời cột mốc, nhưng có vẻ thành tựu duy nhất mà AI hiện vẫn chưa làm được trong toán học là một chứng minh tự chủ kiểu “xây dựng lý thuyết” cho một giả thuyết mở
    Tức là một chứng minh phải tạo ra một lý thuyết mới thực chất, đủ để triển khai ít nhất hơn 30 trang nhằm phá một bài toán mở

    • Thật sự súc tích, và đúng như đã nói, đọc lên giống như nó tận dụng các tính chất đã được phát hiện và kết hợp chúng theo một cách mới
      Tôi rất thích văn phong này
      Nó đọc như các bài báo ngày xưa, kiểu định lý và chứng minh cứ thế được triển khai thẳng đúng như đã nói
    • Gần đây Grant Sanderson trong podcast của Dwarkesh đã phân biệt giữa nhà toán học tạo ra ngữ pháp và nhà toán học thao tác ngữ pháp đó
      Ở một số ngữ cảnh có thể gọi đó là ontology, và tôi khá thích cách phân biệt này
      Có vẻ chúng ta hiện đang ở giai đoạn thao tác ngữ pháp
      Việc tạo ra một ontology hữu ích thì vẫn còn có vẻ hơi xa
      Không phải tôi phàn nàn về kết quả tuyệt vời này, mà là đang nghĩ xem cột mốc tiếp theo sẽ được đặt ở đâu
    • Có lý do gì để nói “tuy nhiên” không?
      Theo cách hiểu của tôi, nó thật sự đã tìm ra một lời giải mới, và đó là một lời giải thanh nhã nhưng trước đây bị bỏ lỡ
      Tôi nghĩ đây chính xác là kiểu kết quả mà một nhà toán học con người khao khát
    • Cho vui, tôi hỏi ChatGPT 5.5 về tầm quan trọng của bài toán này và khả năng 5.6 giải được bằng một lời giải dài ba trang, thì nó trả lời gần như bằng 0
      Tôi cũng cho nó tìm kiếm trên Internet, nhưng nó vẫn cực kỳ hoài nghi
    • Tôi tò mò liệu mỗi lần có chạy các phiên song song không
      Kiểu một phiên thử chứng minh, một phiên tìm phản ví dụ
  • Công bố: https://x.com/eknight/status/2075643450196971805
    Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...

    • “Hãy dành ít nhất 8 giờ trước khi nghĩ đến việc trả lời hoặc bỏ cuộc”
      Harness của mô hình hiện nay có khái niệm thời gian đã dùng không?
      Thỉnh thoảng tôi thấy mô hình nhận ra và giết các tiến trình con nếu chúng chạy quá lâu hoặc bị treo, nhưng tôi chưa từng thấy nó tự bấm giờ
    • “Mất chưa đến 1 giờ một chút”
      Dù vậy tôi vẫn tò mò thiên kiến kẻ sống sót ở mức nào
      Có bao nhiêu bài toán khác đã thất bại?
      Bài này có từng được thử giải bằng prompt khác rồi thất bại không?
      Dù sao vẫn cực kỳ ấn tượng
  • Việc prompt được công khai thật sự rất tuyệt
    Tôi tò mò mỗi khi một frontier model mới ra mắt thì có bao nhiêu bài toán chưa giải được đem ra thử
    Họ có thử tất cả các bài toán trong mỗi lần phát hành không?
    Tỷ lệ giải thành công là bao nhiêu?
    Trong giới toán học có tiểu cộng đồng nào điều phối các nỗ lực như vậy không?
    Còn bao nhiêu cơ hội chưa được khai thác?

    • Việc toàn bộ đầu ra không được công khai thì hơi thú vị
      Một phê bình phổ biến về văn bản toán học là kết quả trông như được “lôi ra từ chiếc mũ”
      Chỉ viết chứng minh cuối cùng đã được trau chuốt, còn mọi thứ dùng để phát triển nó thì bị giấu đi
      Thật mỉa mai là khi mô hình ngôn ngữ lớn viết chứng minh, tập quán đó vẫn tiếp diễn
    • Prompt đã được công khai, nhưng chi phí để có được kết quả thì không
    • Tôi gần như chắc chắn rằng đã có hàng triệu đô la chi phí suy luận được đổ vào Giả thuyết Riemann
      Khi mô hình mạnh hơn, số tiền lớn hơn nữa sẽ được rót vào
      Hãy tưởng tượng một công ty trả “chỉ 1 tỷ đô la” và được ghi nhận là đã giải được bài toán mở khó nhất, nổi tiếng nhất trong lịch sử toán học
      Cũng có thể tưởng tượng các tiêu đề báo chí trên toàn thế giới
      Như người ta thường nói, Giả thuyết Riemann là cách khó nhất để kiếm một triệu đô la
  • Nếu mọi kiểm chứng đều thông qua, đây là một cột mốc khổng lồ
    AI giờ đây đã dùng một mô hình có sẵn để giải một trong những bài toán mở nổi tiếng nhất của lý thuyết đồ thị trong 1 giờ
    Ở thời điểm này, có lẽ nó đã là nhà toán học giỏi hơn phần lớn con người
    Giống như thời điểm phần mềm cờ vua bắt đầu thắng tất cả mọi người trừ các đại kiện tướng
    Giờ còn lại gì nữa?
    Đề xuất và xây dựng các lý thuyết và khung hoàn toàn mới?
    Sau đó là vượt hơn bất kỳ con người nào?
    Rồi sau đó là các kết quả toán học ngoài hành tinh mà chúng ta khó hiểu nổi?

    • Khó mà không thấy hư vô
      Về trí tuệ, tôi là một người rất trung bình, thậm chí có thể dưới trung bình
      Nếu tôi biết rằng bất cứ điều gì mình có thể làm thì mô hình ngôn ngữ lớn đều có thể làm tốt hơn, giá trị hay lý do tồn tại của tôi là gì?
      Giá trị của tôi trên thị trường lao động, cũng như với tư cách con người, là gì?
    • Có lẽ điều còn lại là con người đề xuất các giả thuyết mới, còn máy móc điền phần chứng minh
      Nhưng tôi không biết liệu có đủ nhiều giả thuyết thú vị để tạo ra một sự nghiệp mới hay không
    • Bạn nói những điều đó như thể chúng là các bước tiếp theo rất gần, nhưng thực tế có thể không diễn ra như vậy
      Chẳng hạn, trong vài năm qua AI không đạt được tiến bộ nào trong việc vượt qua chuyên gia ở nghệ thuật hay viết lách
      Khả năng làm theo prompt đã tốt hơn nhiều, giờ cũng vẽ được tay và chữ, nhưng cảm quan nghệ thuật thì hoàn toàn đình trệ
  • Tôi có cảm xúc lẫn lộn khi thấy những công bố như thế này
    Một mặt, có tiềm năng vô hạn trong những gì chúng ta có thể khám phá khi prompt AI giải được các bài toán lâu đời
    Mặt khác, có một điều gì đó về mặt thẩm mỹ bị mất đi vì đó không phải là chuyện con người vật lộn hoặc giải ra bằng một trực giác mới
    Nếu một prompt AI chạy trong trung tâm dữ liệu suốt 2 tuần rồi in ra p=np, tôi nghĩ sẽ cảm thấy hơi trống rỗng

    • Mọi thế hệ đều từng cảm thấy một phiên bản nào đó của cảm giác này
      “Bàn phím không có linh hồn. Chữ viết tay mang tính cá nhân và độc nhất như dấu vân tay.” — Joyce Carol Oates nói về máy đánh chữ
      “Phát minh này của ông sẽ sinh ra sự quên lãng trong tâm hồn người học. Vì họ sẽ không dùng trí nhớ, mà dựa vào các ký tự bên ngoài và sẽ không tự mình nhớ lại. Thứ ông phát minh không phải là thuốc giúp trí nhớ, mà là thuốc giúp gợi nhớ; ông trao cho học trò không phải chân lý, mà chỉ vẻ ngoài của chân lý.” — Socrates nói về chữ viết
    • Tôi đồng cảm với cảm giác đó, nhưng ngược lại, những con người đọc đầu ra ấy sẽ nhận được một boost cảm hứng khá lớn
      Câu trả lời mới thường sinh ra câu hỏi mới
  • ChatGPT 5.6 Sol Pro cho rằng chứng minh này là hợp lý
    Thường thì nó rất giỏi trong việc đánh giá một chứng minh có đúng hay không và sai ở đâu, và một người bạn là nhà nghiên cứu toán học hàng đầu cũng đã kiểm tra giúp: https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea...
    Cá nhân tôi thì càng tin hơn rằng chuyện này là thật

    • Tất nhiên là nó sẽ tin chứng minh đó hợp lý rồi, vì chính nó viết mà
      Muốn kiểm chứng đầu ra của mô hình ngôn ngữ lớn thì phải dùng một mô hình ngôn ngữ lớn khác
  • “GPT-5.6 Sol Ultra tạo ra chứng minh cho giả thuyết phủ kép chu trình”
    Đây là một tiêu đề bài viết rất dễ gây hiểu lầm
    Tiêu đề nên là “Những người vô danh dùng GPT-5.6 để tạo ra một chứng minh chưa được kiểm chứng cho giả thuyết CDC”
    Dù vậy, tôi đoán những gì đến từ ngành AI sẽ là lời quảng cáo

  • Tôi thích việc chứng minh này ngắn gọn như vậy
    Tôi từng đạt được một số tiến triển trong vài bài toán mở của tổ hợp học, và chứng minh mở rộng ranh giới thêm một bước dài tới 45 trang

    • Hồi trung học tôi từng làm nghiên cứu toán học, và chứng minh cuối cùng quy về hàng chục trường hợp bất đẳng thức đa thức xấu xí
      Giờ tôi không tìm được PDF, nhưng bài báo cuối cùng khoảng 70 trang, trong đó có vài trang là các biểu thức đa thức đã khai triển chiếm kín cả trang
      Phần văn xuôi thực sự có lẽ chỉ khoảng 5 trang
      Đó rõ ràng là chứng minh kém thanh lịch nhất trong tất cả những chứng minh tôi từng thấy
      Tôi thật sự biết ơn vì đã có cơ hội nghiên cứu sớm và được nhúng chân vào lĩnh vực này, nhưng nhìn lại bài báo đó thì thấy ngượng