I strongly encourage you to check back in a couple of months. I expect things will be a lot more polished then. The team is currently quite busy with porting ma

I strongly encourage you to check back in a couple of months. I expect things will be a lot more polished then. The team is currently quite busy with porting mathlib from Lean 3 to Lean 4. This is an excellent stress test for the language, and it's used to find and fix all sorts of minor bugs.