Lean4形式化证明

• Lean4
  • 工具链
  • 交互
  • 类型
    • Rat
  • 函数与定义
  • 结构体
  • 关键字
  • 函数
  • 定理与命题
  • Tactics
    • Built-in
      • 逻辑操作
      • 等式化简/转化
    • Mathlib
      • 逻辑操作
      • 等式化简/转化