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 ?
[Math] Proof formalization
formal-languagesformalizationlo.logicproof-assistants
Related Solutions
From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.)
I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction.
When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:
$$ \frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}} {\Gamma \vdash [e]_R \in A/R} $$
That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.
But using this fact is rather painful:
$$ \frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B} $$
This rule says that if you know that
- $e$ is an element of $A/R$, and
- $t$ is some element of $B$ with a free variable $x$ in set $A$, and
- if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)
Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.)
What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof).
I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.
HoTT/HoTT Categories
Links: https://github.com/HoTT/HoTT/tree/master/theories/Categories (current), https://github.com/JasonGross/HoTT-categories (old), https://bitbucket.org/JasonGross/catdb (oldest). Interactive index, non-interactive index, top-level wiki
Language: Coq 8.6; will compile with 8.7 when it comes out; the oldest version compiled with Coq 8.4)
Author: Jason Gross
Active Development: No, but actively maintained in its present form (as of June 2017)
Concepts Formalized:
1-precategories (in the sense of the HoTT Book)
univalent/saturated categories (or just categories, in the HoTT Book)
functor precategories $\mathcal C \to \mathcal D$
dual functor isomorphisms $\text{Cat} \to \text{Cat}$; and $(\mathcal{C} \to \mathcal{D})^{\text{op}} \to (\mathcal{C}^{\text{op}} \to \mathcal{D}^{\text{op}})$
the category Prop of ($U$-small) hProps
the category Set of ($U$-small) hSets
the category Cat of ($U$-small) strict (pre)categories (strict in the sense of the objects being hSets)
pseudofunctors
profunctors
- identity profunction (the hom functor $\mathcal C^\text{op} \times \mathcal C \to \text{Set}$)
adjoints
- equivalences between a number of definitions:
- unit-counit + zig-zag definition
- unit + UMP definition
- counit + UMP definition
- universal morphism definition
- hom-set definition (porting from old version in progress)
- composition, identity, dual
- pointwise adjunctions in the library, $G^\mathcal{E} \dashv F^\mathcal{C}$ and $\mathcal{E}^F \dashv \mathcal{C}^G$ from an adjunction $F \dashv G$ for functors $F : \mathcal C \leftrightarrows \mathcal D : G$ and $\mathcal E$ a precategory (still too slow to be merged into the library proper; code here)
- equivalences between a number of definitions:
Yoneda lemma
Exponential laws
- $\mathcal C^0 \cong 1$; $0^{\mathcal C} \cong 0$ given an object in $\mathcal C$
- $\mathcal C^1 \cong \mathcal C$; $1^{\mathcal C} \cong 1$
- $\mathcal C^{\mathcal A + \mathcal B} \cong \mathcal C^{\mathcal A} \times \mathcal C^{\mathcal B}$
- $(\mathcal A \times \mathcal B)^{\mathcal C} \cong \mathcal A^{\mathcal C} \times \mathcal B^{\mathcal C}$
- $(\mathcal A^{\mathcal B})^{\mathcal C} \cong \mathcal A^{\mathcal B \times \mathcal C}$
- Product laws
- $\mathcal C \times \mathcal D \cong \mathcal D \times \mathcal C$
- $\mathcal C \times 0 \cong 0 \times \mathcal C \cong 0$
- $\mathcal C \times 1 \cong 1 \times \mathcal C \cong \mathcal C$
- Grothendieck construction (oplax colimit) of a pseudofunctor to Cat
- Category of sections (gives rise to oplax limit of a pseudofunctor to Cat when applied to Grothendieck construction
- functor composition is functorial (there's a functor $\Delta : (\mathcal C \to \mathcal D) \to (\mathcal D \to \mathcal E) \to (\mathcal C \to \mathcal E)$, where each $\mathcal A \to \mathcal B$ is a functor category)
- Kan extensions are adjoints to the functorial composition functor
- (co)limits defined as Kan extensions when one of the categories is terminal
- The comma functor $\left(\mathcal C^{\mathcal A}\right)^{\text{op}} \times \mathcal C^{\mathcal B} \to \text{Cat}_{/ \mathcal A \times \mathcal B}$ which sends $\mathcal A \xrightarrow{f} \mathcal C \xleftarrow{g} \mathcal B$ to the comma category $(f / g)$ and it's projection functor to $\mathcal A \times \mathcal B$
- monoidal categories (porting from the oldest version still in progress)
- enriched categories (porting from the oldest version still in progress)
Concepts currently under construction:
- pseudonatural transformations
- (op)lax comma categories
- pointwise Kan extensions
- Cartesian closed categories
Construction Choices:
- Morphisms are dependently typed $\text{Hom}_{\mathcal C} : \text{Ob}_{\mathcal C} \to \text{Ob}_{\mathcal C} \to \text{Type}$
- Morphisms land in Type; propositional equality is used; higher inductive types are used for quotients
- Categories are records with no parameters and all fields
- Based on homotopy type theory; morphisms are hSets (0-truncated; satisfy UIP)
Best Answer
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.