[skybrian]

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use:

> A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs and abstractions, without which no autoformalization could take place. By contrast, Math Inc’s autoformalized proof of Viazovska’s results exposes no intelligible interface. Who in their right mind would merge a 200,000-line unaudited vibe-coded blob into the master branch of global human science?

https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...

[hiAndrewQuinn]

Imo, the proved theorem is the API. And that's really all it has to be.

If there are other lemmas, etc buried inside that 200k blob that can be factored out and proved and used themselves, so much the better. But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me. I see no reason not to accept the vibe coded blob if Lean says it's kosher except anthropocentrism.

[bckgrndrdtn]

You are conflating:

(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.

Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.

Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.

[murderfs]

So add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?

[TheOtherHobbes]

You can't deny it if it's true, but the point is to find new techniques and abstractions. A proof you can't extrapolate and learn from is just a checkmark, and about as useful.

[hiAndrewQuinn]

I don't think that's the point. I think the point is to prove the statement. The techniques and abstractions are a means to an end; making them the point is being seduced by the beauty of the weapon.

[OtherShrezzing]

Most of the interesting research I’ve ever done started while reading through the intermediate steps in an unrelated paper.

As far as I can tell from colleagues in other domains, it’s the same there. One paper will mention something off-hand and that’ll cause someone else to have a spark of insight, which turns into it’s own valuable research

[freehorse]

New techniques and abstractions is how mathematics expand. Mathematics is about studying structures, proving statements is a part of it but it is not all what mathematics is about. If anything, proofs themselves are a means to an end (understanding). Eg Galois developed some techniques and abstractions to prove that there is no general solution to polynomial equations of degree >=5, but these techniques and abstractions gave rise to whole new mathematical fields.

Mathematics has to be also understood from the perspective of theory building, not just problem solving.

[crote]

> I think the point is to prove the statement.

I couldn't disagree more.

A lot of mathematical "problems" are almost entirely pointless. Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map - it is the math that is developed during the solving process that is valuable!

An answer to a question like "what is the exact area of a unit circle" is a mere curiosity. Calculating a good-enough approximation is trivial, after all. But wanting an exact answer leads to developing calculus, which leads to most modern physics. Science was able to make a giant leap forwards due to the techniques developed, while the actual answer itself is mostly useless.

[indiv0]

My instinct is to agree with you. I believe that the drive to a deeper understanding of the problems is what helps us unlock new areas of study, and find opportunities to transfer techniques or bridge otherwise unconnected domains.

But let’s consider a hypothetical: what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? If there truly is no way to simplify some proofs down from 200,000 line incomprehensible gibberish to something you could teach to a high schooler or undergraduate or even a PhD. Is the proof still worthless? Sure, at the moment, it might be. Finding such a proof and understanding the implications of it are different skills, the latter of which AI almost certainly does not possess at the moment. But there may come a time where the AI can view the bigger picture and make the leaps you described (say, an eka-Calculus from an eka-unit-circle). These leaps may be as unintelligible to us as the proof in OP is.

I guess the question is: assuming that we can’t make the proof beautiful enough to spark deeper human understanding, do we still want it if it sparks deeper AI understanding?

Personally I would hate to live in a universe where the boundaries of science are beyond intuitive human understanding, but I think it’s almost certainly the case. The idea that the rules are all within our grasp reeks of anthropocentrism to me. I would love for the universe to prove me wrong though. It’d be a pleasant, hilarious coincidence if they do fit within the boundaries of our understanding.

[Twey]

Mathematics, and its empirical cousin science, are not about picking out individual things that are true in the universe. There is an infinite set of statements of things that are true about the universe, almost all of which are, necessarily, too complex (in a Kolmogorov sense) to be captured by a human mind, and each of which is so specific as to be largely useless. Once you have a statement, though, they're usually trivial to prove by observation.

Mathematics and science are both about building structure on large classes of facts about the (logical or physical, respectively) universe that allow us to generalize our knowledge and make predictions about facts we cannot yet observe. This also lets us make claims about things that are, individually, too complex for the human mind to grasp, by abstracting away the complex details into a simpler structure and then making the claim about anything that satisfies that structure.

To put it another way, mathematics is about finding beauty — specifically those things that exhibit structure that humans can grasp. Modern mathematics, for the most part, makes no claims about what lies outside that space: if it turns out that the universe consists only of things that humans can describe through mathematics that would be neat, but in the much more likely case that it doesn't mathematics continues as it is today.

It's an interesting and maybe even useful trivium if (according to some set of axioms, such as those implemented by your favourite proof assistant) a fact is true, but it's not (human) mathematics, and if there's no useful way for humans to generalize from it there's no point in including it in a library of mathematics. It wouldn't be that surprising (but would be very interesting!) if there were an entire parallel class (or, more likely, family of classes, one for each AI architecture) of AI mathematics comprising structures that AIs can usefully generalize from. Such a thing has no reason to bear any resemblance to human mathematics, which is based on mapping structures to innate human linguistic and spatial intuitions, and may not yield any insights to human mathematicians.

[crote]

> what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind?

By extension: why should we assume that a human would still understand the problems - or the answers? If all of it is complete gibberish to a human and can never be applied in any way, shape, or form, then what's the point?

The way I view it there are two options here: either you completely ignore it and end up burning a massive amount of electricity on what is essentially a bunch of LLMs jerking each other off, or you blindly follow it and end up with a Machine God who can justify a genocide with a "This is the correct thing to do. Trust me bro, I have irrefutable proof - you won't understand it". There's just no sensible way to do post-human math in an inherently human world.

[hiAndrewQuinn]

"Mathematics isn't about proving the statement! It's about the collection of substatements which lead to the proof of the statement."

"Okay, so what determines what is and is not allowed in the collection?"

"Whether the given substatement is true or not, of course."

Like this is obviously silly, right. In your view you could have two guys both trying to prove or disprove that the area of the unit circle is 3, and yet only the guy doing it with some vision of nobility where he's building up to this grand theory of approximations is the one actually doing "real" mathematics. The guy who's doing it just because he thinks it's neat and would like an answer to the problem itself doesn't count, and you suspect he couldn't even exist.

[crote]

"Dear 13th-century Magical Oracle, It is possible to transmute lead into gold?" "Yes. This pile of giant incomprehensible spaghetti[0] is the irrefutable proof that it is possible."

What did the alchemist truly learn from this interaction? Is the answer in any way helpful for him? Will it lead to him making gold, and the implied endless riches it entails? Why should it bring him him to ask follow-up questions with useful answers like "The technology to do this doesn't exist yet and can't be developed within several lifetimes" and "It'll never be economically profitable to turn lead into gold", instead of blindly being fed piecemeal steps in the impossible task of one medieval guy building a LHC?

Writing true statements is absolutely trivial, anyone can do that. There's an endless amount of true statement which have absolutely no value to humanity whatsoever. Their proof is meaningless without something to give it context. "Substatement 1304 is true" has significantly less value than "here's something I call 'group theory', and it might also be helpful solving open issues in fields X, Y, and Z".

Mathematics is about widening our collective understanding. There will of course be some people out there who'll hear "The answer to life, the universe, and everything is forty-two", think "Neato!", and go on with their day without giving it any further thought - but I'd have a hard time calling them mathematicians.

That doesn't mean it is completely useless, of course. A "prove that no efficient algorithm exists to break this new encryption scheme" would be very helpful indeed. Until you realize it neglected to take quantum computing into account, of course.

[0]: https://home.cern/alice-detects-conversion-lead-gold-lhc/

[alberto-m]

The argument of your imaginary dialogue is very weak. To run a valid marathon one must cover 42 kms, but we do not run marathons because we want to be 42 kms away. Building a robot to do that would be probably an interesting feat for robotics, but it would not leave any mark in the history of the sport.

[program_whiz]

Isn't the question at hand whether its bad for mathematics if "prove the circle has area 3" devolves into 500 lines of inscrutable lean code, vs just having `pi r^2 == 3`? Sure they both "proved" it true/false, but knowing an answer isn't as useful as knowing why its an answer. Knowing an answer does have some value, its just not as valuable. If I can't work it out myself, I just trust the oracle.

Now if you ask "does the area of unit circle equal 4?", I don't really know, but we can go back to the oracle and ask again (we haven't learned the general pattern).

