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...
