4 ms·

You 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 reposit

You 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.

crystal_revenge 4mo ago
> 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)
- whattheheckheck 4mo ago
  And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
- zmgsabst 4mo ago
  No — people don’t successfully use things they don’t understand every day. They approximately use them with varying degrees of success, but also mistakes, broken inferences, etc. My exact point is that your view reduces our ability to do mathematics to that broken, flawed usage and thereby undermines its utility for logical precision: mathematics is only useful because we cleanly understand it. When you try to use mathematics without understanding, you cause disasters: stock market crashes from mispricing options, Amazon’s 2018 hiring freeze from misallocating $1B, etc. Note: neither of your examples (sleep, gravity) are things that people intentionally use. They just happen to people. I think it’s very telling you couldn’t think of an example.
  - sdenton4 4mo ago
    How many people drive cars without knowing how an engine works? Or make a phone call without knowing how voice compression for a cellular network does it's thing? Or eats food without knowing how it came together from the supply chain?
    - VBprogrammer 4mo ago
      This feels like a stretch. It would be impossible for someone who didn't know how an engine worked to repair or improve the design of it.
      - drdaeman 4mo ago
        Why not? One can surely use math even if they have no clue about how to prove theorems. I suck at math, but I use it every day, without knowing how to advance it. I think it might be fair to say that a proof cannot be without value if it proves something meaningful to a human, that a human can use somehow? But such proof probably doesn’t belong in a library seemingly explicitly dedicated to human-graspable proofs. Just because it violates the intent. It’s not like such proofs mustn’t exist at all.
    - robrain 4mo ago
      The mechanic who repairs the cars knows how the engine works. The telco that manages loads and allocates networks knows how voice compression works. The farmers and supermarkets know how the supply chain works. None of your questions show why mathematics should include blobs of incomprehensible gloop, where no mathematician, no logician, no philosopher, no man on the street can make sense of said gloop, or use it in any way to further human knowledge. When it's been decomposed down we can discuss this further, but now it's like saying red is red, just because.
      - sdenton4 4mo ago
        Well, you said people can't use things they don't understand. But I'll take your expanded statement, to include riding a horse, something even older than the engine. We don't understand fully how a horse works -- biology is still a matter of seeing fragments of the whole -- but people had no problem riding and breeding them before the invention of the car, and before the discovery of genetics. Meanwhile, understanding the math of a thing -- like stock markets, or nuclear bombs -- does not prevent its use from going badly. Math is useful and beautiful, and a helpful tool for expanding our understanding of the world, but it is not the whole of understanding, or the sole factor in successful application of science to the world . Signed, a mathematician.
- FridgeSeal 4mo ago
  If you’re fine with a future like Warhammer 40k where we all have to be Tech Priests making prayers and performing opaque rituals to get things out of the machine god because we no longer understand things, that’s fine, but that’s not a future the rest of us want.
  - 6510 4mo ago
    The problem is that you cant stop it. If there is a wrong way to do something, then someone will do it. Thankfully we understand almost nothing already so it will be easy to adapt - and surrender to the will of the machine.
  - simonh 4mo ago
    It’s not a matter of what we want or don’t want, or are fine with. The universe doesn’t owe us explanations. Of course I’d prefer to understand everything, or as much as possible, but we don’t always get what we want.
    - zmgsabst 4mo ago
      You didn’t respond to his point: In the 40k universe, modern humanity is below not just their peak of technological prowess, but even their peak of pre-AI prowess. Because they landed in a valley of superstition involving machines they do not understand — and have no way to rebuild towards their peak, without yet further losses by moving away from the magical machines. That has nothing to do with the universe at large — and everything to do with human society and choices. Which we do have control over.
      - simonh 4mo ago
        I’m familiar with 40K, I played Laserburn back in the 80s. I met Bryan Ansel before 40K existed. The comment I replied to equivocated between absolute limits to comprehensibility to humans and sociologically constructed limits, implying that thinking there may be the former makes someone ‘fine with’ the latter. That’s nonsense.
- skydhash 4mo ago
  > 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 If you go to the fiction side of things, you’ll get a lot of things that humans would like to do, but can’t right now as we’re blocked by physics laws and our own biology. We have harnessed electricity, why can’t we harness gravity?
greenavocado 4mo ago
My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.
- dripdry45 4mo ago
  No, but SOMEONE did.

