Toán học bị ma ám

• Lean là ngôn ngữ lập trình được thiết kế để hình thức hóa toán học, cho phép các nhà toán học thao tác các định lý toán học như những đoạn mã
• Người dùng viết định lý, chứng minh, tiên đề dưới dạng mã, và quá trình chứng minh được thực hiện thông qua tập lệnh gọi là tactic
• Ngay cả khi chứng minh chưa được hoàn thành, vẫn có thể tạm dừng bằng sorry, nhưng đây là một dạng chứng minh giả giống với any trong TypeScript
• Nếu thêm sai tiên đề (ví dụ: 2 = 3), sẽ phát sinh nguy cơ mâu thuẫn logic và khả năng chứng minh mọi khẳng định
• Lean chỉ suy ra kết luận dựa trên các tiên đề đã chọn và hệ thống chứng minh về mặt logic, nên việc giữ gìn tính đúng đắn toán học có ý nghĩa quan trọng

---

Lean: Ngôn ngữ làm việc với toán học như mã

• Lean là ngôn ngữ lập trình chuyên dùng để viết các phát biểu toán học được hình thức hóa
• Các nhà toán học dùng Lean để biểu diễn toán học bằng mã và cấu trúc hóa định lý, chứng minh của nhau nhằm hợp tác và chia sẻ
• Họ đưa ra một tương lai trong đó một lượng lớn tri thức toán học của nhân loại có thể được biểu diễn dưới dạng mã, từ đó kiểm chứng tự động và kết hợp một cách cơ giới

Những bước đầu trong chứng minh với Lean

• Trong Lean có thể viết một khai báo định lý đơn giản như theorem two_eq_two : 2 = 2 := by sorry
• Khi chứng minh chưa hoàn thiện, ta chèn sorry, nhưng đây chỉ là mẹo tạm thời chứ không phải chứng minh thật sự
  • sorry sẽ qua được kiểm tra chứng minh của Lean, nhưng về logic thì không đáng tin cậy
• Để có chứng minh đầy đủ, cần dùng tactic như rfl (reflexivity) để chứng minh các đẳng thức hiển nhiên như 2 = 2
• Những nội dung đã chứng minh có thể được tái sử dụng trong các định lý khác bằng exact và các lệnh tương tự, nhấn mạnh tính mô-đun

Tiên đề và mâu thuẫn: Khi toán học bị ma ám

• Nếu thêm tiên đề như axiom math_is_haunted : 2 = 3, Lean sẽ xem tiên đề đó là đúng
• Tiên đề này có thể được dùng trong các bước chứng minh sau đó, và thậm chí có thể chứng minh các kết luận toán học vô lý (ví dụ: 2 + 2 = 6)
• Việc sử dụng tactic rewrite cho phép thay thế 2 bằng 3, rồi kết thúc quy trình chứng minh đẳng thức bằng rfl
• Nếu tiên đề sai gây ra mâu thuẫn, Lean cũng rơi vào trạng thái mọi mệnh đề đều chứng minh được (sụp đổ logic)
• Trên thực tế, vào đầu thế kỷ 20, các mâu thuẫn trong hệ tiên đề như nghịch lý Russell đã dẫn tới những suy tư nền tảng căn bản về toán học
• Như vậy, Lean cho thấy việc chọn tiên đề là nhân tố quyết định để duy trì tính hợp lệ của hệ thống logic

Lean với tư cách trình kiểm tra chứng minh

• Nếu các tiên đề được chọn đúng và Lean nhất quán về logic, nó cung cấp các kết luận có độ tin cậy về mặt lý thuyết
• Từ những đẳng thức đơn giản đến các định lý cực kỳ phức tạp (ví dụ: Fermat’s Last Theorem), tất cả đều được kiểm chứng theo cùng một nguyên lý
• Các định lý lớn được hoàn thiện như một cấu trúc cây, tích lũy qua chứng minh lặp lại các cấu trúc con và định lý cấp thấp
• Ví dụ, có một dự án quy mô lớn đang hình thức hóa Fermat's Last Theorem trong Lean; vào giai đoạn cuối sẽ có một hệ thống chứng minh chính thức hoàn chỉnh không còn dùng sorry

Niềm vui khi học Lean

• Chứng minh với Lean là sự kết hợp sáng tạo giữa lập trình và toán học
• Bắt đầu từ việc chứng minh các mệnh đề đơn giản, rồi dần dần xây dựng chặt chẽ những toán học sâu và phức tạp trở thành một niềm vui quan trọng
• Các tài liệu hướng dẫn chính thức và cộng đồng (ví dụ: Natural Numbers Game, Mathematics in Lean, v.v.) rất phù hợp cho người mới bắt đầu
• Khi dùng Lean, bạn trực tiếp hình thức hóa logic và có thể khám phá lại vẻ đẹp của ý tưởng tinh tế cùng lập luận
• Kết luận rằng, ngay cả khi không có lý do rõ ràng, với một số nhóm người, Lean mang lại một niềm thích thú đặc biệt