Lean (trợ lý chứng minh)

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.

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 và Kevin Buzzard. 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ụ

Đâ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

 Trợ lý chứng minh
 Lý thuyết hình thái
 Kiểu phụ thuộc
 Coq
 Agda
 mimalloc

Tham khảo

Liên kết ngoài
 Lean Website
 Lean Community Website
 The Natural Number Game- An interactive tutorial to learn lean

Thể loại:Ngôn ngữ lập trình được tạo trong 2013
Thể loại:Trợ lý chứng minh
Thể loại:Ngôn ngữ phụ thuộc kiểu
Thể loại:Phần mềm tự do và mở mã nguồn
Thể loại:Phần mềm tự do của Microsoft
Thể loại:Phần mềm tự do được lập trình bằng C++
Thể loại:Ngôn ngữ lập trình của Microsoft
Thể loại:Ngôn ngữ hàm
Thể loại:Microsoft Research
Thể loại:Phần mềm sử dụng giấy phép Apache