Comment by logicchains
10 hours ago
>For example, in my quantum class the teacher wrote "H Psi = E Psi" on the board, we all laughed, "just cancel the psi" but it turns out one was a multiplcation and the other was a matrix multiplication (operator) and so we had to learn all new nomenclature.
This is one of the great things about Lean becoming used for more and more mathematics: understanding exactly how an operator/function is defined is just an IDE click or few away. It completely removes the ambiguity present in hand-written proofs, although it still can require a lot of reading to actually meaningfully understand the definitions.
I would expand on this. AI is great for me because it can read the equations I don't understand and turn it into code I can understand. I've worked in science for decades and it's still like pulling teeth to replicate a competitor's paper when they are vague and sloppy with their description (often intentionally).
ugh, I had some text book that used R for a scalar value and (edit: \u{MATHEMATICAL BOLD FRAKTUR CAPITAL R} here) for a matrix that was related to the scalar and I had to go back and re-learn a month of material once I figured out that the font was being used with intent