Has everyone read Freek Wiedijk's bold and stirring article in the Notices of the AMS, mentioned in the wiki page for HOL Light? Freek's last point occurred to me: how can I get someone to referee my Hilbert paper? Why don't I formalize it myself first in miz3?
-- Best, Bill Freek Wiedijk The Future of Formal Mathematics In mathematics there have been three main revolutions: o The introduction of proof by the Greeks in the fourth century BC, culminating in Euclid’s Elements. o The introduction of rigor in mathematics in the nineteenth century. During this time December 2008 Notices of the AMS 1413 the nonrigorous calculus was made rigorous by Cauchy and others. This time also saw the development of mathematical logic by Frege and the development of set theory by Cantor. o The introduction of formal mathematics in the late twentieth and early twenty-first centuries. Most mathematicians are not aware that this third revolution already has happened, and many probably will disagree that this revolution even is needed. However, in a few centuries mathematicians will look back at our time as the time of this revolution. [...] referees will insist on getting a formalized version before they want to look at a paper. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
