|
|
|
|
|
|
by staunton
757 days ago
|
|
|
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 |
|
|
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.