leanscreen
Lean 4 语句保真度校准筛查工具
leanscreen 是面向自然语言与 Lean 4 形式化语句配对的保真度筛查工具，可在命令行或通过 MCP 供 Claude Code、Desktop 等客户端调用。check_fast 提供确定性 lint、空洞性检查以及基于本地 mathlib 环境的 Lean 4 elaboration；check_deep 追加两个独立 LLM 评审的严格共识判定与反例探测。它只会拒绝存疑语句，通过筛查不等于认证
1
2026-08-11
未收录
5
工具功能
这个工具能做什么、适合谁用，以及目前已识别的核心能力。
工具简介
leanscreen 是面向自然语言与 Lean 4 形式化语句配对的保真度筛查工具，可在命令行或通过 MCP 供 Claude Code、Desktop 等客户端调用。check_fast 提供确定性 lint、空洞性检查以及基于本地 mathlib 环境的 Lean 4 elaboration；check_deep 追加两个独立 LLM 评审的严格共识判定与反例探测。它只会拒绝存疑语句，通过筛查不等于认证
核心功能
价格信息
暂无可验证价格信息暂无足够准确的价格信息。
基础信息
- 更新频率
- 近 7 天 1 条收录动态
- 最近更新
- 2026-08-11
- 覆盖行业
更新日志
按时间记录功能更新、版本发布、新工具入库等重要变化。
- 2026-08-11新工具首发
leanscreen 发布，为自然语言与 Lean 4 形式化语句配对提供校准保真度筛查：可 pip 安装，支持命令行与 MCP 接入 Claude Code/Desktop 等客户端；check_fast 做 lint、空洞性检查和本地 mathlib elaboration（约 0.1 秒），check_deep 加两个独立 LLM 评审共识与反例探测，只筛查不认证。
leanscreen 常见问题
关于 leanscreen 的定位、核心功能、价格与最近更新。
leanscreen 是什么？
leanscreen 是面向自然语言与 Lean 4 形式化语句配对的保真度筛查工具，可在命令行或通过 MCP 供 Claude Code、Desktop 等客户端调用。check_fast 提供确定性 lint、空洞性检查以及基于本地 mathlib 环境的 Lean 4 elaboration；check_deep 追加两个独立 LLM 评审的严格共识判定与反例探测。它只会拒绝存疑语句，通过筛查不等于认证。
leanscreen 有哪些核心功能？
leanscreen 当前已核验的核心功能包括：工具协议集成、静态分析。
leanscreen 如何收费？
AI Equal 当前没有收录 leanscreen 的可验证价格信息。
leanscreen 最近有什么更新？
2026-08-11：leanscreen 发布，为自然语言与 Lean 4 形式化语句配对提供校准保真度筛查：可 pip 安装，支持命令行与 MCP 接入 Claude Code/Desktop 等客户端；check_fast 做 lint、空洞性检查和本地 mathlib elaboration（约 0.1 秒），check_deep 加两个独立 LLM 评审共识与反例探测，只筛查不认证。