Pure ATPs: such a disappointment

---

I have always had a soft spot for automated theorem provers (ATPs). There is something both elegant and exciting about formalising your nontrivial problem in, say, a predicate calculus variant, then pressing the start-button and letting the machine solve it by the powers of deep deduction alone.

But ATPs have always disappointed. Doug Lenat, who spent his entire life handcrafting the general purpose intelligent system Cyc, commented at the last that they had originally encoded the facts and rules of the world in a Lisp-like formal language and then handed that knowledge base and the user-query to a powerful Resolution Theorem Prover to deduce an answer. To avoid the interminable waiting they added layer after layer of special-case heuristics. After decades of such aggregation they quietly turned off the theorem prover: it was never being used.

Edinburgh university was one of the centres of Prolog use and research in the 1980s, along with Oxford and Imperial College. Undergraduates hated it: the elegance of its specification capability was complemented by the opacity of its execution model. Debugging logic programs by mentally running a depth-first tree-search with backtracking-on-failure - well, that could tax the abstraction-powers of the keenest young minds. 

I was much happier with Lisp: you know where you are with β-reduction.

In the heady days of those applied ATPs known as Expert Systems the slogan was: “In the knowledge lies the power”; inferential capability was distinctly secondary.

The culmination of this insight was the success of the LLMs c. 2024. Enormous amounts of encoded knowledge - and no reasoning ability at all…

And yet, there are still those of us who value the elegance of inference... and now, in 2025, my happiness is complete: those LLMs can now reason!

---

Unusual Reasons

This post is about people who undertake significant life changes, but for unusual reasons.

1. Programming

Dr Hamid Lesan escaped to England from Iran, where, as a dissident, he was under the scrutiny of the Shah’s secret police, the SAVAK. He worked as a colleague of mine at STL in the mid-1980s on formal methods research and AI. I asked him once how he had gotten into programming; he replied that he had first engaged with programming as an interesting application of the lambda calculus.

[Dr Hamid Lesan received his Ph.D. in Mathematical Logic from the Department of Mathematics of the University of Manchester in 1978. After a brief period of teaching, he joined STL in 1980, where his work has been mainly concerned with Formal Methods and Natural Language Processing. He is currently working on tools for supporting the formal specification and development of software in the context of the ESPRIT project RAISE. (ICL Technical Journal, Volume 7 Issue 1 - May 1990). He died in August 2006 - I’m not aware of the circumstances.]

2. Joining the revolutionary left

In the early 1970s, when I was at Warwick University, there was a plethora of far-left organisations looking to recruit: the International Socialists (IS, later SWP); the Socialist Labour League (SLL); the Militant Tendency in the Labour Party; and the International Marxist Group (IMG), British Section of the Fourth International.

It was a time of unrest, and we talked big. Our perspective was becoming a mass revolutionary party as the Bolsheviks had achieved in 1917. Once, one of our leaders, Peter Gowan, came to Warwick to speak. He looked forward to the future mass party, but mentioned that today, most of the leading cadres had elected to join the IMG - rather than other bigger, higher profile organisations - specifically because of its link with the International.

Probably not one in one hundred thousand workers and students had ever heard of the Fourth International: I certainly hadn’t before I was recruited…

3. Being received into the Catholic Church

People join religious organisations for many, often prosaic reasons. But JD Vance joined after an intense study of St. Augustine’s massive City of God. In this fifth century work, Augustine condemns Rome, the City of Men, devoted to present excess, hedonism, selfish ambition and heedless individualism. Vance had no problem identifying those ancient Roman pagans with contemporary American coastal elites with their mindless hedonism; their secular, patronising arrogance.

Augustine counterposes the City of God, the community of those who love God and live according to His will. The Catholic Church is a visible manifestation of the City of God on earth, and promotes the virtues of humility, communitarianism and morality.

JD Vance considered the Catholic Church as the right organisation of resistance: he decided to join.

[St. Augustine wrote "The City of God" over a span of several years, beginning in 413 AD and completing it around 426 AD. This period was during a time of great turmoil in the Roman Empire, particularly marked by the sack of Rome by the Visigoths in 410 AD, which partly inspired Augustine to write the work. The full title of the work is "De Civitate Dei contra Paganos" (The City of God against the Pagans), and it addresses the decline of Rome and defends Christianity against the accusations that it was responsible for the fall of the Empire. (ChatGPT).]

Can you write factorial anonymously? Yes

 

Of course you can. Use the Y-combinator.

This would look cleaner if the author had not used Church numerals. Here's something simpler:

   (λf λn. if n=0 then 1 else n*f(n-1) ) (λf λn. if n=0 then 1 else n*f(n-1)) 6.

But this isn't quite right, since recursion stops after one step. The Y combinator is more devious even than this.

So the factorial function is: Y (λf λn. if n=0 then 1 else n*f(n-1) ).

See section 7 of this PDF for a worked example.

---