Post #2525138

@PSL2Z@mathstodon.xyz fwiw "Richard Borcherds: This focus on problems that you can calculate an answer to is a bit misguided, since most mathematics research is not actually about that at all. I’d be much more impressed if you could switch to having your model produce proofs that can be checked in Lean as an answer, rather than just calculating something which half the time it just seems to guess." I'm interested in actual mathematics research. My own has only once led me to calculate a numerical function (turned out to be constant at 1, thankfully) and once I calculated a number to point out a mistake in the literature (some number should have always vanished, and I found some input where the result was positive). So I guess Borcherds was in the discussion, but slightly nonplussed. But again, I'm hoping for more involvement at the research level. I think Hairer is a better example of someone engaging seriously.