Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Mathematicians welcome computer-assisted proof in ‘grand unification’ theory. Parent comment
- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.
- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained
There are no comments on this comment yet.
- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.
- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained