I understand that a group of motivated individuals, even without significant financial resources, could attempt to tackle these challenges, much like the way free and open-source software (FOSS) is developed. The key ingredients would be motivation and intelligence, as well as a shared passion for advancing mathematics and solving foundational problems.
Possible but unlikely given how much demand there is and the pressure to deliver returns to shareholders, however sure it is possible. Right now search is very inefficient, the search space is massive. That is the main problem. You can have many sequences of text that sound plausible, but of them a much smaller number will be logically valid. This is the main challenge. Once we can search efficiently not just in semantically valid space but I suppose what you can call syntactically valid space then we will be able to crack this.
