I could iterate with an LLM and Lean, and generate an unlimited amount of logic (or any other kind of math). This math would be correct, but it would almost surely be useless. For this reason, neither computer programs nor grad students are rewarded simply for generating logically correct math. They're instead expected to prove a theorem that other people have tried and failed to prove, or perhaps to make a conjecture with a form not obvious to others. The former is clearly an achievement, and the latter is a falsifiable prediction.

I feel like Norvig is coming from that standpoint of solving problems well-known to be difficult. This has the benefit that it's relatively easy to reach consensus on what's difficult--you can't claim something's easy if you can't do it, and you can't claim it's hard if someone else can. This makes it harder to waste your life on an internally consistent but useless sidetrack, as you might even agree (?) Chomsky has.

You, Chomsky, and Pearl seem to reject that worldview, instead believing the path to an important truth lies entirely within your and your collaborators' own minds. I believe that's consistent with the ancient philosophers. Such beliefs seem to me halfway to religious faith, accepting external feedback on logical consistency, but rejecting external evidence on the utility of the path. That doesn't make them necessarily bad--lots of people have done things I consider good in service of religions I don't believe in--but it makes them pretty hard to argue with.