> > > * "Pedagogy" section: I would simply remove the whole thing: it merely > expresses someone's opinions (which, FWIW, I happen to disagree with). It > looks like it was written by FL? I you read me, Frédéric, what's your > opinion? Can we delete it? Remember that some of the harshest criticisms > made to Bourbaki were actually directed to people wanting to use ideas from > their Eléments as pedagogical tools. >
1) I'm a little confused. I see no mention of the Bourbaki's treatise on this page. I'm talking about a proof checker from Juha Arpiainen called Bourbaki. It's not the same thing. 2) On the other hand, if someone wants to read Bourbaki's treatise, one of the best things to do is to implement the proofs in set.mm. That I'm sure of it. And it is one of the most beautiful presentations (the most beautiful) of the structure concept of structure. And then I'm for textual references in set.mm. If there is none, no one will read the material. 3) Rereading what I wrote many years ago about the possible use of metamath in high school or college (the pedagogy section), I still agree with this view. 4) Leave some substance to the article anyway. It should be a guide to where and when to use metamath and where and when not to use it. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2dff9523-40e0-4db6-bc12-61859fc2f4ee%40googlegroups.com.
