haskell-jp / mokumoku-online #87 at 2026-07-05 18:06:10 +0900

Project Euler #138 Pythagorean triples の Euclid's formula を用いて | b - h | == 1 その近くを２次方程式で近似して全探索　一発 OK 　Lean の文法書ばかり読むのはホント退屈で飽きてきた　いろいろと Haskell 似なところは良いとして　それで？という疑問が去らない　実用的にどこが良いのかもっと入門者に訴えてくるものが欲しい

Leanを実用、となればやっぱり定理証明支援系として使う入門書が良いのではないでしょうか。詳しい方々に伺ってみたところ、で参照されている、こちらを提案されました。
https://github.com/lean-forward/logical_verification_2025

ありがとうございます　後日読んでみます