Ah yes, that was me.I started it on Nov '18 apparently? How time flies. The idea was to basically comment in a standard book where to find the equivalent definitions/theorems in Mizar, so that people who were taught with the standard book have an easier time learning Mizar. But since I grew up with German literature on the subject, so I just took an English book I found referenced online a lot.
If I remember correctly I put the project on ice because I reached parts of the book that were only sparsely formalized in Mizar: Differential forms. If I'm not mistaken, Shidama-sensei is currently working on these for the Stokes Theorem and I plan to support him in the endeavor.
I can do Mizar commentary on Dieudonne (the English translation) as well if it helps. If so, let me know :-)
Best regards Sebastian "Ayutac" Koch On 26.11.23 04:41, Alex Nelson thmprover _AT_ gmail.com wrote:
Hello,I would like to bring to your attention an effort I stumbled across (of which I have not yet participated in), an attempt to identify the definitions and theorems from Rudin's "Principles of Mathematical Analysis" with their counterparts in Mizar: https://en.wikibooks.org/wiki/Mizar_Commentary_on_Walter_Rudin%27s_Principles_of_Mathematical_AnalysisNow, if only someone would do Dieudonne's treatise on analysis... ;) Best, Alex