We’re grateful to have Prof. Kevin Buzzard as our speaker giving a talk on “Can a computer do your problem sheets?” at Nov 9th) in Main Lecture Hall, Old Divinity School, St John’s College.
“We all know a computer can e.g. very quickly add up the first million prime numbers. But can a computer prove some random theorem on your vector spaces problem sheet or your algebraic geometry problem sheet? The standard programming languages which mathematicians and computer scientists are taught at school or uni can’t, because they are not expressive enough to state and prove theorems. Lean is a programming language which can. To see it in action, try https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/(link works on computers but not phones). I’ll talk about how I’m using Lean to do mathematics from undergraduate level to Fields Medal level and how you can get involved too (and even make money and get publications!). No background in programming is necessary. Suitable for 1st year (and higher year!) mathematicians.”
