AI is now celebrated for producing long chains of logical deductions establishing mathematical theorems, with every step formally verified by a computer. This is presented as a breakthrough in mathematical intelligence.
But what exactly has been achieved?
A formal proof is a finite sequence of logical operations leading from accepted axioms to a theorem. A numerical computation is likewise a finite sequence of operations, but leading to an approximate solution of a given equation.
There is a fundamental difference in how the results can be verified.
Consider the equation
F(u) = 0.
A numerical computation produces an approximation uh, which can be inserted into the equation to compute the residual
r = F(uh).
If the residual is small and the problem is suitably stable, the computed solution can be certified as accurate. The result can thus be checked independently of the procedure used to obtain it.
By contrast, a formal proof of a theorem P is verified by checking the logical steps leading to P. There is generally no direct test of the theorem itself independent of mathematical reasoning.
A numerical computation can produce an answer that speaks for itself through a residual and stability estimate. A formal proof speaks through its chain of deductions.
The distinction becomes particularly striking when a theorem asserts the existence of a mathematical object without constructing it. A million formally correct logical steps may establish that something exists without telling us what it is or how to compute it.
This is possible because classical logic accepts the law of excluded middle, allowing existence to be established indirectly without producing a witness.
Formal verification does not eliminate this nonconstructivity. It merely certifies that the logical deductions are valid.
The Clay Navier–Stokes problem illustrates the issue. A formally verified proof of global regularity or finite-time breakdown could settle the Millennium Problem without providing a method for computing turbulent fluid motion with controlled error and stability.
One achievement would concern abstract mathematical regularity; the other would concern predictive fluid mechanics.
Which is more important for science?
The current enthusiasm for AI theorem proving risks confusing the mechanical verification of logical deductions with the construction of new mathematical knowledge about the world.
This suggests a different direction for AI mathematics:
Instead of asking AI merely to prove that solutions exist, ask it to construct solutions whose accuracy can be independently certified.
Such a shift would connect formal reasoning with computation, stability and physical prediction.
The ultimate test of mathematical intelligence may not be the ability to produce a million correct logical steps, but the ability to produce a solution that can be checked without retracing those steps.
Is AI mathematics going to become an industry producing formally certified existence theorems, or a science producing computable and verifiable solutions?
Inga kommentarer:
Skicka en kommentar