Hacker News new | past | comments | ask | show | jobs | submit login

That makes me think I am forgetting about the relationship between "logic" and "set theory" (starting point of all maths).



Set theory is the start of most maths right now but it only has been for about a century and this might change. Lean is based on type theory, not set theory. On the other hand, (some sort of) logic seems indispensable.


I was talking about "formal logic".

I don't recall how it is built already.


Really? Category theorists would dispute that.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

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

Search: