Lean (trợ lý chứng minh)
From Wikipedia, the free encyclopedia
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.
Mẫu hình | Lập trình hàm, Lập trình mệnh lệnh |
---|---|
Nhà phát triển | Microsoft Research |
Xuất hiện lần đầu | 2013; 11 năm trước (2013) |
Phiên bản ổn định | |
Bản xem thử | |
Kiểm tra kiểu | tĩnh, mạnh, suy luận |
Ngôn ngữ thực thi | C++, Lean |
Hệ điều hành | Đa nền tảng |
Giấy phép | Apache License 2.0 |
Trang mạng | Ổn định: leanprover-community Xem trước: leanprover |
Ảnh hưởng từ | |
ML Coq Haskell |
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.