4 ms·

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

• staunton 2y 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 2y ago
    I was talking about "formal logic". I don't recall how it is built already.
  • pfdietz 2y ago
    Really? Category theorists would dispute that.