[crystal_revenge]

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

[teiferer]

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.

[zmgsabst]

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]

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

[FridgeSeal]

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.

[simonh]

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]

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]

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.

[6510]

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.

[zmgsabst]

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.

[cornholio]

It's easy to find counterexamples: the entire science of pharmacology is based on macroscopic effects that often lack a fundamental understanding of the underlying mechanisms of action. Psychopharmacology is the extreme example. Often, the fact that a drug worked made scientists investigate and discover the mechanism behind it, but for many drugs used every day by billions it's still a mystery, or it's understood only in very broad terms.

So what will you do if the doctor prescribes you an LLM-vibecoded drug that nobody understands how it works, yet it cures some deadly affliction with close to 100% efficacy?

What if, say, these incomprehensible math results lead to a revolution in quantum physics which unlocks chip topologies that are orders of magnitude faster than human comprehensible designs?

Would the high priestess of human reason pass her divining rod over such chips or life-saving drugs and reject it as the work of the AI devil?

[zmgsabst]

Psychopharmacology is a great example of “doesn’t reliably work” as their products have serious and even disastrous side effects at times — including SSRIs triggering violent acts and suicides.

Again, my exact point is that mathematics loses its utility when you reduce it to that inaccurate usage. You no longer can have any faith in the conclusions — just like sometimes psychiatrists kill their patients with an SSRI prescription because they don’t understand the drugs.

> Would the high priestess of human reason pass her divining rod over such chips or life-saving drugs and reject it as the work of the AI devil?

My point is you can’t know if you’re turning it over for life saving drugs or poison, if you don’t understand what you’re getting.

[cornholio]

This is true for any drug, any drug can presumably become a poison, can interact with some genetic or biological trait and trigger a side effect and so on. The complexity of the biological systems is so great that they defy clear deterministic understanding, but stochastic empiric knowledge and treatments still have immense value.

If you give me an inference chip that runs 200x faster, yes, it could be backdoored to take control of my dishwasher and kill me in my sleep - but I can't deny it runs 200x faster an account of nobody being able to explain why. The same for the mistery cancer drug that cured everyone who took it up to now, but could, without doubt, kill the next patient.

[sdenton4]

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?

[robrain]

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]

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.

[VBprogrammer]

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]

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.

[skydhash]

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

[whattheheckheck]

And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece.

Reasoning by analogy...

[greenavocado]

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

[dripdry45]

No, but SOMEONE did.

[bckgrndrdtn]

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.