I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right