math-formalizations

by Evgeny Ivashkevich

This project is focused on the formalization of some elementary mathematical theories in Coq and is intended as a compagnion to the lecture course on math formalizations and certified programming:

1. Sort function as a demonstration of certified programming style
2. Propositional algebra and calculus, their soundness and completeness
3. Untyped lambda calculus
4. Constructive axiomatics for plane Euclidean geometry (https://arxiv.org/abs/1903.05175)
5. Hughes algorithm for list reverse function
6. Example of Goedel's Incompleteness Theorem