[FOM] deautomatization in mathematics

[Timothy Y. Chow]

> Professor Paulson stated:
>
> The importance of legibility can hardly be overstated. A legible proof 
> is more likely to convince a sceptical mathematician: somebody who 
> doesn?t trust a complex software system, especially if it says x=0 = 0. 
> While much research has gone into the verification of proof procedures 
> [32, 47], all such work requires trusting similar software. But a 
> mathematician may believe a specific formal proof if it can be inspected 
> directly, breaking this vicious cycle. Ideally, the mathematician would 
> then gain the confidence to construct new formal proofs, possibly 
> reusing parts of other proofs. Legibility is crucial for this.

I'm wondering if ideas from verifiable computation and interactive proofs 
have been applied to machine proofs of mathematical theorems.  The idea is 
to create a setup where the skeptic issues carefully chosen random 
challenges to the prover.  If the prover really has a proof then all the 
challenges can be met, whereas if the prover does not have a proof then 
the probability of being able to fool the skeptic can be made 
exponentially small.  With a well-designed protocol, the skeptic can be 
convinced with much less work than is needed to check the entire proof in 
detail.

Can this kind of idea be made to work with machine proofs of 
mathematically interesting theorems?

Tim