Coq and Lean: Powerful Interactive Theorem Provers

Coq and Lean are tools that elevate trust in research and software development with rigorous proofs. They also help to prove that code is bug-free.

- Dr Deepu Benson

It is undenible that the open source software movement is affecting the world positively. But how exactly does open source software impact human lives? First and foremost, it offers popular software for free (free as in ‘free beer’). Nowadays, you don’t have to pay for an operating system or a word processing package. There are tons of open source software freely available for you to choose from. This shift has also prompted software giants to offer their software at relatively lower prices to remain competitive.

However, the impact of open source software extends far beyond this. For instance, the research community in various fields, including science, engineering, technology, management, and social sciences, has greatly benefited from the open source software movement. Notable examples include software like Scilab, SageMath, Project Jupyter, LaTeX, and Python libraries like NumPy and SciPy, among others. The list is so extensive that attempting to enumerate all of them would be futile. In fact, I think I have left out many important names from the list. What makes this even more fascinating is the fact that the open source community boasts some of the world’s most brilliant minds contributing as programmers and software engineers— talent that even the largest software companies can only dream of employing. As a result, highly specialised and technical software has been developed to cater to the needs of communities engaged in top-class research in science, engineering, and technology.

In this article, we will acquaint ourselves with one such category of software: interactive theorem provers.