Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Abusing the algebra of algebraic data types – why does this work?. Parent comment
https://www.ma.imperial.ac.uk/~buzzard/xena/
He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.
There are no comments on this comment yet.
https://www.ma.imperial.ac.uk/~buzzard/xena/
He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.