First of all, thank you very much @avigad for writing this textbook and making it publicly available for free! I'm very new to formal mathematics (and Lean in particular) and resources such as this one are crucially important for my learning experience!
While consulting this online textbook I've collected the following typos.
1. Introduction
Four centuries later, Lull's work resonated with Gottfied Gottfried Leibniz, [...]
2. Mathematical Background
The following item isn't displayed correctly (i.e. enumerated):
. Prove by structural recursion that for any (extended) binary tree $t$, we have
$\fn{size}(t) \le 2^{\fn{depth}(t)} - 1$.
6. Decision Procedures for Propositional Logic
The function propagateWithNew is used to peform perform a split on the literal x.
7. Using SAT Solvers
the the same horizontal line, vertical line, or square. Below is one of the hardest sudoko sudoku puzzles with only 17 given numbers.
12. Decision Procedures for First-Order Logic
The first three rules express the reflexivity, symmmetry symmetry, and transitivity of equality,
respectively.
avigad
commented
1 year ago
First of all, thank you very much @avigad for writing this textbook and making it publicly available for free! I'm very new to formal mathematics (and Lean in particular) and resources such as this one are crucially important for my learning experience!
While consulting this online textbook I've collected the following typos.
1. Introduction
2. Mathematical Background
The following item isn't displayed correctly (i.e. enumerated):
6. Decision Procedures for Propositional Logic
7. Using SAT Solvers
12. Decision Procedures for First-Order Logic