6 ms·

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

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-economy https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...

crystal_revenge 4mo ago
> 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.
- zmgsabst 4mo ago
  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 4mo ago
    > 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)
    - whattheheckheck 4mo ago
      And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
    - zmgsabst 4mo ago
      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.
      - sdenton4 4mo ago
        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?
        VBprogrammer 4mo ago
- teiferer 4mo ago
  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.
- bckgrndrdtn 4mo ago
  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.
- tripzilch 4mo ago
  > "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!?!?!" I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.
galaxyLogic 4mo ago
> 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.
- bckgrndrdtn 4mo ago
  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.
- abdullahkhalids 4mo ago
  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 https://mathstodon.xyz/@tao/116789373239346609
teiferer 4mo ago
> 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 4mo ago
  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)
hiAndrewQuinn 4mo ago
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.
pfdietz 4mo ago
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.
bwfan123 4mo ago
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.
UltraSane 4mo ago
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.

crystal_revenge 4mo ago

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

zmgsabst 4mo ago
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 4mo ago
  > 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)
  - whattheheckheck 4mo ago
    And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece. Reasoning by analogy...
  - zmgsabst 4mo ago
    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.
    - sdenton4 4mo ago
      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?
      - VBprogrammer 4mo ago
teiferer 4mo ago
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.
bckgrndrdtn 4mo ago
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.
tripzilch 4mo ago
> "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!?!?!" I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.

galaxyLogic 4mo ago

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

bckgrndrdtn 4mo ago
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.
abdullahkhalids 4mo ago
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 https://mathstodon.xyz/@tao/116789373239346609

teiferer 4mo ago

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

hiAndrewQuinn 4mo ago

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.

pfdietz 4mo ago

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.

bwfan123 4mo ago

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.

UltraSane 4mo ago

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.