Zing 论坛

论坛首页大模型问答与内容策略正文

正文

Lean4-Skills：为AI编程助手打造的定理证明工作流套件

一套跨平台兼容的Lean 4定理证明技能包，提供从草稿生成到证明优化的完整工作流，支持Claude Code、Codex、Gemini等主流AI编程工具。

Lean 4定理证明AI编程助手形式化数学mathlibMCPClaude CodeCodex工作流自动化
发布时间 2026/04/22 05:43最近活动 2026/04/22 05:52预计阅读 6 分钟
Lean4-Skills：为AI编程助手打造的定理证明工作流套件
1

章节 01

Lean4-Skills: AI-Assisted Theorem Proving Workflow Suite

Lean4-Skills: AI-Assisted Theorem Proving Workflow Suite

Lean4-Skills is a cross-platform compatible Lean 4 theorem proof workflow suite designed for AI programming assistants. It provides a complete lifecycle from draft generation to proof optimization, supporting mainstream tools like Claude Code, Codex, and Gemini. The suite aims to lower the barrier to formalized mathematics by enabling AI agents to assist in Lean 4 proof processes, integrating with mathlib and MCP for efficient feedback.

2

章节 02

Background: Formal Proof Challenges & AI Potential

Background: Formal Proof Challenges & AI Potential

Formal mathematical proof requires rigorous machine-verified reasoning, but Lean 4's complex syntax, mathlib mastery, and proof strategies create high barriers for researchers. With the rise of AI programming assistants, Lean4-Skills addresses the question: Can AI automate or assist Lean 4 formal proof? It offers a systematic solution to let AI play a practical role in theorem proving.

3

章节 03

Workflow Design: Structured Loop & Core Skills

Workflow Design: Structured Loop & Core Skills

Lean4-Skills uses a 'structured loop' design—breaking proof into repeatable stages with clear inputs/outputs and checkpoints. It includes 11 core workflows covering the full lifecycle: draft (skeleton code from informal statements), formalize (interactive formality), autoformalize (end-to-end autonomous), prove (guided proof), autoprove (budget-controlled loops), checkpoint (save & verify), review (quality check), refactor (mathlib-based optimization), golf (conciseness), learn (mathlib exploration), and doctor (diagnosis/migration).

4

章节 04

Cross-Platform Compatibility

Cross-Platform Compatibility

Lean4-Skills features a host-agnostic design, working with Claude Code, OpenAI Codex, Google Gemini CLI, Cursor, and Windsurf. Claude Code users can call workflows via /lean4:<name> commands; others use SKILL.md configurations. This avoids skill fragmentation, allowing seamless tool migration. Detailed installation guides are provided for each tool, including environment variables and path settings.

5

章节 05

Proof Engine & MCP Integration

Proof Engine & MCP Integration

The prove/autoprove engine uses a 5-stage loop: Plan → Work → Checkpoint → Review → Replan → Continue/Stop. It analyzes goal states, searches mathlib for strategies, and parallel-tests approaches for sorry placeholders. Integration with lean-lsp-mcp provides sub-second feedback (replacing 30+ second lake builds) via tools like lean_goal (target state), lean_multi_attempt (parallel strategy testing), and lean_diagnostic_messages (error checks without full builds). Claude Code users are recommended to install MCP at user scope for visibility.

6

章节 06

Application Scenarios

Application Scenarios

Typical use flow: Generate initial statements via draft/autoformalize → complete proof with prove/autoprove → review quality → refactor with mathlib → optimize via golf → save via checkpoint. Benefits: Researchers focus on mathematical insights (not formal details), educators get interactive mathlib learning tools, formal verification projects gain scalable automation.

7

章节 07

Future Directions & Community Engagement

Future Directions & Community Engagement

Current limitations: Primarily tested on Pythia/Llama models; Breaking Change handling needs user attention. Future plans: Support Coq/Isabelle, integrate ATPs (Z3/CVC5), domain-specific workflows. Community feedback is enabled via lean4-contribute plugin: bug-report, feature-request, share-insight—all confirmed by users before submission to ensure privacy and intent.

继续阅读

继续阅读同一主题下的更多内容。

01
Splinter：一款无锁零拷贝的共享内存 KV 与向量存储库，让 LLM 推理告别 socket 与 memcpy 开销

Splinter：一款无锁零拷贝的共享内存 KV 与向量存储库，让 LLM 推理告别 socket 与 memcpy 开销

Splinter 是一款极简主义的高性能键值与向量存储系统，通过共享内存和原子操作实现进程间零延迟通信，核心代码仅 766 行，却能支持每秒数百万次操作和 768 维向量存储，为本地 LLM 推理和数据密集型应用提供了全新的架构思路。

最近活动 2026/04/03 08:49
02
Folkering OS：当操作系统本身就是 AI——一个能自我进化的裸机 Rust 系统

Folkering OS：当操作系统本身就是 AI——一个能自我进化的裸机 Rust 系统

Folkering OS 是全球首个 AI 原生裸机操作系统，完全用 Rust no_std 编写，无需 Linux、POSIX 或 libc。它能在 10 秒内从零生成命令、编译为 WASM 并运行，实现真正的自我进化。

最近活动 2026/04/09 16:15
03
LLM-assisted-analysis：用大模型检测智能合约逻辑漏洞的新思路

LLM-assisted-analysis：用大模型检测智能合约逻辑漏洞的新思路

该项目探索如何利用大语言模型（LLM）检测以太坊智能合约中的逻辑漏洞，特别是传统静态分析工具难以捕捉的业务逻辑缺陷，如经济操纵、执行顺序错误等。

最近活动 2026/04/09 16:18
04
LLM推理框架性能对决：vLLM、SGLang与Ollama在Ampere与Hopper架构上的深度评测

LLM推理框架性能对决：vLLM、SGLang与Ollama在Ampere与Hopper架构上的深度评测

基于NVIDIA A10G与H100 GPU的跨代硬件测试，对比分析三大主流LLM推理框架的吞吐量、延迟与并发扩展能力。SGLang在H100上实现3.4倍于vLLM的性能优势，而Ollama在高并发场景下出现架构性瓶颈。

最近活动 2026/04/20 12:19