5 ms·
It's hard to know what math is 'useful' a priori. That's always been the argument for supporting basic research. This is not why I am a mathematician however. I
by tacomonstrous 9d ago
It's hard to know what math is 'useful' a priori. That's always been the argument for supporting basic research. This is not why I am a mathematician however. I think there's intrinsic value into understanding something of depth and meaning, but the societal setup we have now that mostly agrees this is valuable is probably a very contingent phenomenon that is unlikely to last much longer.
- a2ff6eeb0 9d agoYes, so if there's useful math, you throw the LLM at it and use the results, no humans needed. Humans can try to extract some ideas from the million line lean proofs, if they want to, I guess. But I can't imagine anyone really funding the human part of it.