Which mathematical definitions should be formalised in Lean?

Posted by emileokada on Sunday September 23, 2018 @02:49AM
from the mathoverflow.net dept.

https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean

( 1 comment | 15 points | on HN )

Re:Which mathematical definitions should be formalised in Lean? by emileokada on Sunday September 23, 2018 @02:50AM (#18049760)

I thought this mathoverflow post might be of interest to those who mentioned automated theorem proving in discussions on the recent post on the ABC conjecture (https://news.ycombinator.com/item?id=18034714).

[ Parent | on HN ]