alt Hacker NewsYou didn’t answer why merge it into a library focused on humans developing mathematics though.
It remains all of those things, sitting alone in its own repository of 200kLOC; what benefit comes from merging it into mathlib?
> There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use.
This is obviously silly:
Things that aren’t human intelligible aren’t human usable, so the restriction is necessary to have a collection of things humans can utilize.
Replies
greenavocado • yesterday at 5:28 AM
My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.
➕ show 1 reply
> Things that aren’t human intelligible aren’t human usable
This is objectively false, people use things every single day they don't understand. We still have plenty of things about the world we don't understand but still find useful.
You are saying anything we know to be the case, but cannot understand why cannot be used? Can we just stop sleeping because we haven't reasoned why sleep is necessary even though we know it is necessary? I mean we still don't really understand gravity (we know how but not why)