It looks like these models work pretty well as natural language search engines and at connecting together dots of disparate things humans haven't done.

▲

pfdietz 9 hours ago | parent | next [-]

They're finding them very effective at literature search, and at autoformalization of human-written proofs.

Pretty soon, this is going to mean the entire historical math literature will be formalized (or, in some cases, found to be in error). Consider the implications of that for training theorem provers.

▲

mlpoknbji 8 hours ago | parent [-]

I think "pretty soon" is a serious overstatement. This does not take into account the difficulty in formalizing definitions and theorem statements. This cannot be done autonomously (or, it can, but there will be serious errors) since there is no way to formalize the "text to lean" process.

What's more, there's almost surely going to turn out to be a large amount of human generated mathematics that's "basically" correct, in the sense that there exists a formal proof that morally fits the arc of the human proof, but there's informal/vague reasoning used (e.g. diagram arguments, etc) that are hard to really formalize, but an expert can use consistently without making a mistake. This will take a long time to formalize, and I expect will require a large amount of human and AI effort.

	▲	pfdietz 3 hours ago \| parent [-]
		It's all up for debate, but personally I feel you're being too pessimistic there. The advances being made are faster than I had expected. The area is one where success will build upon and accelerate success, so I expect the rate of advance to increase and continue increasing. This particular field seems ideal for AI, since verification enables identification of failure at all levels. If the definitions are wrong the theorems won't work and applications elsewhere won't work.

▲

p-e-w 8 hours ago | parent | prev [-]

Every time this topic comes up people compare the LLM to a search engine of some kind.

But as far as we know, the proof it wrote is original. Tao himself noted that it’s very different from the other proof (which was only found now).

That’s so far removed from a “search engine” that the term is essentially nonsense in this context.

	▲	theptip 7 hours ago \| parent [-]
		Hassabis put forth a nice taxonomy of innovation: interpolation, extrapolation, and paradigm shifts. AI is currently great at interpolation, and in some fields (like biology) there seems to be low-hanging fruit for this kind of connect-the-dots exercise. A human would still be considered smart for connecting these dots IMO. AI clearly struggles with extrapolation, at least if the new datum is fully outside the training set. And we will have AGI (if not ASI) if/when AI systems can reliably form new paradigms. It’s a high bar.