Hacker News new | past | comments | ask | show | jobs | submit login

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/

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact