Astra và Claude giúp giải quyết bài toán xếp 11 hình vuông trong Lean

Một nhóm nhà nghiên cứu toán học đã dùng công cụ chứng minh định lý tự động để xác thực hình thức tính tối ưu của một bài toán hình học lâu năm. ManassehA06 dẫn dắt nỗ lực dựng nên một hệ thống chính thức hóa Lean trong vài ngày, sử dụng các AI model là Astra và Claude để đưa ra một chứng minh chặt chẽ về cách xếp tối ưu 11 hình vuông. Dự án có các đóng góp quan trọng từ Ojoshe, Kleddamag, Wand_125, Guzhou0806 và Ctjlewis. Bản chứng minh hoàn thiện dựa trên một cận dưới vững chắc do Kleddamag phát triển, kế thừa công trình trước đó của Wand_125 và Ojoshe. Quá trình cải tiến toán học này đã vượt qua cận dưới trước đây do Stromquist23881 thiết lập vào năm 2003, qua đó hoàn tất việc giải quyết dứt điểm bài toán xếp hình kéo dài.