I'll recall that vvs mentioned this on Feb. 10: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/h9PRflr9FgAJ
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/: "What if an undergraduate wants to try formalising the Hilbert basis theorem? What do they do?" Well, possibly they might look to http://us.metamath.org/mpeuni/hbt.html for some hints. :) BTW one purpose of the "Quantum Logic Explorer" (ql.mm) was to verify some proofs for a couple of papers, because the logic can be somewhat non-intuitive, and I don't think I'd have peace of mind not knowing if there was a flaw in one of my published claims. On several occasions I wrote the short, informal published proof using the formal proof as a guide. The formal proof, in turn, was based on scribbles on paper that sometimes I'd discover were wrong. https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/: "It will probably cost hundreds of millions of pounds worth of person-hours to digitise any one of the known proofs of Fermat’s Last Theorem, and once digitised, these proofs will need maintaining, like any software, which will cost more money." A curious estimate - I wonder why he thinks it would be that much. Although if the formalization language is stable, it shouldn't need "maintaining", unlike ordinary software in which there are almost always unknown bugs remaining. The point of a formal proof (verified with a small trusted kernel) is to eliminate the possibility of a mistake or bug; once a formal proof is completed, it is finished for all posterity, aside from any optional tweaks such as proof shortening that people may wish to make. On https://xenaproject.wordpress.com/2019/12/07/rigorous-mathematics/ he has a link to Mario's Metamath proof of the prime number theorem. Norm On Saturday, February 22, 2020 at 4:01:48 PM UTC-5, David A. Wheeler wrote: > > Fyi, There is an interesting essay about math formulas ation here: > > https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ > > There is a discussion about it here: > https://news.ycombinator.com/item?id=22390486 > --- David A.Wheeler -- 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/91920866-4420-433e-8cb1-bb75ec2b9314%40googlegroups.com.
