由于各自不同的原因，发现大家这个学期都开始学习起 Lean 了起来，我也不能免俗囧。L∃∀N 一看 logo 就很帅，有点 DUNE 的设计感有没有？

感觉首要工作是先复习一下 Haskell，这样也不必中途翻阅语法手册。显然 Lean4 从 Haskell 里借鉴了相当多的语法和设计思想，说来惭愧，虽然我之前试图用 Haskell 刷刷题，但是总是感觉不得要领，被复杂度卡的死死的囧不得不中途切回 cpp 艹。fingertree 什么的也看的云里雾里，感觉还是我的姿势水平不够，还需特别努力！

然后初学 Lean 我是建议先看 Mathematics in Lean，本书直接使用 mathlib，让你不必过早的被细节劝退，又可以顺便复习一下熟悉的数学知识（初等数论她不香吗，天天学代数人都学傻了）。而且还提供对应的 Github 仓库，可以 step-by-step 边看别改。Lean 不能没有 mathlib，就像是 cpp 不能没有 std，西方不能没有耶路撒冷？

（目前感觉这语言除了优化不行哪哪都还可以？）

再然后感觉可以试试写点题目，比如可以试试先证明静态直径算法？

学习

• Lean (proof assistant), Wikipedia
• https://leanprover-community.github.io/learn.html
• Lean Focused Research Organization
• Theorem Proving in Lean
• Mathematics in Lean
• Type Checking in Lean 4
• Functional Programming in Lean
• https://lean-lang.org/lean4/doc/

习题

• 验证了 scc 的 kosaraju 图算法
• 验证魔方算法

研究

• Peano: Learning Formal Mathematical Reasoning
• Proof Artifact Co-training for Theorem Proving with Language Models
• Generative Language Modeling for Automated Theorem Proving
• Solving (some) formal math olympiad problems
• LeanDojo: Theorem Proving in Lean using Language Models
• 千里冰封 – Canonical定理证明器 -20240508-（内部报告，非公开演讲，仅限爱好者交流）

项目

• Xena project
• Formalizing the proof of PFR in Lean4 using Blueprint: a short tour
• The Fermat’s Last Theorem Project

Posted by xiaodao
Category: 日常