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

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 https://github.com/kbuzzard/xena [1] https://xenaproject.wordpress.com/ https://xenaproject.wordpress.com/