[FOM] formal proofs

[Jacques Carette]

On 2014-10-21 5:49 PM, croux at andrew.cmu.edu wrote:T
> More realistically, I think we should investigate manners of capturing
> "field-specific" knowledge,
> notations and intuition in a way that can be mechanized. It's hard for me
> to think of examples,
> but "working in the group of endomorphisms" in group theory comes to mind,
> as well as "passing to
> the dual" in linear algebra or simply just "swapping integrals" in
> calculus (or swapping sums, or swapping
> differentials and integrals, etc).

Indeed.  This is exactly what "high level theories" [1] and "realms" [2] 
are all about -- structures for mechanized mathematics system to capture 
this kind of knowledge.

It is worthwhile noting that these ideas are largely 
foundations-independent.  By the time you get to capturing 
field-specific knowledge, you've buried foundations in enough levels of 
abstractions [assuming your foundations has decent enough abstraction 
mechanisms!] that they are (mostly) interchangeable.

For those who know software engineering, the best analogy is with 
'architecture patterns': they are valid solutions to the problems each 
pattern is for, regardless of the paradigm (imperative, OO, functional 
or even logic) of the underlying programming language.

Jacques

[1] official link: 
http://link.springer.com/chapter/10.1007%2F978-3-540-85110-3_19
preprint: http://imps.mcmaster.ca/doc/hlt.pdf

[2] official link: 
http://link.springer.com/chapter/10.1007%2F978-3-319-08434-3_19
preprint: http://arxiv.org/abs/1405.5956