In this thread <https://groups.google.com/forum/#!topic/metamath/MuRdrcF6Mgo> FL you say
> Bourbaki's treatise, one of the best things to do is to implement the proofs in set.mm I wanted to ask if anyone has opinions or ideas on this? How much of the Bourbaki material do you think is implemented already in set.mm? Would that material be useful to add or is it the case that the same concepts are already covered in some different fashion? Is there anyone who is keen on this approach? I always admired the Bourbaki group. I also wonder if having the textbooks as a scaffold might make progress relatively quick, I think they do spell out everything in quite rigorous detail. -- 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/4e716b7c-c69f-4945-9bbb-7033483ffa2a%40googlegroups.com.
