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ờ!

Trong bài viết cộng đồng này, tôi muốn đưa ra các liên kết đến một số trò chơi và môi trường tương tác hấp dẫn (có sẵn miễn phí) giúp mọi người khám phá các khái niệm cao cấp trong cả lập trình và toán học. Nếu bạn biết bất kỳ nơi nào thú vị khác để ghé thăm, hãy đơn giản đăng bên dưới. Chúc bạn vui vẻ! Lean: Một bộ sưu tập các câu đố lập trình hấp dẫn giúp bạn học cách mà toán học được chứng minh và hình thức hóa. Bạn sẽ không bao giờ nhìn nhận sự khó khăn của 5*7=7*5 theo cách giống như trước đây nữa. NandGame: Bạn tự tạo ra bộ xử lý của riêng mình từ đầu (ngay cả NAND cũng được tạo ra từ mạch đơn giản hơn). Rất gây nghiện và cực kỳ thú vị! Quantum Flytrap: Đây là nơi bạn sẽ cuối cùng hiểu được các phép toán lượng tử. Màu sắc, vô hạn, hấp dẫn và rất sâu sắc về mặt toán học. Scratch: Học lập trình theo cách thú vị. Euclidea: Học cách thực hiện các cấu trúc với thước kẻ và compa. Nó từng là một phần của giáo dục ở trường nhưng giờ đây nó là một ứng dụng. Thú vị và rất thông tin. Planarity: Cố gắng tìm một nhúng đồ thị cho thấy rằng nó thực sự là phẳng. Golly: Người khám phá tự động tế bào tối thượng. Nếu bạn muốn đào sâu hơn: SageMath: Đây là một hệ thống đại số máy tính mạnh mẽ với cú pháp Python. Nó lý tưởng cho các khóa học và cú pháp của SageMath gần gũi hơn với diễn ngôn toán học thông thường. Tôi thích dạy các khóa học với SageMath. GeoGebra: Bạn có thể thực hiện chứng minh, tính toán và các applet tương tác. Đây là một cách thú vị để học nhiều khía cạnh khác nhau của toán học đại học. Wolfram Demonstration Projects: Một bộ sưu tập các applet toán học có thể giúp bạn hiểu các chủ đề rất tinh vi. Bạn không cần Mathematica để chạy nhưng bạn cần nó để thiết kế các applet của riêng mình. The Mechanics of Proof (bởi Heather Macbeth): Đây là một cuốn sách với một repo GitHub tương tác nơi bạn có thể học một cách toàn diện hơn về cấu trúc và cú pháp của Lean. An Illustrated Theory of Numbers (bởi Martin H. Weissman): Đây là một sách giáo khoa về lý thuyết số cơ bản với các ứng dụng. Và những ứng dụng này có sẵn từ trang web dưới dạng một bộ sưu tập các Jupyter Notebooks miễn phí dạy bạn các khái niệm chính. Graphical Linear Algebra: Theo cách minh họa và ở một mức độ nào đó là cách học tương tác các khái niệm sâu sắc trong đại số. HomotopyContinuation.jl: Đây là một cách học vô cùng đẹp và tương tác (với Julia) về một số ý tưởng phức tạp từ hình học đại số (các thành phần liên kết, phương pháp tiếp tục homotopy) và với các ứng dụng cho các hệ thống đại số rất đặc biệt đến từ các ứng dụng. Bạn có thể học Julia trên đường đi. Mathamaze: Đây là một trải nghiệm của Helena Verrill. Hình học đẹp, lát gạch, hoa văn. Thật tuyệt vời. Khó để giải thích: n: con đường của ninja: Nếu bạn nghĩ toán học là khó. Học sự kiên nhẫn theo cách khó khăn. Cảnh báo: rất gây nghiện HyperRogue: Bạn có thể học hình học hyperbolic trong một môi trường rogue-like.

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