[pfdietz]

At some point the effort shifts from proof of concept to exploration of impact. Of course doing proving at large scale provides further feedback for improving the AIs. Visual reasoning, for example, may still need work.

The big impact will be with scaling, for example complete autoformalization of existing math, and automatic exploration for new conjectures, with emphasis on how interesting they are. Automatic conjecture generation goes way way back, to the days of Lenat's AM system. Modern AI should do a far better job.