Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> resolutely non-classical approach

Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics ….

As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic).



:-) Yes, by assuming classical logic the Lean community is taking a non-classical approach to bringing formalisation to the masses :-)




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

Search: