Lean (trợ lý chứng minh)

Bách khoa toàn thư mở Wikipedia
Lean
Mẫu hìnhLập trình hàm, Lập trình mệnh lệnh
Nhà phát triểnMicrosoft Research
Xuất hiện lần đầu2013; 11 năm trước (2013)
Phiên bản ổn định
3.48.0 / 17 tháng 9 năm 2022; 18 tháng trước (2022-09-17)
Bản xem thử
4.0.0-m5 / 7 tháng 8 năm 2022; 20 tháng trước (2022-08-07)
Kiểm tra kiểutĩnh, mạnh, suy luận
Ngôn ngữ thực thiC++, Lean
Hệ điều hànhĐa nền tảng
Giấy phépApache License 2.0
Trang mạngỔn định: leanprover-community.github.io
Xem trước: leanprover.github.io
Ảnh hưởng từ
ML
Coq
Haskell

Lean là phần mềm chứng minh định lý và ngôn ngữ lập trình. Ngôn ngữ này được viết dựa trên tích phân của các phép xây dựng cùng tự suy kiểu.

Dự án Lean là dự án mã nguồn mở nằm trên GitHub. Dự án khởi động bởi Leonardo de Moura tại Microsoft Research vào năm 2013.[1]

Lean có thể biên dịch về JavaScript và chạy trong trình duyệt web. Ngoài ra nó còn có hỗ trợ cho ký tự Unicode. (Các ký tự còn có thể đánh tương tự như LaTeX, ví dụ như dùng "\times" cho "×".) Lean còn có hỗ trợ cho meta-programming.

Lean đã thu hút được sự chú ý từ các nhà toán học như Thomas Hales[2] và Kevin Buzzard.[3] Hales đang sử dụng nó trong dự án của ông, Formal Abstracts. Buzzard sử dụng cho Xena project. Một trong những mục tiêu của dự án Xena là viết lại mọi định lý và chứng minh trong chương trình toán học của trường đại học Imperial College London bằng Lean.

Các ví dụ[sửa | sửa mã nguồn]

Đây là cách các số tự nhiên được định nghĩa trong Lean. 

inductive nat: Type
| zero: nat
| succ: nat → nat

Định nghĩa phép cộng cho các sự tự nhiên trong Lean. 

definition add: nat → nat → nat
| n zero     := n
| n (succ m) := succ(add n m)

Một bài chứng minh trong Lean. 

theorem and_swap: p ∧ q → q ∧ p:=
    assume h1: p ∧ q,
    ⟨h1.right, h1.left⟩

Bài chứng minh tương tự có thể viết lại như sau. 

theorem and_swap (p q: Prop) : p ∧ q → q ∧ p:=
begin
    assume h: (p ∧ q), -- assume p ∧ q is true
    cases h, -- extract the individual propositions from the conjunction
    split, -- split the goal conjunction into two cases: prove p and prove q separately
    repeat { assumption }
end

Xem thêm[sửa | sửa mã nguồn]

Tham khảo[sửa | sửa mã nguồn]

  1. ^ “Lean Prover About Page”.
  2. ^ Hales, Thomas (ngày 18 tháng 9 năm 2018). “A Review of the Lean Theorem Prover”. Truy cập ngày 6 tháng 10 năm 2020.
  3. ^ Buzzard, Kevin. “The Future of Mathematics?” (PDF). Truy cập ngày 6 tháng 10 năm 2020.

Liên kết ngoài[sửa | sửa mã nguồn]

Bản mẫu:Microsoft FOSS Bản mẫu:Microsoft development tools

Lấy từ “https://vi.wikipedia.org/w/index.php?title=Lean_(trợ_lý_chứng_minh)&oldid=69488483”