Tôi xin trình bày một cách tự động hoàn chỉnh của một bài báo toán học gần đây (một lần nữa!) Barańczuk, Stefan. "Giảm số lượng phương trình xác định một tập con của không gian n trên một trường hữu hạn." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Tôi đã dành vài ngày cho dự án này. Đầu tiên, tôi đã chạy Aristotle bởi @HarmonicMath, mà trong khoảng 15 giờ đã hoàn toàn tự động hóa chứng minh. Sau đó, với sự giúp đỡ tuyệt vời của @PietroMonticone, tôi đã thiết lập một phiên bản bản thảo của chứng minh. Đây là một phiên bản mà tất cả các phần của tài liệu trong LaTeX trở nên tương tác và có thể được kiểm tra và nghiên cứu. Chúng ta có thể thấy các phụ thuộc trong chứng minh và nghiên cứu mối quan hệ của chúng. Trong giai đoạn xử lý hậu kỳ, tôi cũng đã sử dụng Grok Heavy và Codex CLI với GPT-5.2 ở chế độ xhigh để viết một phân tích từng dòng của chứng minh chính thức. Đây là một sự trợ giúp tuyệt vời cho những người không phải là lập trình viên Lean 4 chuyên nghiệp. Bạn thực sự có thể nắm bắt tất cả các bước của chứng minh. Tôi muốn tóm tắt ấn tượng của mình và những gì tôi đã học được từ trải nghiệm này. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei