Re: [mizar] Rudin's "Principles of Analysis" Rosetta Stone

This could probably be tried today with neural autoformalization methods [1] helped by interested people in some wiki/github-style collaborative project. One would need the Diedonne's books, best in Latex, or at least as images/pdf's from which the text/latex can be reasonably extracted by OCR. The publishers might be interested in such an open project (and provide the latex).

Josef

[1] https://doi.org/10.1007/978-3-319-96812-4_22

On Sun, Nov 26, 2023 at 4:44 AM Alex Nelson thmprover _AT_ gmail.com <owner-mizar-forum@mizar.uwb.edu.pl> 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