6 ms·

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theo

• jackyinger 3mo ago
  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.
• rdedev 3mo ago
  Reminded me of this quote: the problem with machine learning is that it's the machine that does the learning
  • smitty1e 3mo ago
    A montage is a fantastic device in a movie. But a montage about weight lifting does not a body builder make.
• slopinthebag 3mo ago
  Reminds me of a quote from Tsoding > “Programming is understanding. If you don't understand what you are doing, you are not programming. You are generating text.” Perhaps a proof without understanding is just generating numbers.
  • nok22kon 3mo ago
    programming is also solving problems in medicine they use all kinds of drugs which they don't really understand how they work. anesthetics is a great example
    • slopinthebag 3mo ago
      By necessity perhaps, but they are desperate to find out why they work so doctors can kill less people. Almost half a million people die each year from medical errors in the USA. Now they have a valid excuse that the human body is incredibly complex and not yet understood. We don’t have that excuse, because we build all of our software from the ground up. If we don’t understand it, that is our fault.
• crystal_revenge 3mo ago
  > but I would like to understand the problem, too But why should it be the case that this is always possible? It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs. In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.
  • zmgsabst 3mo ago
    No, it doesn’t imply that. Just that the set of proofs a human can interpret and the set of statements a human can understand overlap; conversely, you require that the statements/theorems humans can understand be a larger class than the proofs they can understand. To me, it’s not obvious which of those should be true: - can we only understand theorems for which we comprehend their proof? - or can we understand theorems despite not comprehending the proof structure? Within the mathematics community, opinions differ. But you’re elevating your perspective on that question into a law, without any evidence.
    • crystal_revenge 3mo ago
      > understand theorems for which we comprehend I don't know what your distinction between "understand" and "comprehend" but my point was not about these words, but about being "useful" and being "understandable". I'm saying there's no relationship between a mathematical statement being useful and it being understandable. If it is true that "understanding is a prerequisite for usefulness" (where "understanding" means that a statement can be proven in a way that is intelligible to humans) was a property of mathematical expressions, then this fact would certainly be useful (we could exclude any statements that no human understand from the world of useful mathematical expression). But, by that definition, we would need to understand that statement, so you would need to be able to prove that "understanding is a prerequisite for usefulness" in a human intelligible way. Now what I just wrote is in itself not a proof that we can't know, but proving the above statement would involve expressing the claim in a mathematically verifiable way that was also understandable by humans, which does imply something remarkable about human cognition (something that would be intelligible no less!)
    • 3mo ago
• schmuhblaster 3mo ago
  Mathematics has always been an experimental science to some extent. While Newton, Euler and Gauss would spend a lot time calculating numerical approximations by hand, modern mathematicians have been doing the same using computers and software. And once an a clear picture emerge about what’s going, you can start to formalize that and attempt to prove and communicate your results in the standard definition, proposition, lemma, theorem scheme. (Btw there is even a journal called Experimental Mathematics devoted to this approach). I don’t see that LLMs will fundamentally change this, but rather accelerate the speed of mathematical research. Some computer generated proofs might of course be hard to understand, but at least their existence gives another data point work with. Doing Mathematics is more than proving something, that’s just the end of a long road spent pondering at one’s desk about how things could work out.