I think one has to be a bit careful here. I wouldn't say the primary users of proof assistants would self identify as mathematicians. I think many use proof assistants for software and hardware verification. And even those looking to formalize mathematics would identify as a mix of undergraduates, hobbyists, computer scientists, philosophers, mathematicians, and other professionals. I think proof assistants have very low visibility to mathematicians (especially outside of logic), but it is increasing every year, with prominent mathematicians like Tom Hales, Vladimir Voevodsky, Kevin Buzzard, Sébastien Gouëzel, and Peter Scholze popularizing them. In particular, Kevin's talk at ICM 2022 goes a long way to making the greater community aware of what is going on.
So that is to say that the numbers you are asking for are going to be quite low probably, and I'm not sure they are even the "right questions". But having said that, one thing to look for is the various MSC Classification Codes which relate to proof assistants. For example, zbMath shows 1069 documents with code 68V15 and 366 documents with code 68V20. Of course, these are self-selected and ambiguous, so you will have many false positives. You can also search for the names of the various provers. There are 16 papers on arXiv containing "Lean theorem prover" for example. I'm not sure anyone has done a systematic evaluation of the literature, but it doesn't seem to be that big of a lift.
Again, you will probably find a lot more published in CS conferences and journals than mathematics conferences and journals.
Last, as for "Percentage of mathematicians who have published a paper critically using a computer proof assisted result", "critical" is a difficult word here. For almost every paper using a proof assistant, the proof assistant part is most of the paper and "critical" to the paper, but rarely are proof assistants used to prove new mathematical theorems. Even in places where they have shown a lot of value in checking difficult or important proofs---the four color theorem, the Kepler conjecture proof, and liquid tensor theory---the theorems were first published without formal proofs and only later were formal proofs added. For questions like this, I think you would do better with case studies rather than percentages, since there are only a handful of important uses of proof assistants in mathematics so far (but hopefully that is increasing).
Edit: Sorry. I missed the main question about most popular proof assistants. Some proof assistant communities, like HOL-Light, Lean, and Coq store much of their code on Github. So it is possible (but I don't know how off-hand) to see how much code there is. (Well Lean has a distinct extension .lean. I don't know if Coq's .v extension is used by other applications. HOL-Light is just written inside Ocaml .ml files, but also there isn't a lot of it outside of a few major projects.) Others like Mizar, Metamath, and Isabelle have their own repository systems.
My guess is that if you consider all proof assistant code, then Coq would win by far (unless other industrial systems like PVS are more popular than I realize). Coq has been used for a large number of projects, both mathematical and industrial. There are verified compilers, verified software, and a lot of programing language theory is done in Coq. (Also, see the Coq user survey, including the graph at the bottom of other proof assistants used by Coq users).
But if you are interested in just formalizing pure math, then I think Lean, Coq, Isabelle, Metamath, Mizar, HOL-Light, and Agda are the most popular. Here are some statistics I compiled about the sizes of their libraries. (It is hard for Coq since there isn't a single canonical math library like the others. I also don't know a lot about the Agda community.)
I think Lean's mathlib currently has the most momentum for a large unified library of pure math. I could be wrong and I don't mean to dismiss the other projects. As for Lean's mathlib library, you can see all the subjects it covers.
Also, one shouldn't dismiss work done on homotopy type theory. It is a mathematical subject closely tied to proof assistants and some proof assistants like Coq, Agda, and Arend have libraries specifically for univalent mathematics in homotopy type theory. Those might not have the same level of total popularity as software verification projects or classical mathematics, but they are important projects with a lot of potential to grow as this area becomes more popular.
