idris

Introduction

• Formal theorem proving is a field of rising interest in mathematics where one “codes up” mathematical proofs and chains of reasoning in order to formalize them and get them verified by a computer. This is to avoid various plausible sounding but incorrect arguments from leaking into human-made proofs.
• This also serves the alternate purpose of moving towards automating theorem proving and mathematical reasoning by providing a structured framework for reasoning that can be used to train robust automated mathematical reasoning systems.

What I did

• Implemented proofs of various mathematical results in Idris (a dependently typed language), for the Logic, Types and Spaces course at IISc.
• This involved programming in a dependently typed language.
• Most of the proofs involved results from results on groups, rings and modules (early graduate-level algebra). These were chosen since dealing with analytic and topological results would have been more complex for an experimental course, and had far less support back in 2019.

Code

Link to the code on Prof. Gadgil’s repository. Link to a file listing my contributions.