Jack Morrison

Imperial College London

To What Extent are Computer-Assisted Proofs Valid?



This project was completed as my Extended Project during my A Level studies, and discussed the controversy over computer-assisted proofs.
At the start of this project, I was unfamiliar with the area of computer-assisted proofs, and mathematical proofs in general for that matter. I decided on the topic because my mathematics teacher had discussed it in a lesson and I was curious to find out more. He mentioned that many mathematicians, to my surprise, did not agree that a theorem which had been proved using proof by exhaustion on a computer was legitimate. I did not understand their reasoning behind it not being a proof, because I presumed that if every case was proved to be true, then the proof would have to be valid. That is why I became interested in the subject, and when that chance to write a project on the topic arose, I decided I wanted to consider it further.