Đến nội dung

Hình ảnh

Lean for the Curious Mathematician 2023

* * * * * 2 Bình chọn

  • Please log in to reply
Chưa có bài trả lời

#1
Nxb

Nxb

    Thiếu úy

  • ĐHV Toán học Hiện đại
  • 679 Bài viết

Sắp tới một hội nghị về ngôn ngữ lập trình Lean (một loại hỗ trợ chứng minh) sẽ diễn ra ở Đức. Hội nghị bao gồm hướng dẫn làm quen với Lean cũng như giới thiệu về các tiến bộ gần đây trong chứng minh định lý với sự hỗ trợ của máy tính và vai trò của nó đối với toán học trong tương lai. Chi tiết xem tại đây https://lftcm2023.github.io/

 

Liên quan đến Lean thì từ năm ngoái, Meta thông báo rằng họ đã đạt được một số tiến bộ trong giải quyết các bài toán ở cấp độ IMO https://ai.facebook....heorem-proving/ 

Mặt khác, theo như ở đây https://www.icms.org...Events/talk.pdf, Kevin Buzzard cho rằng ứng dụng của AI vào toán học sẽ dừng lại ở mức độ toán phổ thông hoặc những năm đầu đại học, tức là nó có khả năng giải quyết những bài toán mà con người biết chắc có lời giải. Không có bằng chứng nào hiện tại cho thấy AI có thể đóng góp những ý tưởng quan trọng vào toán học, chẳng hạn một lời giải cho giả thuyết BSD bằng AI là “hoàn toàn khoa học viễn tưởng”.






0 người đang xem chủ đề

0 thành viên, 0 khách, 0 thành viên ẩn danh