leanprover/theorem_proving_in_lean4

Theorem Proving in Lean 4

Lean

275

1,059 commits

updated Aug 14, 2026

lean-lang.org/theorem_proving_in_lean4

README

Theorem Proving in Lean 4

This repository contains the source code of the book Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, with contributions from the Lean Community.

To build the book, change to the book directory and run lake exe tpil. After this, book/_out/html-multi contains a multi-page Web version of the book. From the book directory, run lake exe verso-serve to view it.

lean

lean4

Contributors

(top 30 of 78)

287 commits

280 commits

203 commits

31 commits

Similar repos

leanprover/lean

Lean Theorem Prover

2,154

leanprover/fp-lean

Functional Programming in Lean

194

leanprover/theorem_proving_in_lean

Theorem proving in Lean

49

leanprover/functional_programming_in_lean

A book about functional programming in Lean

47

leanprover/vscode-lean4

VS Code extension for the Lean 4 programming language and theorem prover

313

leanprover/verso

Lean documentation authoring tool

386

leanprover/doc-gen4

Document Generator for Lean 4

173

leanprover/LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

67

Languages

Lean

95.6%

CSS

3.0%

TeX

1.1%

leanprover/theorem_proving_in_lean4

Theorem Proving in Lean 4

Lean

275

1,059 commits

updated Aug 14, 2026

lean-lang.org/theorem_proving_in_lean4

README

Theorem Proving in Lean 4

This repository contains the source code of the book Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, with contributions from the Lean Community.

To build the book, change to the book directory and run lake exe tpil. After this, book/_out/html-multi contains a multi-page Web version of the book. From the book directory, run lake exe verso-serve to view it.

lean

lean4

Similar repos

leanprover/lean

Lean Theorem Prover

2,154

leanprover/fp-lean

Functional Programming in Lean

194

leanprover/theorem_proving_in_lean

Theorem proving in Lean

49

leanprover/functional_programming_in_lean

A book about functional programming in Lean

47

leanprover/vscode-lean4

VS Code extension for the Lean 4 programming language and theorem prover

313

leanprover/verso

Lean documentation authoring tool

386

leanprover/doc-gen4

Document Generator for Lean 4

173

leanprover/LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

67

Contributors

(top 30 of 78)

287 commits

280 commits

203 commits

31 commits

Languages

Lean

95.6%

CSS

3.0%

TeX

1.1%