Discrete Math's Book in Lean
Book written by the class about some classic topics in Discrete Mathematics and applied in Lean Theorem Prover. It was our final project in the course.
Book written in portuguese, our native language, by the class about some classic topics in Discrete Mathematics and applied in Lean Theorem Prover. It was our final project in the course.
The book was based majorly in the main reference of the course: the book Logic and Proof. The idea is to build important topics in the area using a Theorem Proof, in special the Lean. It was an interesting team project with several difficulties in the process.
The project was organized as follow: each chapter of the original book was designated for a group or a person and that person had to structure it, write it in portuguese, create additional examples and program all in Lean, explaining the code.
Topics
- Introduction: general description, deductive systems and provers, as Lean.
- Lean: description of the language used through the book.
- Propositional Logic: natural deduction and inference rules, as \(\rightarrow\), \(\neg\) or \(\lor\).
- First Order Logic: syntax and semantics.
- Sets: foundations, properties and theorems.
- Relations: concept, order relations and equivalence relations.
- Functions: concept, definitions, second order logic and relations.
- Induction: natural numbers, the principle, arithmetic operations, recursive definitions.