Tôi không thể tin rằng con người viết mã Lean bằng tay. Và những thứ đã được chính thức hóa trong đó trước khi có LLMs. Việc chính thức hóa bất cứ điều gì trong Lean cảm thấy thú vị như việc lột da của bạn bằng một cái dao gọt khoai tây và thú vị như việc xem sơn khô.

Đừng nói với tôi về "niềm vui của trò chơi" / "nó rất tương tác" hay bất cứ điều gì. Có những trò chơi có mọi thứ để xem, cũng giống như có ra*e ở khắp mọi nơi, và tôi biết sự khác biệt.

@notmoeezm "Tôi thậm chí không quan tâm nếu máy móc xác minh chứng cứ" nguồn: người điều chỉnh thuật toán tìm kiếm trên không gian chứng cứ vì vui, sử dụng Lean😞