Computer-assisted proofs aren't entirely new in mathematics, but the form of assistance we're used to hearing about are either naive (e.g. Four colour theorem) or formal (using proof verification software like Coq or Lean).
I usually don't pay that much attention to developments in AI, however reading about GPT-2 really piqued my attention and got me wondering about a possible third form of computer proof which I shall call generative.
The idea would be to train some kind of general-purpose generative model on a large database of mathematical proofs and see if it were able to generate semblances of correct proofs by feeding it statements as prompts. The resulting text would be the result of something profoundly different to mathematical reasoning as we know it, and instead based on only form and context. Basically 100% "machine intuition" if that makes any sense.
A first obvious caveat is the size of the database: I am unsure that even the entirety of arXiv would large enough to get a workable model.
Secondly, I think such a model would be fundamentally ineffective against any statement that is in the least technical. It would be unrealistic to expect for a machine to generate even a few lines of correct calculation using contextual cues alone. This rules out a large class of theorems and lemmas from those which we might expect our putative model to have a reasonable shot at.
Nonetheless, the idea doesn't seem entirely unpromising as a whole. I feel like a sufficiently-trained model should have a reasonable chance at a certain class of non-technical, but non-trivial theorems. Obviously nothing close to cutting-edge (it would be absurd to expect such a model to reason about perfectoid spaces) but still strong enough to potentially teach us something new, like a link between two things that was never noticed, or a simplification of an otherwise complicated proof. Kind of like how AlphaGo taught chess players something new (IIRC some line of some opening had been considered losing in modern play, but then AlphaGo used it and showed that it could provide a decisive advantage 20+ moves in).
Has such a work been attempted, or theorised? To those with experience of knowledge on the subject, to what extend is this flawed or otherwise unrealistic?
[link] [comments]
from math https://ift.tt/3f3ohko
Post a Comment