What is...computer aided mathematics?

[@dr-evil]

I recently finished a course ' Mathematics in Lean' which was learning lean by solving simple proofs. And I loved to game against the assistant to solve the proof. One could just click on definitions and theorems to expand them etc. Having an interactive proof would be so much clearer. One could experiment with it to understand it.

[@VisualMath]

Oh, that sounds fun 😆 And thanks for making one point I forgot to mention: We really need to work on the way we present math. This is true in general, but (computer) proofs would definite profit from a more interactive component instead of being plain dry 🤔

[@lwmarti]

I'm now retired, but when I used to do math for a living, I found a computer to be a very useful tool. At least in my experience, you do math by understanding small examples, understanding what's going on, and then generalizing to more general cases. Using computers to do calculations, draw graphs, etc., makes understanding simple cases much faster and easier, which makes the process of doing math much faster and easier. I never would have really understood elliptic and hyperelliptic curves, particularly projective ones, without a computer, for. example. Or complex multiplication. Before I used a computer, I never really understood CM. After using one, it seemed painfully obvious. There are places where computers may not help much. I don't think that they helped me understand divisors (Weil, etc.), for example, but I'm a big believer in using computers in math.

[@VisualMath]

I totally agree: computer are great for “experiments” and visualization alike. I didn’t make the second point, so thanks for reminding me 😀