AI
EasyProver giải 669/672 bài PutnamBench bằng Lean mà không cần huấn luyện thêm
EasyProver dùng một model frontier có sẵn kết hợp các agent đệ quy, không fine-tune, và chứng minh được 669/672 bài PutnamBench cùng toàn bộ 6 bài IMO 2026 đã được hình thức hóa. Nó cũng xử lý 597/600 điều kiện của NTP4VC và đủ 189 tác vụ VERINA. Nhóm tác giả ra mắt thêm Aegis, bộ 2.045 cặp chương trình Rust và Lean dựng bằng Aeneas để kiểm chứng code thực tế.
Vì sao đáng chú ý
Chứng minh hình thức đang chuyển từ bài toán thi sang kiểm chứng code Rust thật, mảng gần với kỹ sư phần mềm.
Nguồn
- arXiv arxiv.org · nguồn chính