[Hacker News] 'Why not just use Lean?'
Nguồn: Lawrence C. Paulson Tóm tắt Nhà khoa học máy tính Lawrence C. Paulson viết về câu hỏi thường gặp khi đề xuất hình thức hóa toán học ngày nay: “Tại sao không dùng Lean?” Tác giả, người đã làm việc trong lĩnh vực proof assistant từ những ngày đầu, bày tỏ sự phê phán nhẹ nhàng về “văn hóa bầy đàn” xung quanh Lean, đồng thời nhắc nhở về lịch sử dài của lĩnh vực hình thức hóa toán học....