On: AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems

I think you're missing my point. It's that once the workbooks are completely interpreted, which is happening at an accelerated pace thanks to AI, von Plato's value as an interpreter of the short hand becomes severely reduced, presumably as does his ability to get future grants.

I'd think there would be more competition to lead studies and receive grants now that the workbooks are accessible to a wider audience of logicians

If he was facing mandatory retirement nearly ten years ago it’s likely he might be ready for voluntary retirement, particularly after achieving this fantastic result.

Indeed, he is 75 years old.

I would his not be in verifying the AI is output?