Definitely looks like a smoother experience than using Lean from this presentation. I guess their library is less fleshed-out than mathlib at the moment but that can only grow I suppose (hence acorn??). Will be curious to see how it develops
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
Definitely looks like a smoother experience than using Lean from this presentation. I guess their library is less fleshed-out than mathlib at the moment but that can only grow I suppose (hence acorn??). Will be curious to see how it develops
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!