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.
Related questions
Breakdown: I'd say there's at least a 30% chance (if not more like 50%) that arXiv mathematicians don't noticeably cite any more computer assistance than they do today by 2026. And an independent 40% chance (if not more like 70%) that the tools they do use aren't natural language-based. This is mainly because I think any mathematician who is going to benefit from an autoformalized statement will probably be able to get more accuracy by encoding what they want more formally.
Another comment: Perusing several pdfs from https://arxiv.org/list/math/new, ctrl-F finds no mentions of "Wolfram Alpha", which you might call the state of the art in terms of natural language input for mathematics. Many mathematicians do use this tool though, so perhaps even if there is a better tool by 2026, mathematicians won't mention it in their papers.
