🚀 Aleph prover vừa chuyển sang CHẾ ĐỘ QUÁI VẬT 4 bài toán toán học chưa được giải quyết trong hơn 20 năm. Chứng minh chính thức trong Lean 4. Dưới 48 giờ. Tổng cộng dưới 5k đô la. ✅ Giả thuyết giới hạn đuôi nhị thức (Telgarsky, 2009) ✅ Xấp xỉ lưới cổng lượng tử (Greene & Damelin, 2015)* ✅ Erdős 124 ✅ Erdős 481 ✅ #1 trên bảng xếp hạng PutnamBench Thời đại toán học AI đã đến. Cảm ơn đặc biệt đến @BorisHanin và @ylecun vì đã giúp hiện thực hóa điều này 🙏 Và một lời khen lớn đến đội ngũ @LeanFRO — không có nền tảng tuyệt vời mà các bạn đã xây dựng, tất cả điều này sẽ không thể xảy ra. Aleph sẽ sớm có sẵn cho công chúng, hãy theo dõi nhé! *điều kiện dựa trên kết quả từ Sardari (2015), đang chờ formalization