Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
sylware
15 days ago
|
parent
|
context
|
favorite
| on:
Anatomy of a Formal Proof
That makes me think I am forgetting about the relationship between "logic" and "set theory" (starting point of all maths).
staunton
15 days ago
[–]
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.
sylware
15 days ago
|
parent
|
next
[–]
I was talking about "formal logic".
I don't recall how it is built already.
pfdietz
15 days ago
|
parent
|
prev
[–]
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: