It is definitely less fleshed out since the project is very new (I think the first usable instance is like beginning of this year!) whereas afaik Lean 4's mathlib was ported from Lean 3 which has been around for at least 8 years and has had active contributions from around then too.
On the other hand, the `acornlib` (https://github.com/acornprover/acornlib) repo happily takes PRs that pass for many objects such as `Group`s (especially those in the standard library). so if there's something you're interested in proving, I would highly recommend just cloning it and proving it directly in the standard library and then PRing!
Comments
It is definitely less fleshed out since the project is very new (I think the first usable instance is like beginning of this year!) whereas afaik Lean 4's mathlib was ported from Lean 3 which has been around for at least 8 years and has had active contributions from around then too.
On the other hand, the `acornlib` (https://github.com/acornprover/acornlib) repo happily takes PRs that pass for many objects such as `Group`s (especially those in the standard library). so if there's something you're interested in proving, I would highly recommend just cloning it and proving it directly in the standard library and then PRing!