|
Well, as a computer scientist, I'd urge them to reconsider. :) My intuition is that, given a sufficiently formalized system, computers can help them achieve their goal of understanding and discovering more math, much more rapidly and with compounding effects. Although perhaps there is a risk that any mathematics the computer might "discover" would become increasingly incomprehensible to human mathematicians, in which case the discoveries wouldn't be worth much. I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable? Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world. But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics? |