MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 ?

share|cite|improve this question
up vote 3 down vote accepted

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.


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.

share|cite|improve this answer

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.

share|cite|improve this answer

There is a Journal of Formalized Mathematics connected with Mizar project

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.