WIP: work in progress

Lean の基本的な構文や機能を紹介するためのサンプルコード集です．（執筆中止）

Theorem Proving in Lean 4

コード例で学ぶ Lean 言語

LeanSSR: an SSReflect-Like Tactic Language for Lean

Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

These are Lean translations of Ninety-Nine Haskell Problems (WIP)

mdbook template for Lean project

Formalization of Mathematical Logic

Lean 4 kernel / 'external checker' written in Lean 4

Xena の記事「Mathematics in type theory」の非公式日本語訳です．

Markdown file of the list and explanations of all mathlib4 tactics