I have a lot of thoughts about this topic and about what a good proof assistant for pure mathematics would look like, most of which don't fit the scope of this question, but I'd like to respond to both your actual question and what I see as an implicit assumption in your question.
Your primary question is a little bit difficult to answer because it depends on what 'seriously' means. Is it merely sufficient for the organization providing the alternative to be serious, or does it need to be a meaningfully viable alternative in the sense of attracting an active community? If intent is sufficient, then Prove-It (which is in part developed by researchers at Sandia National Laboratories) is already a positive answer. If you also require some amount of actual activity with the proof assistant, then Mizar might qualify. Let me know if I'm wrong, but I think your question is really intended to be more like 'could an organization support an alternative to Lean that captures a meaningful mind share among mathematicians?'
User experience and money
I think that a successful alternative is possible, but I think foundations are not really the operant issue. Part of the reason Lean took off is that it had enough money behind it to have better (although, I still maintain, meaningfully bad) user experience than the other major offerings. Annoying foundational considerations do bubble up to the user experience of working with a proof assistant (even in the context of type theory, despite what some people seem to think), but the majority of the usability of a proof assistant has to do with the existence of well-designed libraries and more pedestrian user experience issues like how annoying it is to install, how responsive it is in the editor, good autocomplete, good tutorials or other on-boarding, etc. I said in a comment on your question that the amount of community effort that has been put into the Mathlib ecosystem could have built a better pure math proof assistant, but I think I misphrased that. At some scale you really need some kind of institutional (and therefore monetary) support for this kind of project. (Although Mathlib does have institutional support separate from Lean these days, so my comment doesn't overstep if you include this in 'community effort'.) For example, the Lean FRO also hosts an online Lean editor. This makes it easy to dabble in Lean. (I've heard that some people do all of their Lean work in that web editor.) But the Lean frontend is probably a little bit too bloated to run smoothly in-browser, so when you use this website, the Lean FRO runs a copy of Lean on their server for free. This costs money.
Someone is certainly going to get mad at me for saying this, but Isabelle is the only other major proof assistant that in my opinion has made a reasonable effort towards good user experience. That said, their answer (a pre-packaged modified version of jEdit) is by modern standards a bit clunky and dated. I personally (for accessibility reasons) was annoyed by the lack of compatible dark mode support in jEdit, for instance. Beyond this, the formal system of Isabelle/HOL itself suffers from things like a frankly confusing object theory/metatheory distinction that the user is supposed to be shielded from but is nevertheless exposed to often (at least in my experience). Isabelle has a VSCode plugin now, but it seemed to lack polish the last time I looked at it. As far as I can tell, Isabelle doesn't have full-time developers whose whole job is building and maintaining the program, which Lean does. Good full-time developers, again, cost a lot of money.
So I feel like this makes the case that money and a full-time development team are pretty essential for building a proof assistant with good, well-maintained user experience. I think that the most plausible structure for such a project would be something similar to the Lean FRO, CoCalc, or Overleaf, an organization focused explicitly on developing a proof assistant for mathematics rather than software development. This could be bankrolled by an existing organization, sure, but I don't think just giving a couple of individual academics grants would be enough.
Foundations
As you mention in your question, Lean (i.e., the "truth machine" as it has been eye-rollingly dubbed recently) just had a widely publicized kernel soundness bug. The soundness issue involved a feature of Lean that Mario Carneiro's proof of the consistency of the idealized type theory of Lean did not cover (i.e., nested inductive types). Nevertheless, I'm not sure I actually think this is a case for basing a proof assistant on set theory in particular, at least not in a user-facing way. The idea that basing a proof assistant on set theory is the right solution to this issue seems to be an implicit assumption of your question. More broadly, there's a deeper implicit assumption in this whole discourse that proof assistants should be primarily judged on the basis of their foundational systems.
To me, thinking about proof assistants in a foundational way, building the user experience from the ground up, is fundamentally wrongheaded. My ideal actually-for-mathematicians proof assistant would be built from the top down. (I think you could do this while still building a soundness architecture that compiles down to something an extremely minimal Metamath-like kernel could check.) For example, Mathlib's category theory library is notoriously awful to use because it runs into all this obnoxious bureaucracy involving managing definitional equality, universes, transport, coherence, and typeclass inference. (Consider for example, the mathematically trivial bookkeeping lemma CategoryTheory.shiftFunctorAdd'_assoc, whose theorem statement is so complicated it contains two inline proof scripts.) Having a smooth user experience for category theory would be a fundamental design goal of my ideal proof assistant, because category theory is a fundamental tool in many parts of mathematics. This would be important enough to potentially motivate very low-level changes to the implementation of the system. But I also wouldn't use categorical foundations because (and, again, someone is going to get mad at me for saying this), categorical foundations are actually pretty bad and difficult to use in practice. Foundationalism makes sense if your goal is industrially paranoid rigor or if your goal is to philosophically ground the semantics of mathematics or to prove metamathematical unprovability results; it doesn't make sense as a UX organizational principle if your goal is to actually do mathematics on a computer.