Foundations for Mathematical Methodology

[Juan Michelini]

Hi everybody!

Long time listener, first time caller.

Just wanted to see if you are interested in my master's thesis. Here is the abstract:

We present, for the equational theory of a variant of typed λ-calculus, a
method to find interesting conjectures and to design their proofs. Like the
methods taught in basic arithmetic, for the most part the practitioners, which
we imagine as undergraduate or even high-school students, can just follow the
rules but, if they want to, they can apply an intuitive jump at any point without
compromising the outcome. More specifically, we present a series of rules which
allow the student to discover, say, the type of lists, discover that the function
that reverses a list is interesting, discover that the reverse function is its own
inverse and prove so, in much the same way in which they solve a second degree
equation. We maintain a firm conceptual grasp of the method by formalizing it
as a computer program. Such formalization allows us to establish properties of
the method with certainty, first by doing experiments and, in some future work,
by doing Mathematics over the method itself.

I have attached the full version. All feedback is welcome.

Thanks for reading!

Juan Michelini

[Juan Michelini]

If we want to study methodology for doing mathematics, it follows that we should study methods on its own right. Can we formalize methods that humans can comfortably use to develop mathematics? I think we can, and I think that the attached document proves it.
Many caveats can be given, as always, but I believe that with love, luck and discipline they can be resolved. Continuing this line of work allows us a deeper and more conscious understanding of mathematics and mathematical thought. It also allows us to automatize the search of proofs that follow the methodology. Please, if you are serious about Dijkstra's dream, do not dismiss this message. I will cherish any questions or comments you might have.

[a c]

Your thesis is very interesting. Timothy Gowers, a british mathematician is also trying to program a theorem prover for elementary real analysis. Here is the link:

https://www.google.com.ar/url?sa=t&rct=j&q=&esrc=s&source=web&cd=4&ved=0ahUKEwje2MzB55PUAhVBGpAKHYVMDFEQFghBMAM&url=https%3A%2F%2Fwww.repository.cam.ac.uk%2Fhandle%2F1810%2F256497&usg=AFQjCNEX9kaMZEUBIH7B7NSoi6CjK40ILA&sig2=NBB_6mnudJvh54KBqz2GvA

[Juan Michelini]

You are very kind. I am studying Gowers' work and might contact him in the future.
Thank you, sometimes all it takes is a little bit of light.

[a c]

Hi again, I am still interested in this topic.

Here I found another paper about theorem proving ("On Learning to prove"), but this time the technique used is deep learning. However, there are still a lot of open questions as discussed at the end of the article.

https://arxiv.org/abs/1904.11099

I know it is not about lambda calculus, but as R. Feynmann used to say "we have to run in as many directions as possible". 

Saluti!

[Juan Michelini]

Hey a c, sorry for the late reply, you are very kind.

How do you find these papers? And I'm curious, how would you call this approach that models mathematically how humans prove?

Thanks!

--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/402a4007-b17f-4225-802f-8ccdb1b21c2fo%40googlegroups.com.

--

Juan Michelini