3 ms·

It will be incredibly interesting to assess how the mainstream "textbook" approach to the subject compares to the one taken in the Mathlib. In general, formali

It will be incredibly interesting to assess how the mainstream "textbook" approach to the subject compares to the one taken in the Mathlib. In general, formalized math libraries make it comparatively easier to state results with a maximum degree of generality and to refactor proof developments for straightforwardness and elegance. (Refactoring is of course made easier because the system will always keep track of what follows logically from what. You don't have that when working with pen and paper, so opportunities to rework things are very often neglected.) It is a natural question also to ask whether it makes sense to teach the Mathlib, "maximum generality" version of real analysis, or at least something approaching that, in an academic course. Same for any other field of proof-based math, of course.

smohare 1y ago
As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers. I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.
- thdhhghgbhy 1y ago
  Is there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.
krapht 1y ago
Certainly not for introductory courses. There's already too much on the table - how to prove, how to program, and the base material itself. I believe that's the experience of faculty who've tried as well - it's fine for advanced students, but a waste of instructional time for the average pupil.

smohare 1y ago

As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers. I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.

thdhhghgbhy 1y ago
Is there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.

krapht 1y ago

Certainly not for introductory courses. There's already too much on the table - how to prove, how to program, and the base material itself. I believe that's the experience of faculty who've tried as well - it's fine for advanced students, but a waste of instructional time for the average pupil.