crystal_revenge 4mo ago

> 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)

whattheheckheck 4mo ago
And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
zmgsabst 4mo ago
No — people don’t successfully use things they don’t understand every day. They approximately use them with varying degrees of success, but also mistakes, broken inferences, etc. My exact point is that your view reduces our ability to do mathematics to that broken, flawed usage and thereby undermines its utility for logical precision: mathematics is only useful because we cleanly understand it. When you try to use mathematics without understanding, you cause disasters: stock market crashes from mispricing options, Amazon’s 2018 hiring freeze from misallocating $1B, etc. Note: neither of your examples (sleep, gravity) are things that people intentionally use. They just happen to people. I think it’s very telling you couldn’t think of an example.
- sdenton4 4mo ago
  How many people drive cars without knowing how an engine works? Or make a phone call without knowing how voice compression for a cellular network does it's thing? Or eats food without knowing how it came together from the supply chain?
  - VBprogrammer 4mo ago
    This feels like a stretch. It would be impossible for someone who didn't know how an engine worked to repair or improve the design of it.
    - drdaeman 4mo ago
      Why not? One can surely use math even if they have no clue about how to prove theorems. I suck at math, but I use it every day, without knowing how to advance it. I think it might be fair to say that a proof cannot be without value if it proves something meaningful to a human, that a human can use somehow? But such proof probably doesn’t belong in a library seemingly explicitly dedicated to human-graspable proofs. Just because it violates the intent. It’s not like such proofs mustn’t exist at all.
  - robrain 4mo ago
    The mechanic who repairs the cars knows how the engine works. The telco that manages loads and allocates networks knows how voice compression works. The farmers and supermarkets know how the supply chain works. None of your questions show why mathematics should include blobs of incomprehensible gloop, where no mathematician, no logician, no philosopher, no man on the street can make sense of said gloop, or use it in any way to further human knowledge. When it's been decomposed down we can discuss this further, but now it's like saying red is red, just because.
    - sdenton4 4mo ago
      Well, you said people can't use things they don't understand. But I'll take your expanded statement, to include riding a horse, something even older than the engine. We don't understand fully how a horse works -- biology is still a matter of seeing fragments of the whole -- but people had no problem riding and breeding them before the invention of the car, and before the discovery of genetics. Meanwhile, understanding the math of a thing -- like stock markets, or nuclear bombs -- does not prevent its use from going badly. Math is useful and beautiful, and a helpful tool for expanding our understanding of the world, but it is not the whole of understanding, or the sole factor in successful application of science to the world . Signed, a mathematician.
FridgeSeal 4mo ago
If you’re fine with a future like Warhammer 40k where we all have to be Tech Priests making prayers and performing opaque rituals to get things out of the machine god because we no longer understand things, that’s fine, but that’s not a future the rest of us want.
- 6510 4mo ago
  The problem is that you cant stop it. If there is a wrong way to do something, then someone will do it. Thankfully we understand almost nothing already so it will be easy to adapt - and surrender to the will of the machine.
- simonh 4mo ago
  It’s not a matter of what we want or don’t want, or are fine with. The universe doesn’t owe us explanations. Of course I’d prefer to understand everything, or as much as possible, but we don’t always get what we want.
  - zmgsabst 4mo ago
    You didn’t respond to his point: In the 40k universe, modern humanity is below not just their peak of technological prowess, but even their peak of pre-AI prowess. Because they landed in a valley of superstition involving machines they do not understand — and have no way to rebuild towards their peak, without yet further losses by moving away from the magical machines. That has nothing to do with the universe at large — and everything to do with human society and choices. Which we do have control over.
    - simonh 4mo ago
      I’m familiar with 40K, I played Laserburn back in the 80s. I met Bryan Ansel before 40K existed. The comment I replied to equivocated between absolute limits to comprehensibility to humans and sociologically constructed limits, implying that thinking there may be the former makes someone ‘fine with’ the latter. That’s nonsense.
skydhash 4mo ago
> 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 If you go to the fiction side of things, you’ll get a lot of things that humans would like to do, but can’t right now as we’re blocked by physics laws and our own biology. We have harnessed electricity, why can’t we harness gravity?

greenavocado 4mo ago

My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.

dripdry45 4mo ago
No, but SOMEONE did.