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!