It’s depressing to see people you admire pessimistic about the future of science, maths and proof assistants globally. I used to be optimistic, but tonight, after a day spent at slowly hand proving lemmas in mathcomp in between meetings, it’s a bit more difficult.