[flagged]
AI in mathematics is forcing big questions
21–30 of 193 posts
Re: AI in mathematics is forcing big questions
#22Re: AI in mathematics is forcing big questions
#23It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it.
It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify the correctness. One hallucination in 300 steps of logic is enough to destroy the entire proof.
Re: AI in mathematics is forcing big questions
#24Earlier quoted context omitted.
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.
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.
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.
Re: AI in mathematics is forcing big questions
#25Earlier quoted context omitted.
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.
Almost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.
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.
Re: AI in mathematics is forcing big questions
#26Human mathematicians could become “priests to oracles.” Priests were interpreting the oracles (at least at a place like Delphi) according to the context of the people asking the questions aka participating in politics of that ancient times. Subjectivity was a feature and I’m not sure that fits to mathematics though. I wonder if mathematics as a science field moves more into engineering or if a different branch will e…
Human mathematicians could become “priests to oracles.”
This is a decidedly anti-enlightenment statement.
Re: AI in mathematics is forcing big questions
#27[flagged]
Re: AI in mathematics is forcing big questions
#28It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify th…
I would imagine that in the future AI will be doing proofs in Lean or whatever the successor to it, which gives you a pretty good confidence it’s correct.
Re: AI in mathematics is forcing big questions
#29The 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 theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…
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.
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.
Re: AI in mathematics is forcing big questions
#30It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify th…
> It would be great if someone could explain to me how AI improves this situation.
It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean.
> One hallucination in 300 steps of logic is enough to destroy the entire proof.
The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.