Also, I'm not sure that assuming this 'area of circle' question was cutting edge math, that the oracle wouldn't say 'yes, to a certain level of tolerance'. Can't count how many times I've seen agent decide a test needs to be loosened or deleted because its an "edge case" or "blocking". If you don't understand the proof you might get back 'yes' for some versions of 'is the area of unit circle 3' (depending on complexity of that ask).

[YeGoblynQueenne]

I guess if I project this argument onto software engineering there is no need to write maintainable code; as long as a vibe-coded blob of horror spaghetti "does the job" demanding that the blob is "comprehensible with what a human being considers a reasonable effort" is anthropocentrism.

Have I treated your argument unfairly?

[mittensc]

There's a difference in math between giving just the answer to a problem and doing it properly/elegantly.

So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.

[_zoltan_]

there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is.

just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.

[crote]

> just as we don't re-prove Fermat's little theorem every time I use it in a proof

Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface.

But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfully repurpose the individual Lego blocks to build a different interface. You end up having to reinvent the same Lego blocks over and over again, just with a slightly different color each time.

Don't want to re-prove each and every Lego brick? Then you shouldn't accept giant black box proofs.

[whoke]

I think the interesting part here is that the black box gives us a starting point. And it's not a true black box: if a model is generating Lean, we can examine the entire source, iteratively refine by refactoring into smaller self-contained units, and the compiler gives us the certainty that our decomposition is correct.

[fdupress]

The theorem doesn't exist in a vacuum. It talks about objects that must be formally defined. And if that formal definition (which is part of the API) is not immediately compatible with those others use, and every single theorem comes with its own definitions of the objects they're working on, you're going to be reinventing the wheel over and over again.

Replacing thought and curation with repeated automation is tech debt, pushed down to fundamental knowledge and understanding.

[ben_w]

> I see no reason not to accept the vibe coded blob if Lean says it's kosher except anthropocentrism.

