alt Hacker NewsI am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?
i feel like this would be the equivalent of having all CS undergrads program with assembly and assembly only.
it might(?) work? but abstractions exist for a reason (mostly...)