4 ms·

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 an

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.

messe 4mo ago
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.
mittensc 4mo ago
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_ 4mo ago
  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.
  - fdupress 4mo ago
    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.
  - crote 4mo ago
    > 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 4mo ago
      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.
    - _zoltan_ 4mo ago
      I just wanted to commend you on this analogy. Very nice. Thank you!
x______________ 4mo ago
>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 4mo ago
  hell yeah brother let's do it
TheOtherHobbes 4mo ago
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 4mo ago
  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.
  - crote 4mo ago
    > 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.
    - hiAndrewQuinn 4mo ago
      "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.
ben_w 4mo ago
> 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 4mo ago
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 4mo ago
  > These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.
  - Diogenesian 4mo ago
    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/main/JunkTheorems.lean 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 4mo ago
      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/778bc714030b3e974ab5f4038783d1a9 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-Autoformalization/topic/Jacobian.20challenge/near/586351734 https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...
goalieca 4mo ago
> 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.
bckgrndrdtn 4mo ago
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 4mo ago
  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?
euroderf 4mo ago
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 4mo ago
  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.
YeGoblynQueenne 4mo ago
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?

messe 4mo ago

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.

mittensc 4mo ago

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_ 4mo ago
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.
- fdupress 4mo ago
  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.
- crote 4mo ago
  > 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 4mo ago
    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.
  - _zoltan_ 4mo ago
    I just wanted to commend you on this analogy. Very nice. Thank you!

x______________ 4mo ago

>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 4mo ago
hell yeah brother let's do it

TheOtherHobbes 4mo ago

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 4mo ago
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.
- crote 4mo ago
  > 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.
  - hiAndrewQuinn 4mo ago
    "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.

ben_w 4mo ago

> 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 4mo ago

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 4mo ago
> These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.
- Diogenesian 4mo ago
  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/main/JunkTheorems.lean 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 4mo ago
    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/778bc714030b3e974ab5f4038783d1a9 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-Autoformalization/topic/Jacobian.20challenge/near/586351734 https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...

goalieca 4mo ago

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

bckgrndrdtn 4mo ago

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 4mo ago
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?

euroderf 4mo ago

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 4mo ago
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.

YeGoblynQueenne 4mo ago

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?