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.
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.