xena

Mainly for my own reference when I return to this story with more time, links to Professor Kevin Buzzard's project Xena [0][1] >Basically, Lean can understand mathematics, and can check that it doesn't have any mistakes in. Most of the files here are Lean verifications of various pieces of undergraduate level mathematics. >Some of the lean files are in a library called Xena. One could imagine Xena as currently studying mathematics at Imperial College London. [0] https://github.com/kbuzzard/xena [1] https://xenaproject.wordpress.com/

I'll have to work through this when I get the time. I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory. For anyone else with an interests in this area, I'd strong urge you to look at some of the work from Kevin Buzzard (Imperial College), perhaps better known as an algebraic number theorist, who leads the Xena [1] Project, which started as an attempt to completely formalise all the problem sheets for one of the undergraduate maths modules at Imperial in Lean. There's also a GitHub repo [2] with a lot of work to build on. Adam Chlipala (MIT) also teaches a course in formal progr