Comment by curt15
4 days ago
Why not use some of the money to develop open-weight, open-training-pipeline, fully introspectable and hackable LLM-based theorem proving assistants? Make them a commodity in every mathematician's office like other computational tools. Such a project would itself yield research topics.
I do seeing this becoming a trend more and more. A lot of open models are fairly strong and fine-tuning and other post-training techniques could easily make bespoke domain-specific inference considerably cheaper (in token usage and energy consumption) and allow for more data sovereignty.