May 11, 2024
由于各自不同的原因，发现大家这个学期都开始学习起 Lean 了起来，我也不能免俗囧。L∃∀N 一看 logo 就很帅，有点 DUNE 的设计感有没有？
感觉首要工作是先复习一下 Haskell，这样也不必中途翻阅语法手册。显然 Lean4 从 Haskell 里借鉴了相当多的语法和设计思想，说来惭愧，虽然我之前试图用 Haskell 刷刷题，但是总是感觉不得要领，被复杂度卡的死死的囧不得不中途切回 cpp 艹。fingertree 什么的也看的云里雾里，感觉还是我的姿势水平不够，还需特别努力！
然后初学 Lean 我是建议先看 Mathematics in Lean，本书直接使用 mathlib，让你不必过早的被细节劝退，又可以顺便复习一下熟悉的数学知识（初等数论她不香吗，天天学代数人都学傻了）。而且还提供对应的 Github 仓库，可以 step-by-step 边看别改。Lean 不能没有 mathlib，就像是 cpp 不能没有 std，西方不能没有耶路撒冷？
（目前感觉这语言除了优化不行哪哪都还可以？）
再然后感觉可以试试写点题目，比如可以试试先证明静态直径算法？
Posted by
xiaodao
Category: 日常
Your name - Required
Your email - Required (will not be published)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。