By proof assistant I mean a tool intended to aid mathematicians find proofs by making suggestions for techniques, proving lemmas, suggesting proof structures, etc. I am not requiring it to produce formally checkable output as is currently common (universal, afaik) for proof assistants.

A tool does not count if it requires significant additional annotation/interaction by the mathematician (e.g. if it requires the mathematician to take notes in a particular formal way). The inputs should be natural language (could be speech, text, images of handwriting) and proofs stated in natural language, and the output should be some kind of assistance towards proving some desired theorem(s). I'm intentionally leaving the exact form of assistance vague: the question is about whether there will be any such tool that becomes very common among mathematicians, regardless of its exact function (a tool that scanned notes and found relevant things in the literature would resolve YES, if it became common among mathematicians)

Common use: a survey shows >=20% of professional mathematicians use it, or >=20% of math arxiv papers cite/reference/credit the tool in some way, or (barring more formal surveys) mathematicians say that it is very popular/common and I personally know several mathematicians who use it.