In this project, two problems from elementary number theory are explored with the aid of the Coq Proof Assistant (tCPA). The first is concerned with the parity of Fibonacci numbers (is the fifth Fibonacci number odd or even?).
The second is a discussion of a formula for computing polygonal numbers from Prof Danvy’s Summa Summarum. The prerequisites to follow the core body of this final project includes a basic familiarity with both the Coq Proof Assistant, the technique of mathematical induction, and high-school algebra.
There is a report associated with the project which gives explainations of the formal proofs.
To follow the digressions in the Lagniappes and Vantage Loaf, a basic knowledge of elementary number theory is required. However, these are in no way required to follow the main line of discussion and may be safely skipped over.