I'm disappointed in the maths community but not regretting my decision to avoid taking maths as a major. This is remarkably in line with the mentality cultivated by the typical maths department and must be a frustrating daily experience.
If you ever reopen the topic with your colleagues, an interesting starting point might be their thoughts on theorem 14 from this suite; in my opinion, Lean 4 is clearly untrustable. The lack of awareness of this issue seems to stem from the same blind spot that leads to lack of awareness of non-mathematical cognition: whaddaya mean it doesn't all reduce to one particular pile of symbols which all fit together perfectly?