proof methods

[Buday Gergely]

11/10/2020 5:28 PM keltezéssel, Timothy Y. Chow írta:

> On Tue, 10 Nov 2020, Buday Gergely wrote:
>> In science, narrowing a topic is a useful method and can lead to a 
>> tractable problem.
>>
>> How about this one: proof methods in university mathematics 
>> textbooks? So, what is in the standard toolbox of a mathematician who 
>> has an undergraduate degree in pure or applied mathematics.
>>
>> Is this still too broad?
>
> I feel that I'm still not sure what you're really asking for.
>
> Are you asking for strategies for coming up with a proof in the first 
> place?  Or are you focusing on the final writeup of the proof and 
> trying to categorize the different kinds of templates that exist?
>
> Are you looking for high-level descriptions that are largely 
> independent of subject matter ("to distinguish two objects, find an 
> invariant that differs in the two cases") or do you also want to 
> include techniques that use specific theorems ("bound your sequence 
> and apply the dominated convergence theorem")?
>
> Is your goal to teach students how to come up with proofs and/or write 
> them up properly?  Or to teach a computer how to come up with proofs?  
> Or to draw philosophical conclusions about mathematical proof?
>
> If your answer is, "All of the above," then I think your question is 
> still too broad.
>
> Tim

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.

Direct, indirect proof, in general natural deduction: programmable in a 
functional language in a few thousand lines, originally a research 
project, now a triviality

Induction, coinduction: extensive research

Symmetry: the theory of nominal sets and its implementation in Nominal 
Isabelle: multi-year multi-person research project.

All these are done. I would like to read about more proof methods, 
whether there are ones that nobody formalized.

Is this specific enough?

- Gergely