>The logical calculus is easier to execute than any of the techniques of mathematics itself, yet only in 1934 did Gerhard Gentzen set it out in a natural way. Even now, mathematics students are expected to learn complicated (epsilon, delta)-proois in analysis with no help in understanding the logical structure of the arguments. Examiners fully deserve the garbage that they get in return.
With an opening like that how can I not read the rest of the book?
This actually touches on some work I've been doing the past week - arbitrary term rewriting to test how reliable a given LLM is when it needs to reason about symbolic manipulation. Everything is dynamically generated to avoid the usual problem of memorising every validation set every llm seems to suffer from.