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

[indiv0]

That’s a fair point. I wouldn’t want to take machine god’s proclamations on faith either. I’d prefer it if the knowledge was always within our grasp. There is also a possible middle ground where we don’t understand the questions or the answers but we still benefit from the effects of the application of that knowledge. “Sufficiently advanced technology is indistinguishable from magic” and all that. Hopefully we can still judge the results based on the effects. Rejecting a call to genocide should be easy enough, but on the other hand the Native Americans couldn’t foresee what the smallpox blankets would do to them. Working from a position where you are the weaker side of a knowledge gap is a scary thought. It’s a rational fear and I think a lot of people will end up on that side of the divide if AI continues to advance.

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

[skydhash]

It’s like the Hilbert’s problem and the birth of computers. Turing’s paper is like 66 pages, but the most valuable output is the Turing machine which can be explained in a few paragraphs.

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