⚡

Lean定理证明助手Skill lean-proof-assistant

Lean 定理证明助手是一个基于 Lean 4 形式化验证系统的专业工具，专注于数学定理的形式化证明与验证。它能够将非形式化的数学证明转化为机器可检查的 Lean 代码，利用 Mathlib4 数学库中的已有成果，通过自动化策略辅助用户完成严谨的证明过程。该工具适用于数学研究、计算机科学中的形式化方法验证以及数学教育等领域。 关键词：Lean 4, 定理证明, 形式化验证, 数学形式化, Mathlib4, 证明助手, 自动推理, 策略证明

其他 0 次安装 0 次浏览 更新于 2/25/2026

name: lean-proof-assistant description: 与 Lean 4 证明助手交互，用于形式化定理验证 allowed-tools:

  • Bash
  • Read
  • Write
  • Edit
  • Glob
  • Grep metadata: specialization: 数学 domain: 科学 category: 定理证明 phase: 6

Lean 证明助手

目的

为使用 Lean 4 证明助手进行形式化定理验证和数学形式化提供专家指导。

能力

  • 将非形式化证明解析为 Lean 4 语法
  • 生成基于策略的证明脚本
  • 访问 Mathlib4 库以获取标准结果
  • 自动项重写和简化
  • 生成带有 sorry 占位符的证明大纲
  • 从证明中提取可执行代码

使用指南

  1. 证明开发：使用符合 Mathlib4 约定的 Lean 4 语法
  2. 策略应用：系统地应用策略（intro, apply, exact, rw）
  3. 库导航：在 Mathlib4 中搜索现有的引理和定理
  4. 证明完成：逐步填充 sorry 占位符

工具/库

  • Lean 4
  • Mathlib4
  • Lake 构建系统
  • VS Code Lean 扩展