# idris

Interactive proofs in Idris, 2019.

### 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.