[FOM] Formal Proofs

[Rempe-Gillen, Lasse]

Harvey Friedman wrote:

> CHALLENGE: Use this example to create a new field of *micro proof 
> theory*, whereby new kinds of subtle quantitative and possibly 
> qualitative features of actual mathematical proofs are investigated, 
> those which correspond to important features of actual mathematical 
> proofs that are immediately recognized as interesting and significant 
> by those reflecting on actual mathematical practice."

This sounds like a nice challenge. Certainly, there are usually some "standard" type of arguments in any given area. Some of these may even be of the kind where it seems "clear" how to proceed, but producing even a usual "rigorous" mathematical proof may be omitted in papers, because it seems odious and not particularly illuminating. (Of course this is also where errors can creep in if one is not careful ...)

Investigating some such arguments and their potential for formalization does indeed seem like a good way to focus attention.