An AGI is often claimed to be a general purpose problem solver and these are exactly the types of problems that a general purpose problem solver would be able to solve if given access to a mathematical library. All existing LLMs have been trained on abstract mathematics and logic but it is obvious that they are incapable of abstract logical reasoning, e.g. solving sudoku puzzles.
Here is my prediction, FWIW: the hard part of the problem has already been solved, in the following technical sense: there is a few 1000 lines program that has not been invented yet, but it will be invented soon, that loads a current LLM model, runs fast on current hardware, and you will deem it to be an AGI. In other words, the conditional Kolmogorov complexity of undisputable AGI given the Llama weights is only a few 1000 bytes. We are at the pre-AlphaGo, post Clark-Storkey stage of reasoning. That's my guess, anyway.
I think you are likely right but coming up with that final inference strategy is still "the hard part" IMO. Not in terms of computation, but in terms of algorith development.
99.9% of the population would not be able to solve these problems given a year and access to every piece of mathematical literature ever written (except the solutions to these problems of course).
Saying that you need to solve these to be considered AGI is ridiculously strict.