These are broad questions and I doubt you will get a complete answer in a single stack exchange answer. But since you seem ernest and interested, let me at least try to help clarify some of your questions.
What types of theorems can proof assistants solve, and what types can they not at the present moment?
First, to be clear, the primary purpose of proof assistants isn't to solve new theorems in mathematics automatically. It is to help a human write proofs in an air-tight form. Think of them as a programing language but instead of writing code, you write a proof---and instead of compiling and running the code, the computer checks that the proof is correct.
The three primary use cases of proof assistants are:
- To prove the correctness of computer code and hardware. Unlike mathematical proofs, these proofs are very tedious and a small missing case could mean the difference between correct code and a costly bug. Proof assistants help to do this tedious work and not miss edge cases.
- To build a library of formal mathematics. By formalizing all of mathematics we can begin to make mathematics more accessible to computers and unify all of mathematics into a few curated digital libraries of mathematics.
- To explore new types of logical systems. New logics can be unintuitive and formal systems can help work with them. Conversely, new foundational systems may be better suited for formalizing mathematics on a computer.
A related technology called automated theorem provers are used to prove theorems automatically. SAT solvers, SMT solvers, and resolution theorem provers are some examples. They are often used for industrial applications, but they also have been used to solve certain combinatorial theorems.
Having said all this, there is a continuum between proof assistants and automated theorem provers. More proof assistants have some levels of automation (some using full powered automated theorem provers) which fill in "obvious proof steps". Further a lot of current work in AI theorem proving uses data from proof assistant libraries to train AI models.
Now, if I misunderstood your question and you meant what types of theorems can a proof assistant be used for formalize, here is the answer: In principle, all correct theorems should be formalizable since they follow from the axioms of mathematics. In practice, some types of mathematics are easier than others. Obviously, theorems like Fermat's Last Theorem which both depend on a lot of other kinds of mathematics and are large proofs in themselves, would be a lot of work to formalize. It is better to build a library of mathematics slowly adding in more and more until you have the theorems and tools you need to prove modern theorems.
Also, some subjects like calculus and statistics are import so we teach them to college freshman, but their foundations are actually quite complicated making them difficult to formalize.
How can they be improved?
Usability is a big concern. Proof assistants are still hard to work with. Formalizing is slow and it is a specialized skill. Adding the state of art in program language design and interactive development environment tools would help.
Mathematics in a proof assistant is also very different looking than informal mathematics. Bridging this gap would go a long way to speeding up formal proofs.
Better automation might help. Then the user could have the computer fill in the obvious and not-so-obvious steps. A dream would even have a computer system which could auto-formalize mathematics from say an informal LaTeX proof to a formal proof. This is incredible challenging, but an exciting research goal.
Proof repair is an interesting topic. Proofs break if you change the theorem you are proving. This is especially common when proving the correctness of a piece of computer code which is subject to change. But in many cases, it should be straight forward to repair the proof, and the computer in principle should be able to do it for you.
There are many proof assistants, but they are incompatible with each other. A proof in one proof assistant isn't usable by any other proof assistants. Better interchangeability would go a long way.
There is also the problem that formalization is not well rewarded in academics or industry.
What avoidable and unavoidable limitations are there?
I think I mentioned many avoidable limitations.
As far as unavoidable ones, baring human-level artificial intelligence, it is likely going to continue to be a somewhat tedious human process which gets progressively easier with better tools.
Is there anything else I should know about the current and potential future states of proof assistants?
Probably. But at the same time, just get started playing with proof assistants if they interest you. They are video-game level addictive! I recommend the natural number game as a fun starting point. After doing that, pick a proof assistant that interests you, get to know the community, and start formalizing stuff!
