Tự động hóa với Aristotle bởi @HarmonicMath và kỹ thuật đảo ngược với @OpenAI GPT Codex CLI (thực tế là GPT-5.2 với xhigh và tất cả các đặc quyền thử nghiệm được kích hoạt). Khi làm một bài tập từ Đại số của Bourbaki về ma trận, tôi đã có gần 900 dòng mã Lean 4 được tài liệu hóa đầy đủ, bao gồm tất cả các chi tiết của chứng minh. Sau đó, tôi đã chuyển nó - sử dụng một thiết lập tác nhân được thiết kế phù hợp - đến Codex CLI để đảo ngược kỹ thuật tệp LaTeX tương ứng, tái tạo các bước chứng minh trực tiếp từ Lean, theo phong cách của các chứng minh có cấu trúc của Leslie Lamport. Đây chưa phải là chương trình Langlands, nhưng chúng ta cần loại toán học cấp trung gian này được tự động hóa. Và điều này đang diễn ra ngay bây giờ. Tôi chỉ cần xây dựng thiết lập tác nhân đúng, kết nối mọi thứ và thu thập văn bản từ Bourbaki (ngay cả phần đó cũng hoạt động tốt với @grok 4.1, điều này thật tuyệt cho việc xem trước LaTeX trực tiếp). Tôi sẽ hoàn thành tài liệu và đăng nó lên GitHub. Kiểm tra đồ thị phụ thuộc - Aristotle đã xử lý tất cả một cách tự động. Và chứng minh hoàn toàn tương tác. Chúng ta đang sống trong tương lai của khoa học ngay bây giờ!