It is a strange state of affairs that very good and renowned mathematicians are expressing rather ignorant, superficial or just plain wrong views about the value of AI in mathematics. These seem to be mathematicians with evidently no technical background in mathematical logic, type theory, computer science or the foundations and philosophy of mathematics.
More intelligent views are expressed by computer scientists and by expert coders.
What is needed is an illuminating and simple way of explaining what is going on.
Suppose we wanted to write a program in a high-level language to perform a certain task.
A mathematician is like the human coder who writes in this high-level language.
The Lean proof-assistant is like a program that given a binary executable file and description of a task tells you if the program performs the task or not.
AI generated mathematics is about generating binary executable files and checking if they perform a given task.
How are they generated? This could be done using models trained on human high-level code using processes involving compiling and task-checking. Or it could be by some brute force or heuristic guided low-level or high-level search (again using compiling and task-checking).
If the generated code is checked for the task, the code is still totally opaque - it has no necessary connection to any high-level language. Also, it is not guaranteed to be the most efficient or elegant way to perform the task.
A further program may attempt to reverse engineer the code into a high-level language, but this will, in general, be both unreadable and useless.
AI generated proofs may tell you that a theorem is true or not (in a given system), but not why or how it is true or what is the best theory or framework to prove it in.
AI generated math is, in the end, largely a combination of low-level non-optimal brute force proof search and plagiarism of human work.
Why any self-respecting mathematician could call this "being good at math" or confuse serious proof-assistant based methods with standard generative AI plagiarism and slop, is beyond me.
By the way, there is at present no freely available generative AI that can come near to "doing the homework" of advanced graduate work in mathematics or philosophy: the quality of the output is a function of the quantity (and specific kind of statistical distribution) of material available relating to a given specialized technical area (as well as quality, selectivity, bias and so forth).
Perhaps the problem with the opinions of people like Richard Borcherds is that they think their particular areas (saturated and thus eminently machine-learnable) are the center of the world of mathematics, when in reality they are drops in the ocean of possible mathematics.
That is, perhaps, why they are trying to shut down or restrict university libraries. They do not want people to see and explore new horizons, dig up buried treasures and come face-to-face with reality.
One last but very important addition to the post below. The analogy between human mathematics and Lean formalizations on one hand and high-level coding and binary executables collapses however in regarding certain fundamental aspects.
There is no adequate, reliable and robust way to automatically "compile" human mathematics into Lean formalizations. In fact, even the theoretical foundations for such a process are lacking. On the other hand, there is also no adequate way to "reverse engineer" Lean formalizations into human readable mathematics employing high-level conceptual architecture. A corollary is that there is absolute no trustworthy way of automatically determining if a human mathematics paper corresponds correctly and exactly to a Lean formalization (and in general this may be a many-to-many correspondence).
So what AI mathematics gives us is basically two monstruous, useless and not necessarily related things.
1. An unreadable opaque code with a probable truth claim regarding a proposition whose value is still dependent (among other things) on the type theoretic soundness, formalization decisions in the library and implementation issues of Lean.
2. A huge unreadable dubious natural language based paper not necessarily related to the opaque Lean code which does not only require peer-review but a huge amount of previous reworking, simplification and improvement by mathematicians (assuming that the paper has any value at all).
I suggest that while 1) may have interest in motivating mathematicians to find an intelligent and elegant proof of the theorem in question, 2) has very little value.
No comments:
Post a Comment