I feel kind of bitter about this, because a whole team of people whose mathematical work has been very inspiring and enlightening to me has pivoted to working on “autoformalisation” — in other words, “messing around with the computer and begging it to keep working”. I am not saying that it's impossible for anything of value to come from that work. I am saying that it is a huge social waste for some of our most brilliant researchers to be working on such things… From them, I want more novel mathematics, more brilliant textbooks, more community-oriented proof libraries! I am not blaming people for the fact that funding for doing almost anything else is scarce… You have to survive. I'm just sad about it.