proof methods

[Timothy Y. Chow]

On Wed, 11 Nov 2020, Buday Gergely wrote:
> My answer is: to have a taxonomy of general proof methods, so that I can 
> investigate them, how much they are amenable to formalization in a 
> theorem prover.

Ah!  Yes, this is now a specific question.  However, I'm not really 
competent to answer it.  A proof taxonomy that makes sense to a human does 
not necessarily translate into a research program for people working on 
formal proofs.  In particular, I'm not even sure that it makes sense to 
think of the current challenges facing proof assistants as being 
formalizing *kinds of proofs*.  For example, Tom Hales's criticisms of 
Lean a couple years ago focused a lot on the difficulties with dealing 
with *mathematical structures* rather than *kinds of proofs*:

https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

Presumably you're aware of the Xena project?

https://xenaproject.wordpress.com/what-is-the-xena-project/

Buzzard wants to formalize the entire undergraduate curriculum in Lean.

Tim