[ADeerAppeared]

> However, by itself, it seems like this capability wouldn't be very useful, commercially for example.

Quite the opposite, it's the holy grail of all AI.

Consider various work that isn't (and can't) be done by computers/robots/etc right now.

The intelligence constraint is universally, a required amount of problem solving. Even the "low skill" labour requires it.

And to perform such problem solving, you need advanced logic and reasoning capabilities, which is the same thing as novel mathematics, just applied to a different end.

[staunton]

Let's be a little more concrete: do you think FormalGeo [1] is a big deal? I think it's very cool but ultimately not useful in and of itself. It's only useful insofar as it shows AI capabilities advancing in general.

Let's suppose we had an AI that works roughly like [1] but for the kind of mathematics done in Lean's Mathlib, and that was on par or better than humans working on it. Would that AI by itself be commercially useful?

Again, of course having such an AI implies a major jump in capabilities and it would most likely mean useful AI can be trained with similar techniques. But that's not what I mean by the system itself being useful. If all you're saying is that such an AI demonstates we can now probably build AIs that do things which we usually say require "logic and reasoning abilities", I completely agree.

Maybe I'm splitting hairs too much here. However, it could well be that such an AI would be useful by itself. I just can't think of much besides a major advance in the formal software verification niche, which still almost nobody would use...

[1]: https://github.com/FormalGeo/FormalGeo

[ADeerAppeared]

> I just can't think of much besides a major advance in the formal software verification niche, which still almost nobody would use...

The reason is slightly different here.

What's so desirable here is an AI system with such general intelligence that it is capable of such mathematics by itself as a consequence. Not because the mathematics is so useful, but because the required reasoning capabilities are at such a level that, we could speak of an artificial intelligence that is meaningfully "general" about any problem.

It's a decent approximation of "able to solve any problem" that we can still reasonably test.

> Let's be a little more concrete: do you think FormalGeo [1] is a big deal?

It looks to be an interesting approach in modelling mathematics, and their use of machine learning is an interesting novelty that may pave the way to more useful general mathematics systems, but I can't find much about how these systems might interop with current/'generative' AI systems.

And that last bit is one of the big roadblocks for current AI. They're very weak at reasoning, but we can't directly interop to (e.g.) LLMs, so we can't compensate for that weakness.