Bharat Rakshak

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.

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….

Tanaji wrote: ↑14 May 2026 01:03 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.

Tanaji wrote: ↑14 May 2026 03:34 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.

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.