I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
If you want to master it and use it effectively for something real, yeah some reading would help.
It sounds like for your use case of software verification mathematical logic is important, but that’s definitely not the case for most lean users. I wouldn’t say it’s required or even useful if you want to use lean for proving things in general.
Sure.
The article we are commenting on has the "for software engineers", so I assumed the software use case is the primary one here.