Kiểm chứng chứng minh định lý do AI tạo ra: Lean 4 và quy trình tái dựng
Một câu trả lời toán học nghe hợp lý chưa đủ để xác nhận chứng minh của AI. Lean 4 giúp kiểm tra mệnh đề hình thức và proof term, nhưng người dùng vẫn phải đối chiếu đề bài, giả định, phiên bản, thư viện và các tiên đề mà dự án đã dùng.