I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of abstraction is it currently possible to perform formal proofs using proof assistants with reasonable effort?

Of course many branches of contemporary research rely heavily on large and complex theories which fill books but have not been formalised at all. On the other hand there are theorems which are thousands of years old (irrationality of $\sqrt{2}$) whose proofs can be found in every example-page on the websites of the proof assistants. I would not find it very compelling to perform elementary proofs in say arithmetics, elementary number theory or euclidean geometry, I would prefer a context where there is already some more abstraction available. There must be some level in-between were it is still possible to perform proofs without having to formalise whole theories. How can we describe this level?

Let me give an illustrative example: We could try to prove existence and uniqueness of the Haar measure. It is an old theorem from 1940 and it only uses very established and common theories. The proof is technical and you would definitely have to do some hard work to get all inequalities right in a fully formalised version, but we might think—it is probably naive—that it would be a manageable project. However, if it turns out that there are not yet any definitions and theorems from measure theory in the proof assistant, if you would have to formalise some stuff about Banach spaces and some concrete function spaces first, and if even the available material for general topology is very limited, it might turn out to be a project taking years.

So, can anybody tell me what is already available and usable for reusage in proof assistants? Are there basic frameworks for say general topology and for dealing with the most common algebraic structures available, which are usable and well-structured and not totally messed up and which are still maintained? With which kinds of structures can you actually work (measure spaces? categories? manifolds? function spaces?), this includes, of course, the most fundamental lemmata/theorems (since the community of formal proofs is not that big, of course I do not expect any of such collections to be as exhaustive as some informal, large books). Are there large differences between the major proof assistants (Isabelle, Coq, Mizar…) with respect to such support?

(I am not asking for the state of current big projects to formalise a theorem, for example by Hales, but I want to know where the software is “ready to use”)

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of abstraction is it currently possible to perform formal proofs using proof assistants with reasonable effort?

Of course many branches of contemporary research rely heavily on large and complex theories which fill books but have not been formalised at all. On the other hand there are theorems which are thousands of years old (irrationality of $\sqrt{2}$) whose proofs can be found in every example-page on the websites of the proof assistants. I would not find it very compelling to perform elementary proofs in say arithmetics, elementary number theory or euclidean geometry, I would prefer a context where there is already some more abstraction available. There must be some level in-between were it is still possible to perform proofs without having to formalise whole theories. How can we describe this level?

Let me give an illustrative example: We could try to prove existence and uniqueness of the Haar measure. It is an old theorem from 1940 and it only uses very established and common theories. The proof is technical and you would definitely have to do some hard work to get all inequalities right in a fully formalised version, but we might think—it is probably naive—that it would be a manageable project. However, if it turns out that there are not yet any definitions and theorems from measure theory in the proof assistant, if you would have to formalise some stuff about Banach spaces and some concrete function spaces first, and if even the available material for general topology is very limited, it might turn out to be a project taking years.

So, can anybody tell me what is already available and usable for reusage in proof assistants? Are there basic frameworks for say general topology and for dealing with the most common algebraic structures available which are usable and well-structured and not totally messed up and which are still maintained? With which kinds of structures can you actually work (measure spaces? categories? manifolds? function spaces?), this includes, of course, the most fundamental lemmata/theorems (since the community of formal proofs is not that big, of course I do not expect any of such collections to be as exhaustive as some informal, large books). Are there large differences between the major proof assistants (Isabelle, Coq, Mizar…) with respect to such support?

(I am not asking for the state of current big projects to formalise a theorem, for example by Hales, but I want to know where the software is “ready to use”)

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of abstraction is it currently possible to perform formal proofs using proof assistants with reasonable effort?

Of course many branches of contemporary research rely heavily on large and complex theories which fill books but have not been formalised at all. On the other hand there are theorems which are thousands of years old (irrationality of $\sqrt{2}$) whose proofs can be found in every example-page on the websites of the proof assistants. I would not find it very compelling to perform elementary proofs in say arithmetics, elementary number theory or euclidean geometry, I would prefer a context where there is already some more abstraction available. There must be some level in-between were it is still possible to perform proofs without having to formalise whole theories. How can we describe this level?

Let me give an illustrative example: We could try to prove existence and uniqueness of the Haar measure. It is an old theorem from 1940 and it only uses very established and common theories. The proof is technical and you would definitely have to do some hard work to get all inequalities right in a fully formalised version, but we might think—it is probably naive—that it would be a manageable project. However, if it turns out that there are not yet any definitions and theorems from measure theory in the proof assistant, if you would have to formalise some stuff about Banach spaces and some concrete function spaces first, and if even the available material for general topology is very limited, it might turn out to be a project taking years.

So, can anybody tell me what is already available and usable for reusage in proof assistants? Are there basic frameworks for say general topology and for dealing with the most common algebraic structures available, which are usable and well-structured and not totally messed up and which are still maintained? With which kinds of structures can you actually work (measure spaces? categories? manifolds? function spaces?), this includes, of course, the most fundamental lemmata/theorems (since the community of formal proofs is not that big, of course I do not expect any of such collections to be as exhaustive as some informal, large books). Are there large differences between the major proof assistants (Isabelle, Coq, Mizar…) with respect to such support?

I am wondering whether I should try to have some fun using proof systems. I have never used such a system, but I have some experiences in logic and programming. My question is: At which level of abstraction is it currently possible to perform formal proofs using proof assistants with reasonable effort?

Of course many branches of contemporary research rely heavily on large and complex theories which fill books but have not been formalised at all. On the other hand there are theorems which are thousands of years old (irrationality of $\sqrt{2}$) whose proofs can be found in every example-page on the websites of the proof assistants. I would not find it very compelling to perform elementary proofs in say arithmetics, elementary number theory or euclidean geometry, I would prefer a context where there is already some more abstraction available. There must be some level in-between were it is still possible to perform proofs without having to formalise whole theories. How can we describe this level?

Let me give an illustrative example: We could try to prove existence and uniqueness of the Haar measure. It is an old theorem from 1940 and it only uses very established and common theories. The proof is technical and you would definitely have to do some hard work to get all inequalities right in a fully formalised version, but we might think—it is probably naive—that it would be a manageable project. However, if it turns out that there are not yet any definitions and theorems from measure theory in the proof assistant, if you would have to formalise some stuff about Banach spaces and some concrete function spaces first, and if even the available material for general topology is very limited, it might turn out to be a project taking years.

So, can anybody tell me what is already available and usable for reusage in proof assistants? Are there basic frameworks for say general topology and for dealing with the most common algebraic structures available, which are usable and well-structured and not totally messed up and which are still maintained? With which kinds of structures can you actually work (measure spaces? categories? manifolds? function spaces?), this includes, of course, the most fundamental lemmata/theorems (since the community of formal proofs is not that big, of course I do not expect any of such collections to be as exhaustive as some informal, large books). Are there large differences between the major proof assistants (Isabelle, Coq, Mizar…) with respect to such support?

(I am not asking for the state of current big projects to formalise a theorem, for example by Hales, but I want to know where the software is “ready to use”)