Comment by dnautics

There are things you can do in lean which are footguns. For example, 1/0 = 0 in lean. For much of math that's not a problem. Still though, you have to remember that this is the case for whatever number system you're doing a proof in. For things which map to real world scenarios it's potentially a big problem.