= 27d567bc2d48d9f40e9ccc20ea370b15)
RichardKennaway comments on Formalized math: dream vs reality - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (9)
Isn't all this being worked on already? Just put "automath", "mizar", or "automated reasoning" into Google Books, and you'll find a vast quantity of material. Did you have something else in mind that no-one is doing?
As far as I know, none of these "proof assistants" is actually used as such. Although Automath and Mizar are decades old, the research is still all about how to build such systems and make verified depositories of known mathematics in them.
Yes, this is all being worked on; I didn't mean to imply this stuff was new. Two examples of useful applications: proving the four-color theorem in Coq, and proving the correctness of microprocessors (e.g. floating point division after the notorious Pentium bug) in ACL2.