Re: Rudin's "Principles of Analysis" Rosetta Stone

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_Analysis 
>
>
> Now, if only someone would do Dieudonne's treatise on analysis... ;)
>
> Best,
> Alex