Proof formalization - MathOverflow

Proof formalization

2010-02-25T11:48:21Z

I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport.

Are there more recent works in this field ?

Answer by Charles Stewart for Proof formalization

2010-02-25T12:01:28Z

In general, "formalising mathematical vernacular" is a good source for work relevant to your question. The field generally started in earnest with de Bruijn's Automath project.

Harvey Friedman has done some nice work on leveraging his theory of explicit definitions for set theory (cf. The Logical Strength of Mathematical Statements I, 1976) to give a language for doing mathematics in a way that is fairly natural and that can be easily translated into proofs over ZFC.

I'm afraid I don't have a good reference for this: he gave an invited talk to the ASL 2006 conference in Nijmegen.

Postscript

I remembered there were coauthors: the system was written up in a series of papers for a system called A language for knowledge management, due to Steve Kieffer (for a Master's project), Jeremy Avigad, and Harvey Friedman.

Answer by kakaz for Proof formalization

2010-02-25T13:43:33Z

There is a Journal of Formalized Mathematics connected with Mizar project

Answer by Cotton Seed for Proof formalization

2010-02-25T15:02:57Z

There was a special issue of the Notices of the AMS on Formal Proof in 2008. Freek Wiedijk, who wrote one of the Notices articles, has some good resources on his home page.