The laws of mathematics exist and their truths hold before they are proven by humans or our machines, so in a very real sense the entire point of proving anything in the first place is anthropocentrism.

That, plus cleaning it up may reveal it contains proofs of other things we also want to know. Imagine if this happened to also contain as a sub-part a proof of all the open Millennium Prize Problems? We don't know until we investigate. (If it was a specific list of things to check from rather than expanding humanity's library, we could just ask an AI to do it for us… but as The Wachowski sisters wrote in their most famous script: "I say your civilization because as soon as we started thinking for you, it really became our civilization").

[Diogenesian]

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct. But you gotta check.

This future of "the AI built the compiler and it's totally incomprehensible spaghetti, but don't worry, it verified the compiler works using this AI-generated proof assistant whose codebase is also pure spaghetti" terrifies me.

[bckgrndrdtn]

> These proof checkers all have bugs, every single one

Please show me a proof of `False` in Lean.

[Diogenesian]

That's not what I mean. I am talking about quirks and bugs that really are pretty subtle, and which really might turn up in e.g. a verified systems programming context: https://github.com/James-Hanson/junk-theorems-in-lean/blob/m... (there is a proof of 0=1 at the end - it is easy to understand where it comes from, but low-level compiler stuff like this is always a possibility.)

LLM agents will a) discover dumb counterintuitive stuff like this and b) exploit it to satisfy the kernel with c) the questionable lines being buried behind millions of lines of math slop. Humans have to check this stuff.

[cdetrio]

I'd be very curious whether such junk lean code could be used to solve Kevin Buzzard's Jacobian challenge: https://gist.github.com/kbuzzard/778bc714030b3e974ab5f403878...

The idea behind the challenge to provide a few lines of human-written/checked scaffolding that defines an "API surface". The API surface is resistant to junk/slop filling out the sorry's. This is supposed to reduce the number of lines that humans have to read to only a handful, while the full valid AI-generated proof is tens of thousands of lines. The challenge was just solved a couple weeks, here's the discussion about it: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...

[x______________]

>But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me.

Why not just fork the original master branch of human science to an ai-enhanced one and see where that brings us?

[hiAndrewQuinn]

hell yeah brother let's do it

[euroderf]

You might get the Riemann hypothesis robo-proven and unintelligibly dense. Would mathematic professionals trust it, or would they always be putting asterisks next to proofs downstream of it ?

[znkr]

We put asterisks next to proofs that use the axiom of choice. If a machine comes up with proof that’s not verifiable by humans, you can very well be sure that there will be asterisks.

[messe]

But part of the point of mathematics is human understanding. I think most would be willing to accept the proof. They just wouldn't think it's nearly as useful as one that could be understood.

[goalieca]

> Imo, the proved theorem is the API. And that's really all it has to be.

The novel approaches to solving challenging proofs is very useful.

[teiferer]

> Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use:

Here is a other one: hello_world.c versus hello_world.exe (apologies for windows extensions, just for illustration).

One is made by a human for human consumption and extension (though legible by a machine). The source code.

One is made by a machine for a machine. Unreadable by a human. The "binary", though that's a terrible misnomer. (Sure you can disassemble but any nontrivial program is too much to cope with as a whole).

Source vs binary. Both are useful but only one is useful for human consumption.

[dr_dshiv]

Binaries are executed by machines but are not yet understandable by machines. (Now that we live in an era where machines can understand, imperfectly, like us)

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

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

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

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

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

[pfdietz]

Perhaps in the future we'll see golfing of formalized proofs as a valid and valuable form of mathematics, not just proving a theorem for the first time.

Of course there's no reason AI couldn't do that too.

[galaxyLogic]

> Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics.

So why don;t they use AI to write Lean programs? That should make the AI-proofs more readily human undersrndable.

[abdullahkhalids]

Terence Tao talks about this [1]

> In particular, the process of converting a medium-sized Lean document (containing a few thousand lines of code, with some proofs AI-generated) into a nicely golfed and structured Mathlib submission has been an interesting experience. AI agents can be used to perform local golfs that can shave the size of the code somewhat, but global refactoring decisions, such as noticing that a certain argument appears multiple times across the document and can be abstracted into a standalone lemma that can may have additional utility beyond the file, is still largely beyond the reach of current AI tools. (I find that I can explain such a refactor to an AI agent, who can then execute it, but they struggle to spontaneously discover such refactors on their own.)

[1] https://mathstodon.xyz/@tao/116789373239346609

[bckgrndrdtn]

It's a mixed bag. Some people don't use AI, for the usual reasons that people don't use AI. Others have used AI to write Lean programs. For example the 200K loc example mentioned in OP. But generally speaking, the quality isn't good enough yet. And when you've looked at 13 AI-generated examples and found them lacking on various axes compared to Mathlib, then you'll take a break before being motivated to look at example 14.

[UltraSane]

I don't quite understand the objection. The 200,000 line Lean proof can be used in other proofs without needing to understand it. This is the biggest advantage of formally verified proofs.

[bwfan123]

Loved Bessis's book and his writings because of his human-centric view which is missed by the ai maximalists. I just cant wait for the upcoming AI bust to skim the froth in the debate.