(This answer was originally for verifying combinatorial constructions - choice of a proof assistant, but others thought it was better as an answer for this question---or for Are some proof assistants better suited for given areas of math than others?  .)

I think for these sorts of questions it depends a lot on your goals. Here is some general advice.

• Is this a fun project to learn a proof assistant? If so, you may just want to pick the proof assistant which is most appealing to you for other reasons. For example, maybe in the end you really want to start contributing to one of the big libraries of formal mathematics like AFP, mathlib, set.mm, Mizar, etc.
• Do you want to use a specific logic like HoTT or intuisionistic logic, just to learn it? Then pick a theorem prover and library which uses that kind of logic and has many good examples, tutorials.
• Do you want to be able to say that you formalized a particular theorem (maybe because it is your favorite area of mathematics)? Almost any theorem prover would work, but if you need lots of other areas of mathematics as prerequisite then you should look into what some of the larger math libraries (AFP, mathlib, set.mm, Mizar) already have available and ask if the prerequisites you need play well together.
• Do you want your theorems and definitions to be used by others for further mathematics? Then you should likely pick not only a proof assistant, but the formal mathematics library you would like it to eventually go into. If you put your code into another library, the library maintainers will make sure it doesn't "bit rot".
• Do you want your theorems to be used by yourself or others for certifying software and hardware? Then again, look for the proof assistants which focus on this sort of thing.
• Do you want to compute with the objects you are creating? This can get a bit tricky. Coq, Lean, Agda act as programming languages for working with your objects. (Lean 4 is a lot more capable in this area than Lean 3.) So if your definition is computable, you can compute with it. On a separate topic you can also extract programs from proofs in some proof assistants. I don't know much about this, but it seems from what I have heard this can be hit or miss. A proof is not necessarily optimized to be good code. Also, I think the proof needs to be constructive for automatic extraction. Another option is just to code up the algorithm used in the proof directly (in say Lean 4, Agda, or Coq) and then prove it has the properties you want. This way you have both an algorithm and proof. Also, you can use whatever axioms you want for the proof. It doesn't need to be constructive.

(This answer was originally for another question, but others thought it was better as an answer for this question, or for this question.)

I think for these sorts of questions it depends a lot on your goals. Here is some general advice.

• Is this a fun project to learn a proof assistant? If so, you may just want to pick the proof assistant which is most appealing to you for other reasons. For example, maybe in the end you really want to start contributing to one of the big libraries of formal mathematics like AFP, mathlib, set.mm, Mizar, etc.
• Do you want to use a specific logic like HoTT or intuisionistic logic, just to learn it? Then pick a theorem prover and library which uses that kind of logic and has many good examples, tutorials.
• Do you want to be able to say that you formalized a particular theorem (maybe because it is your favorite area of mathematics)? Almost any theorem prover would work, but if you need lots of other areas of mathematics as prerequisite then you should look into what some of the larger math libraries (AFP, mathlib, set.mm, Mizar) already have available and ask if the prerequisites you need play well together.
• Do you want your theorems and definitions to be used by others for further mathematics? Then you should likely pick not only a proof assistant, but the formal mathematics library you would like it to eventually go into. If you put your code into another library, the library maintainers will make sure it doesn't "bit rot".
• Do you want your theorems to be used by yourself or others for certifying software and hardware? Then again, look for the proof assistants which focus on this sort of thing.
• Do you want to compute with the objects you are creating? This can get a bit tricky. Coq, Lean, Agda act as programming languages for working with your objects. (Lean 4 is a lot more capable in this area than Lean 3.) So if your definition is computable, you can compute with it. On a separate topic you can also extract programs from proofs in some proof assistants. I don't know much about this, but it seems from what I have heard this can be hit or miss. A proof is not necessarily optimized to be good code. Also, I think the proof needs to be constructive for automatic extraction. Another option is just to code up the algorithm used in the proof directly (in say Lean 4, Agda, or Coq) and then prove it has the properties you want. This way you have both an algorithm and proof. Also, you can use whatever axioms you want for the proof. It doesn't need to be constructive.