I am a software engineer with education in mathematics and I have been working on a formalized mathematics project for the last 16 years (on and off). There is no particular purpose of this, other than it is a good mental workout and a satisfying way to acquire understanding of various areas of mathematics by writing proofs that are sufficiently detailed and correct that can be checked by a machine. I would like to improve the presentation of the project at isarmathlib.org and I would love some help with this. Of course there is plenty of math to formalize as well. If you are interested, you can contact me through the project's GitHub Discussions or other links at the project's site.