Thats not true… in Lean you can restrict yourself to constructive math if you want to for some reason. Just that most actual mathematicians don’t.