BR Maths Corner-1

[Tanaji]

Thank you Vayutuvanji it does clarify the role of ATPs a lot. To be honest while I could read the notation, I could only understand about 50% of the proof… abstract maths is not my cup of tea

I think it’s only a matter of time before NNs come into this field - as you said it’s ripe for that application.

[Tanaji]

On another note have you or AmberG noticed a diminishing of your maths prowess with age? I recall vaguely a study that showed that. I am no mathematician by any means long shot but I my younger days I could rapidly do mental calculations like multiplying 3 digit numbers quickly, I still can but I can see it takes longer and am unsure of the result. Or I am getting dementia….

[Vayutuvan]

Thank you Vayutuvanji it does clarify the role of ATPs a lot. To be honest while I could read the notation, I could only understand about 50% of the proof… abstract maths is not my cup of tea

I think it’s only a matter of time before NNs come into this field - as you said it’s ripe for that application.

@Tanaji ji, as for understanding the proof, if you play the game interactively, goals keep changing and also assumptions keep getting added.

For example, when you do by_cases h : P, the goal splits into two. A goal with assumption h : Not P is pushed onto a goal stack. Then the goal with assumption h : P gets is pushed onto goal stack, which becomes the active goal.

You will be able to see everything nicely laid out on the web page. So the series of tasks, as I quoted above, is a lot harder than actually looking at it interactively. IOW, the state of the proof assistant is nicely visualized.

Similar visualization is supposed to be there in VS Code if you install the Lean plugin. I tried installing on my Fedora desktop, but I am running into problems. My guess is that I am running too old a Fedora version.

[Vayutuvan]

On another note have you or AmberG noticed a diminishing of your maths prowess with age?

I am never good at mental arithmetic calculations. But I do seem to be forgetting stuff like trigonometric identities, integration tricks, Fourier transforms for some commonly used generalized functions and such.

People who are in academia tend to remember physical constants, different strategies to solve ODEs, and all the identities, series expansions, or complexity classes for most algorithms problems etc. as they have to keep teaching them every year. It is usually the case that professors will be asked to teach basic courses for one semester and a course of their choice in the second semester.

[Vayutuvan]

I came across this lovely 30 min video on YT explaining Combintory Logic. It has to be seen at 0.5 speed or even 0.25 speed to work out everything he says in the video. It is quite fascinating that he could get across the basics of combinatory logic, going from S, K, I to Y Combinator and then iota combinator (which is the universal combinator).

Introduction to Combinatory Logic

Alexander Faruja and Giorgio Grigolo demonstrate how all computer programs, including complex functions like Fibonacci, can be constructed using only two foundational combinators, S and K. The Malta Mathematical Society explores the history and application of combinatory logic to eliminate the need for variables.

[Vayutuvan]

@Tanaji ji, I included that small tutorial on "how to read the notation" for those who are not introduced to First-order logic.

Please do tell your background so that I would skip the basics (unless others who are silently following and need those small 1 minute tutorials).

I usually don't like videos but I found the above interesting. It needs to be supplemented by the following introduction to the Lambda Calculus. It gives a graphical notation for Raymond Smyllyan's book "To Mock a Mockingbird".

To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
David C Keenan, 27-Aug-1996
last updated 1-Apr-2014
116 Bowman Parade, Bardon QLD 4065, Australia

https://dkeenan.com/Lambda/

Abstract
The lambda calculus, and the closely related theory of combinators, are important in the foundations of mathematics, logic and computer science. This paper provides an informal and entertaining introduction by means of an animated graphical notation.

Introduction
In the 1930s and 40s, around the birth of the "automatic computer", mathematicians wanted to formalise what we mean when we say some result or some function is "effectively computable", whether by machine or human. A "computer", originally, was a person who performed arithmetic calculations. The "effectively" part is included to indicate that we are not concerned with the time any particular computer might take to produce the result, so long as it would get there eventually. They wanted to find the simplest possible system that could be said to compute.

Several such systems were invented and for the most part looked entirely unlike each other. Remarkably, they were all eventually shown to be equivalent in the sense that any one could be made to behave like the others. Today, the best known of these are the Turing Machine, of the British mathematician Alan Turing (not to be confused with his touring machine, the bicycle of which he was so fond), and the Lambda Calculus, of the American logician Alonzo Church (1941). The Turing machine is reflected in the Von Neumann machine which describes the general form of most computing hardware today. The Lambda calculus is reflected in the programming language Lisp and its relatives which are called "functional" or "applicative" languages.

The Turing machine is based on the idea of a tape of unbounded length, with a head which can move left or right along the tape reading and writing symbols. These symbols can be interpreted as instructions (to move left or right or read or write symbols) but may also be interpreted as data, particularly when it comes time to read the result.

The lambda calculus is based on the more abstract notion of "applying a function". For example we may write y := 2x+3 to describe how to obtain y given x, but suppose we want to describe, in the abstract, what it is we are doing to x, so that we can do it to other things. We might make up a name for it, say "DoubleAndAddThree" or just "f", and write f(a) = 2a+3 to describe what we mean. But this is all rather indirect and it would be a nuisance to have to keep making up new names and remembering what they meant. Church used the greek letter lambda and a dot and showed that we could simply write λa.2a+3 as a name for the function.
...

[Vayutuvan]

Came across David McKay (I did know of his research before) while conducting cursory research on Occam's Razor.

https://en.wikipedia.org/wiki/David_J._C._MacKay

In 2003, his book Information Theory, Inference, and Learning Algorithms[29] was published. (Ed: It is available online)
...

Link to "Information Theory, Inference, and Learning Algorithms" is https://www.inference.org.uk/mackay/itila/book.html. I gave it a quick scan. He has a lucid style. End of the chapter exercises are ranked in difficulty similar to Knuth's TAoCP. Some solutions are provided.