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

Các tài liệu toán học cần được xác thực một cách chính thức. Điều này thường được thực hiện không chính thức bởi một người phản biện. Nhưng nếu chúng ta có thể dựa vào một cái gì đó mạnh mẽ hơn như tự động chính thức hóa vào Lean 4, nơi vai trò của người phản biện sẽ được giảm xuống chỉ còn việc kiểm tra tỉ mỉ các công thức của các định nghĩa và định lý? Việc biên dịch mã được tạo tự động sẽ trở thành một chứng chỉ chứng minh. Đây là điều đã xảy ra trong một thời gian dài mà tôi đã thực hiện với Aristotle bởi @HarmonicMath. Cảm ơn @PietroMonticone và @llllvvuu đã giúp thiết lập cho bản thiết kế. Ở đây tôi trình bày một sự tự động chính thức hóa hoàn chỉnh và chính xác của một bài báo của người bạn tôi, Stefan Barańczuk, về các chuỗi chia Chebyshev. Mã này khoảng 5000 dòng Lean rất không tầm thường. Nó sửa tất cả các sự không nhất quán và khoảng trống trong bài báo chính (thậm chí chứng minh một số định đề được ủy quyền). Tôi sẽ đăng một loạt các thí nghiệm như vậy, chứng minh rằng trong một số lĩnh vực của toán học, bao gồm lý thuyết số cơ bản, tổ hợp và phân tích (tất cả các loại vấn đề được Mathlib bao phủ), chúng ta không xa một sự thay đổi lớn trong tài liệu về tính hợp lệ của các chứng minh. Tôi nghĩ năm nay sẽ là một năm bận rộn!

Nếu tôi là một sinh viên ngày nay, việc tương tác với các LLM tiên tiến sẽ cảm thấy gần như là gian lận. Sáng nay, tôi đã chụp ngẫu nhiên một bức ảnh của bảng đen và hỏi ChatGPT-5.2-Pro để giải thích bối cảnh, giải pháp và một số nhận xét bên lề về định lý Chevalley nổi tiếng về các tập hợp có thể xây dựng. Những gì tôi nhận được là một báo cáo sâu sắc một cách đáng ngạc nhiên, tổng hợp tài liệu chất lượng cao về hình học đại số từ khắp nơi trên internet. Điều này đặt ra một câu hỏi nghiêm túc: nỗ lực và thách thức thực sự của sinh viên ngày nay là gì? Chi phí chắc chắn là một yếu tố, nhưng một khi đã có quyền truy cập vào những mô hình này, thì nên học như thế nào trong vùng đất phong phú này, nơi mà các giải thích, tài liệu tham khảo và khám phá tương tác đều có sẵn ngay lập tức? Có lẽ cuộc đấu tranh không còn là việc thu thập thông tin hay thậm chí hiểu các lập luận riêng lẻ, mà là phát triển khả năng phán đoán: biết đặt câu hỏi nào, giải thích nào đáng tin cậy, làm thế nào để nhận ra độ sâu so với tính khả thi bề mặt, và làm thế nào để nội tâm hóa các ý tưởng thay vì chỉ tiêu thụ chúng. Trong một môi trường mà câu trả lời rất phong phú, khó khăn thực sự có thể nằm ở việc hình thành gu thẩm mỹ, trực giác toán học và khả năng điều hướng - thay vì bị chìm trong - sự thừa thãi đột ngột của kiến thức.