# LeanScreen: Công cụ kiểm chứng độ chính xác cho các mệnh đề Lean 4

- Nguồn: Hacker News Nổi bật (buzzing.cc bản dịch tiếng Trung)
- Thời gian phát hành: 2026-08-12 02:52 (giờ Việt Nam)
- Điểm AI: 34/100
- Link AIHOT.vn: https://aihot.vn/items/4552c772b2c19f5a
- Nguồn dữ liệu AI HOT: https://aihot.news/items/cmsp3o23e04vmrortsnb45nga
- Link gốc: https://www.millenniumresearch.ai/leanscreen.html

## Tóm tắt AI

LeanScreen là công cụ hỗ trợ kiểm tra độ trung thực của các mệnh đề Lean 4, giúp phát hiện các lỗi logic dù mã nguồn đã biên dịch thành công. Công cụ này hỗ trợ cả dòng lệnh và giao thức MCP, tập trung vào việc sàng lọc thay vì chứng thực toán học.

## Thân bài

Một bộ lọc độ trung thực (faithfulness screen) cho Lean 4.

pip install leanscreen

Trình biên dịch không phản đối, nhưng leanscreen thì có.

leanscreen check Demo.lean exists_perfect_number: BỊ TỪ CHỐI flags=deterministic-vacuous:reflexive-goal even_add_even: không tìm thấy lỗi

Định lý đầu tiên biên dịch thành công. Docstring của nó hứa hẹn về một số hoàn hảo; nhưng phát biểu của nó lại là ∃ n: ℕ, n = n.

### NHANH

Kiểm tra lỗi (lints), kiểm tra tính rỗng (vacuity checks), và đối chiếu với mathlib của bạn. Miễn phí, chạy cục bộ, ~0,1 giây.

### SÂU

Hai giám khảo độc lập và một công cụ dò tìm phản ví dụ. Hãy chạy nó trước khi phát hành bất cứ thứ gì.

### ĐƯỢC HIỆU CHUẨN

Được đo lường dựa trên 886 đánh giá từ con người. Một kết quả đạt (pass) không bao giờ là một sự chứng nhận.

Bộ lọc đưa ra từ chối. Con người đưa ra chứng nhận.

Khi một phát biểu cần phải chính xác, chúng tôi đặt một chuyên gia đánh giá phía sau nó.