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 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 understanding. I like this one quote by (allegedly) Wigner that illustrates it well:
"It is nice to know that the computer understands the problem, but I would like to understand the problem, too."
The article poses if AI will be a tool, a collaborator or an oracle. Why not all 3?
If mathematics is human understanding of logical consequences, understanding is the priority. But if AI proves something we can't understand but can utilize, that is a different sort of useful.
We are getting awfully close to "the answer of the universe is 42" and having it not be a joke...
I don’t know about “close”,
but there are certainly results in math that are considered deep because they require the use of a “Hard Theorem” at some point. That kind of building on top of something Very Difficult is still possible without understanding the “Very Difficult” part. I’d say a lot of not-amazing math is built by believing the platform works but not being able to built it yourself.
I couldn’t build an internal combustion engine or even a plastic box, so maybe there’s nothing wrong with this approach.
It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very expensive and propitiatory. They are not like the commercial AI that regular people use. It takes considerable prompting and trial an error to solve even Olympiad/Putnam problems, and tons of work by humans pouring over the results to see if it's correct. For every Erdos problem that captures the headlines, there are many where it failed or untold hours of prompting and token burn to get that result, and manhours verify it.
I don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN.
You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.
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 understanding. I like this one quote by (allegedly) Wigner that illustrates it well:
"It is nice to know that the computer understands the problem, but I would like to understand the problem, too."
If mathematics is human understanding of logical consequences, understanding is the priority. But if AI proves something we can't understand but can utilize, that is a different sort of useful.
We are getting awfully close to "the answer of the universe is 42" and having it not be a joke...
I couldn’t build an internal combustion engine or even a plastic box, so maybe there’s nothing wrong with this approach.
You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.
(edit: lol didn't realize the sibling comment below is essentially my comment)
Would some one with tokens to burn mind checking that statement out and post back. Be sure to use long dashes too.