5 ms·

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

seanmcc 3mo ago
Almost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.
- therobots927 3mo ago
  So… more peer review backlog. That sounds fun. Oh, you want someone to review your paper, Mr phd in mathematics with 20 years of experience? Get in line behind chatGPT.
- wbl 3mo ago
  Look up the story of Flyspeck for this taking an entire career.
avaer 3mo ago
As a programmer I definitely get annoyed when I see code and I don't understand what it does. But I also definitely don't understand the problem if I can't get the computer to understand it, with tests. In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. With all of these questions in the air, epistemology might be making a comeback.
- therobots927 3mo ago
  Tests only work for a limited set of programming verification. In many cases you don’t actually know what the output for any given input should be, so there’s no way of verifying the AI-generated code. You just kind of have to trust it. The only exception I can think of is robotics and quantitative trading. Which have already been extensively utilizing AI.
  - subscribed 3mo ago
    That's a very handwavy way of saying no. I disagree, software engineering is a mature discipline now, and at this point we have so many testing frameworks (unit testing, syntax testing, regression testing, fuzzing, testing end to end, live, with a subset of known good and incorrect inputs, chaos monkeys, etc, etc, that to say "there's no way of verifying the AI-generated code" is frankly incorrect. Or, if you insist, defend the "there's no way of verifying the code, at all", and not only AI-generated. (if it helps I work in the company where before the code even starts being written, several extensive tests for it must be ready first. It's hard to even commit a broken code, and later in the pipeline it's very easy to catch the subtly broken or incorrect code)
- godelski 3mo ago
  > In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify
  - zmgsabst 3mo ago
    That depends on who you ask. Type theory can also be an independent synthetic foundation atop which you build mathematics.
    - godelski 3mo ago
      You can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know how to be bridged between entire subfields. So I'd be impressed if type theory really could do everything, but hey, I don't know
akoboldfrying 3mo ago
Well, if you can formalise the problem statement (this is the hard part) sufficiently well that the computer can produce a proof, you can be very sure the proof is sound. A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the truth of which has already been established. So while coming up with a proof may require genius-level thinking, checking an existing fully fleshed out proof is simple -- just potentially very tedious because of the sheer number of steps. That said, a typical human-written proof omits many steps considered "obvious" to a trained mathematician. Converting this to a formal proof involves interpreting what the original author "must have meant", which requires a lot of expertise and can go wrong -- or it may reveal that there is some inconsistency in the original claim itself.
- bsder 3mo ago
  > checking an existing fully fleshed out proof is simple The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.
  - akoboldfrying 3mo ago
    How does this involve computer checking of a formal proof? Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs. ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.
  - pfdietz 3mo ago
    His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed. This is one of the great things about formalization: it would have avoided this entire debacle.
kimjune01 3mo ago
lean compiles or it doesnt
- whattheheckheck 3mo ago
  You can also pass pytest with assert 1 = 1...
  - pfdietz 3mo ago
    There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.
    - tripzilch 3mo ago
      Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.
      - pfdietz 3mo ago
        > wouldn't there be a way to hide such cheats in it? No.

seanmcc 3mo ago

Almost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.

therobots927 3mo ago
So… more peer review backlog. That sounds fun. Oh, you want someone to review your paper, Mr phd in mathematics with 20 years of experience? Get in line behind chatGPT.
wbl 3mo ago
Look up the story of Flyspeck for this taking an entire career.

avaer 3mo ago

As a programmer I definitely get annoyed when I see code and I don't understand what it does. But I also definitely don't understand the problem if I can't get the computer to understand it, with tests. In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. With all of these questions in the air, epistemology might be making a comeback.

therobots927 3mo ago
Tests only work for a limited set of programming verification. In many cases you don’t actually know what the output for any given input should be, so there’s no way of verifying the AI-generated code. You just kind of have to trust it. The only exception I can think of is robotics and quantitative trading. Which have already been extensively utilizing AI.
- subscribed 3mo ago
  That's a very handwavy way of saying no. I disagree, software engineering is a mature discipline now, and at this point we have so many testing frameworks (unit testing, syntax testing, regression testing, fuzzing, testing end to end, live, with a subset of known good and incorrect inputs, chaos monkeys, etc, etc, that to say "there's no way of verifying the AI-generated code" is frankly incorrect. Or, if you insist, defend the "there's no way of verifying the code, at all", and not only AI-generated. (if it helps I work in the company where before the code even starts being written, several extensive tests for it must be ready first. It's hard to even commit a broken code, and later in the pipeline it's very easy to catch the subtly broken or incorrect code)
godelski 3mo ago
> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify
- zmgsabst 3mo ago
  That depends on who you ask. Type theory can also be an independent synthetic foundation atop which you build mathematics.
  - godelski 3mo ago
    You can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know how to be bridged between entire subfields. So I'd be impressed if type theory really could do everything, but hey, I don't know

akoboldfrying 3mo ago

Well, if you can formalise the problem statement (this is the hard part) sufficiently well that the computer can produce a proof, you can be very sure the proof is sound. A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the truth of which has already been established. So while coming up with a proof may require genius-level thinking, checking an existing fully fleshed out proof is simple -- just potentially very tedious because of the sheer number of steps. That said, a typical human-written proof omits many steps considered "obvious" to a trained mathematician. Converting this to a formal proof involves interpreting what the original author "must have meant", which requires a lot of expertise and can go wrong -- or it may reveal that there is some inconsistency in the original claim itself.

bsder 3mo ago
> checking an existing fully fleshed out proof is simple The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.
- akoboldfrying 3mo ago
  How does this involve computer checking of a formal proof? Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs. ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.
- pfdietz 3mo ago
  His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed. This is one of the great things about formalization: it would have avoided this entire debacle.

kimjune01 3mo ago

lean compiles or it doesnt

whattheheckheck 3mo ago
You can also pass pytest with assert 1 = 1...
- pfdietz 3mo ago
  There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.
  - tripzilch 3mo ago
    Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.
    - pfdietz 3mo ago
      > wouldn't there be a way to hide such cheats in it? No.