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 ?
3 Answers
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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.