TIN NÓNG: Phiên bản tiêu dùng của Aristotle đã vượt qua Putnam, giải quyết và xác minh chính thức 10/12 bài toán trong @leanprover. Chúc mừng nhà toán học nghiệp dư @namrata_anand2, người đã sử dụng phiên bản tiêu dùng của Aristotle với một bản phát hành công khai sớm của các bài toán. Có vẻ như Aristotle đã giải quyết chúng một cách dễ dàng, tự động giải quyết 10/12 bài toán. Chúng tôi hiện đang xem xét các tệp và sẽ chia sẻ thêm chi tiết sau, nhưng có hai điều hữu ích cần lưu ý ngay bây giờ: ▪️ Đây có vẻ là những giải pháp chính thức hoàn toàn đầu tiên cho các bài toán Putnam 2025 được phát hành công khai. ▪️ Tất cả đều sử dụng giao diện ngôn ngữ tự nhiên mới được phát hành, trong đó Aristotle đã nhận câu hỏi bằng ngôn ngữ tự nhiên, sau đó tự động hình thức hóa nó thành một tuyên bố Lean4, và sau đó hoàn thành chứng minh, hoàn toàn tự động mà không có sự can thiệp của con người. Trong quá khứ, chúng tôi đã tập trung vào khả năng chứng minh định lý tiên tiến của Aristotle, nhưng giờ đây nó cũng đang trở nên khá khả năng trong việc tự động hình thức hóa. Chúng ta đang bước vào một bình minh mới cho AI và toán học. Từ từ... rồi tất cả cùng một lúc!