Lean - main-custard

Lean

from 気になる

最も気になるのは,学部生レベルの数学をLLMを使って効率的に学ぶために有用なのでは,という点

cf. Lean が数学科に流行ると何がうれしいのか

Leanで書かせる,というのは非常に面白そう. 初めてlatexを触った時のように,ワクワクする

ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発

大学数学すらおぼつかないが,関数型言語に興味がある

将来的にどこまで数学を学ぶかは不明だが,学習の一助になるのなら嬉しい,という打算もある

日本のコミュニティ: https://lean-ja.github.io/

リソース: https://lean-ja.github.io/links/