David Talone and Christian Kolker

Abstract:

We are proving mathematical theorems using a program called LeanProver. Developed at Microsoft, LeanProver is a mathematical computer language. We started with simple proofs pertaining to the natural numbers, and then we moved onto topics pertaining to Mathematical Analysis. In particular, we proofed multiple lemmas and theorems associated to real analysis.