psibi/how-to-prove

My Solution to Velleman's book

TeX

275

384 commits

updated Oct 2, 2025

See the code

README

How to Prove It: A Structured Approach

Contains solution for the Velleman's book.

The reason I have started studying this is to ultimately study type theory.

Feel free to raise issue if you think a proof is wrong or if it needs some clarification. Pull requests and contributions are welcome.

Credits

David Cantrell for Section 3.3 and various other improvements.

Notes:

From Chapter 2, I have moved from markdown format to Latex as it helps in much easier rendering of mathematical symbols. It can be compiled using pdflatex:

pdflatex tex_filename

Although I did solve Chapter 3 problems, I haven't uploaded all of them yet because of my laziness.

Contributors

362 commits

5 commits

4 commits

4 commits

Similar repos

djvelleman/HTPILeanPackage

Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It"

blanchette/logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

119

barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

205

hrmacbeth/math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

372

leanprover/theorem_proving_in_lean4

Theorem Proving in Lean 4

275

mo271/FormalBook

Formalizing "Proofs from THE BOOK"

sdiehl/zero-to-qed

From Zero to QED: An informal introduction to formality with Lean 4

126

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

Languages

TeX

99.5%

psibi/how-to-prove

My Solution to Velleman's book

TeX

275

384 commits

updated Oct 2, 2025

See the code

README

How to Prove It: A Structured Approach

Contains solution for the Velleman's book.

The reason I have started studying this is to ultimately study type theory.

Feel free to raise issue if you think a proof is wrong or if it needs some clarification. Pull requests and contributions are welcome.

Credits

David Cantrell for Section 3.3 and various other improvements.

Notes:

From Chapter 2, I have moved from markdown format to Latex as it helps in much easier rendering of mathematical symbols. It can be compiled using pdflatex:

pdflatex tex_filename

Although I did solve Chapter 3 problems, I haven't uploaded all of them yet because of my laziness.

Similar repos

djvelleman/HTPILeanPackage

Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It"

blanchette/logical_verification_2023

Hitchhiker's Guide to Logical Verification (2023 Edition)

119

barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

205

hrmacbeth/math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

372

leanprover/theorem_proving_in_lean4

Theorem Proving in Lean 4

275

mo271/FormalBook

Formalizing "Proofs from THE BOOK"

sdiehl/zero-to-qed

From Zero to QED: An informal introduction to formality with Lean 4

126

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

Contributors

362 commits

5 commits

4 commits

4 commits

Languages

TeX

99.5%