View Proposal

Proposer
Fairouz Kamareddine
Title
Checking the correctness of a mathematical book in Lean/Coq/Isabelle
Goal
Take your favourite book of mathematics and check it in the language lean
Description
Computer checking the correctness of entire books of mathematics has moved on since the ideas were first introduced independently by de Bruijn in his Automath system and Trybulec in his Mizar system. Since, Computer systems have been created to check the correctness of not only mathematical books but of software and information in general. In this project you will investigate the checking of a a mathematical book in a choice of three computer checkers: Isabelle, Coq or Lean. You will first need to familiarise yourself with one or all of these systems after you have done the background research on them, and then you will need to investigate initial proving of a couple of results you have studied in one of your favorite courses (e.g., it could be your course on discrete mathematics or logic and proof or lambda calculus or Turing machines), and then decide whether you want to do all the work in one prover or you want to compare the three provers in question.
Resources
Background
Url
Difficulty Level
High
Ethical Approval
None
Number Of Students
1
Supervisor
Fairouz Kamareddine
Keywords
Degrees
Back to List