4 ms·

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob Anyone who understands type theory and how theorem provers work? It's sort of ak

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this is different than saying the program behaves correctly, but that's precisely the difference between formal proofs and compiled programs). The entire argument both you and Bessis are implying is that mathematics must be human intelligible. But there's absolutely no reason to assume that every mathematical statement must have a human intelligible representation. 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. Just because people who don't want this to be true, and I can understand the motivation, doesn't mean that it isn't still the case.

zmgsabst 3mo ago
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 3mo 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 3mo ago
    And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
  - zmgsabst 3mo 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 3mo 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 3mo 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 3mo 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.
- greenavocado 3mo ago
  My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.
  - dripdry45 3mo ago
    No, but SOMEONE did.
teiferer 3mo ago
Imagine tomorrow all source code for all software disappears. Would we still be able to use computers? Of course! They don't need the source code to run. Would we nevertheless be in big trouble? Oh definitely. We'd need to write all software again, from scratch. Some critical parts we could reverse engineer. Maybe even derive some structures that translate back into source code, but only because a human wrote that source code in the first place. Hopefully the point is clear: A proof, even if it is correct, that is totally obscure and unintelligable by humans is not very useful for mathematics. It's a black box that doesn't further understanding of the structures and approaches to think about them, and that's what math is all about.Just having a big binary blob of a program doesn't help much if you want to add a feature. That's also why biology is so hard. There is no source code. It's just millions and millions of years of evolution and things have evolved in weird ways that don't really make it easy to understand them, even though they clearly work.
bckgrndrdtn 3mo ago
You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}... Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies. You can have all the type theory of the world, but the library still needs maintenance. Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them. Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library? And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.
tripzilch 3mo ago
> "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!" I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.

zmgsabst 3mo ago

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 3mo 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 3mo ago
  And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
- zmgsabst 3mo 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 3mo 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 3mo 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 3mo 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.
greenavocado 3mo ago
My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.
- dripdry45 3mo ago
  No, but SOMEONE did.

teiferer 3mo ago

Imagine tomorrow all source code for all software disappears. Would we still be able to use computers? Of course! They don't need the source code to run. Would we nevertheless be in big trouble? Oh definitely. We'd need to write all software again, from scratch. Some critical parts we could reverse engineer. Maybe even derive some structures that translate back into source code, but only because a human wrote that source code in the first place. Hopefully the point is clear: A proof, even if it is correct, that is totally obscure and unintelligable by humans is not very useful for mathematics. It's a black box that doesn't further understanding of the structures and approaches to think about them, and that's what math is all about.Just having a big binary blob of a program doesn't help much if you want to add a feature. That's also why biology is so hard. There is no source code. It's just millions and millions of years of evolution and things have evolved in weird ways that don't really make it easy to understand them, even though they clearly work.

bckgrndrdtn 3mo ago

You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}... Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies. You can have all the type theory of the world, but the library still needs maintenance. Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them. Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library? And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.

tripzilch 3mo ago

> "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!" I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.