4 ms·
Which mathematical definitions should be formalised in Lean?
- emileokada 8y agoI 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 https://news.ycombinator.com/item?id=18034714).