alt Hacker News> 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.
Replies
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.
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.
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.