[FOM] deautomatization in mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Wed Oct 9 16:34:15 EDT 2019
> 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
More information about the FOM
mailing list