I can't stand math classes because they're not formal enough; class on surreal numbers

[gusl]

am I the only person in the world who can't stand math classes because they're not formal enough?

Today I went to a lecture on surreal numbers, saw people struggling with bad notation, and with bringing variables out of quantifiers and then back in (this pisses me off because it's best done by an algorithm, and can be quite taxing for humans)... Some people would argue that if you're searching for a syntactic way of proving something (i.e. without *seeing* the underlying facts), then you're not being a "noble mathematician". I have no such prejudices.

Comments

[jcreed.livejournal.com]

I am totally with you on this issue in general.

I can't think of a class off-hand where I got pissed off by it not being formal enough because, by and large, the classes I've taken here have been rather formal.

[gustavolacerda.livejournal.com]

the classes I've taken here have been rather formal.

what's your definition of a "formal math class"?

[gustavolacerda.livejournal.com]

My complaint is that doing math by hand is often unnecessarily hard. i.e. it's only hard because my memory is small, and the sheet of paper in front of me isn't dynamic enough, so I end up having to write things many times (something I have no patience for). A proof assistant like Coq can help a lot in cases like this.
(Other limitations of paper include running out of space for diagrams, whatever.)

Much of the work we do when doing math is algorithmic. And by this I mean "automatable by simple algorithms". (under my philosophy saying something is "algorithmic" is vacuous, since I believe that minds are machines.)

Also, when trying to find a proof, we do proof-planning in our heads, but for some reason mathematicians don't like to write it down, as if it were an admission of weakness. The consequence of this is that the process by which people arrive at proofs is mysterious. People would be better mathematicians if they were explicit about the meta-level reasoning they do when searching for proofs, how they use heuristics, etc.