943 words
Apocryphally, Fodor said of interdisciplinary work that it was only worth doing in one person’s head. (I don’t have a source for this, but I think it is true that he said this apocryphally, and he probably said something less bold and therefore ridiculous.) Indeed, although my research interests are nominally interdisciplinary, I am convinced that what I enjoy thinking about is really one discipline: pedantry.
Yesterday, OpenAI released a long list of results proved using an internal model. There are good questions about whether, for instance, some of the results are afflicted by erroneous definitions or kernel soundness.1
Note
I shall explain what I mean here for a popular audience in more detail. Many of these results were proved using systems that mechanise mathematics called theorem provers. A theorem prover works by computationally verifying inferential steps from one mathematical claim to another, in accordance with underlying logical rules. A simple one (not specific to mathematics) is modus ponens: we may infer from the propositions that if A then B and that A that B. It is possible to make a mistake in writing the code of the theorem prover. This allows the theorem prover to make illicit steps from one mathematical proposition to another that should not have been accepted. If it does this, the results claimed on the basis of a mechanised proof may be wrong, and the proof may be unsound.
A related problem is that of erroneous definition. Mathematicians prove results about objects that they have defined (e.g. sets, vector spaces, categories and so on). We need to define these objects in theorem provers. Sometimes, we define them somewhat idiosyncratically. As Kevin Buzzard (Division by zero in type theory) explains, there’s nothing inherently illicit about this. The problem arises with severely nested definitions (e.g. fifth- or tenth-level definitions). Somewhere, you might make a mistake, unless you are being very careful. If so, a result that seems to be about categories or vector spaces might not in fact concern them at all. This is another source of error.
I am not competent to comment on such questions in fine. However, I think it is reasonable to conclude that we are close to or have already mechanised a large proportion of mathematics previously reserved only to humans. This could have interesting implications for applied mathematics.
There are many areas of intellectual endeavour in which mathematical competence is an important limiting factor. In analytic philosophy (the field I know best), many—from graduate students to full professors—will occasionally find that they wish they knew more mathematics—e.g. category theory, or higher-order logic or more probability. The same is true in, for instance, economics, physics and theoretical computer science.
It might be hoped that the mechanisation of mathematics will also be its democratisation. Those with the requisite philosophical imagination will be able to summon proofs in the appropriate formalism without their having to spend time in tedious graduate classes. Economists will be free to experiment without their having to worry about the niceties of measure-theoretic statistics. And so on. The effect would be similar to that of democratisation of access to calculators or slide rules. One doesn’t need to be a mathematical savant capable of multiplying large numbers in one’s head to make use of a calculator.
I conjecture that this democratising effect will be very limited in scale, for two reasons. First, much of the conceptual apparatus of these fields is itself highly mathematised. One might want to throw out the sort of formalised metaphysics that can be found in modern analytic journals; but in significant segments thereof, to participate and to actually advance the field, one must know some higher-order modal logic. One simply will not know where to start—let alone how to instruct a model—without minimal and irreducibly mathematised knowledge of the formalisms of the field.
Second, the combination of an human who knows some metaphysics (but not mathematics) with a machine that knows mathematics (but not metaphysics) will not in fact be competent mathematised metaphysics, but what is popularly known as slop. Small or large infelicities will creep in, and the resultant mathematised results will be useless or misleading.
If I am correct, models will democratise adjacent fields only to the extent that they democratise the fields themselves, rather than simply mathematics. Therefore, if these fields are more difficult to mechanise than mathematics, mathematicians’ abilities will remain of use in directing the applied mechanisation of mathematics (in e.g. philosophy, physics and so on). Models good at maths may accelerate progress in fields that apply mathematics, but will not ipso facto democratise them. This admittedly unstable position may itself only be an interlude, followed by a longer period in which machines are better than us at all fields of intellectual endeavour. I have long learned not to make predictions in that connexion.
A further speculative note. Once upon a time, there may have been a certain disciplinarily specific art to arithmetic. Now, access to computerised arithmetic is democratised. Nobody needs to know about specifically arithmetic minutiæ to make good use of a computer to do arithmetic in their field. What about pure mathematics? My suspicion—and this is a mere guess—is that pure mathematics will not be analogous to arithmetic. There will remain value in the intuitions of pure mathematicians about the organisation of the vast tapestry of possible and actual mathematical results and the direction of efforts to that end, both instrumentally and otherwise. That is: an ecosystem in which pure mathematicians are permitted to direct some proportion of research in search of elegance is an ecosystem that even on instrumental grounds will produce more industrially useful mathematics than in the counterfactual.
References
Buzzard, Kevin, Division by zero in type theory: Division by zero in type theory: a FAQ, Xena, 2020. |