[ykonstant]

It's truly miserable and I share your sentiments completely. Unfortunately, I do not have the right words to express my sadness about the status quo; I am a mathematician who actually believes in the importance of the "mathematics edifice" as a service for society, present and future. Oh well.

[chongli]

I don’t know if it’s recency bias or some other cognitive distortion on my part but I seem to be seeing more and more stories about Lean and formalizing mathematics recently. Perhaps the project is gaining some momentum!