có vẻ như Lean đang phổ biến hôm nay, vì vậy đây là một bài viết nhỏ về cách/ lý do nó hoạt động và cách triển khai một phiên bản mini của nó trong Julia

bạn thực sự không cần phải biết Julia cho điều này vì nó rất đơn giản! (và bạn _chắc chắn_ không cần phải biết Lean)

dù sao đi nữa, đây là bài đăng

nếu bạn là người thích xem livestream:

@outputlayer rosé pine dawn (không in nghiêng), phông chữ là berkeley mono từ @usgraphics không thể bắt chước.

@frang_u99393 ồ vâng, các kiểu phụ thuộc hoàn toàn xuất hiện ở đây, thì Lean sẽ là một tác dụng phụ dễ dàng của hệ thống kiểu với một số điểm cộng bổ sung là bạn thực sự có thể viết phần mềm trong Julia.

@frang_u99393 "Lean" như một đại diện cho "các hệ thống chứng minh định lý tương tác giống Lean"