TL;DR
I’m interested in the question: how to build NL-manipulating tools that we can trust? that are reliable?
We couldn’t trust or rely on (symbolic) NLP systems in the 1990s. Performance on harder parts of tasks was patchy, and it was not easy to trace where a particular part of the output came from, or to check why it failed to get some other part. See this summary of my thesis for evidence. We still can’t trust or rely on contemporary LLM-based systems either. Yes, they can do more tricks than 1990s systems, but the criticisms of 1990s systems still apply – possibly even got worse, as the systems have got much more complex, whether as huge matrix networks or systems that use the outputs of those networks in various combinations.
It’s time to move beyond 1950s optimism (or hubris, perhaps), and be more scientific in the engineering of tools that are both reliable and useful. Tools that do not need a permanent disclaimer like: “System XYZ is AI and can make mistakes. Always check output carefully.”
I suggest the way to do this is by taking a wider view, acknowledging the inherent limitations and realities of our abilities to make reliable tools, and respecting the things we can’t change (no matter how much fantasy thinking). Not by building artifacts of increasing complexity and pushing them off cliffs, and hoping they will fly a bit further this time. Or assuming – without good evidence – that they’ll ever reach an acceptable distance. Part of this is strongly top-down thinking, examining the problem we’re trying to solve and the limits and context. Compare to the current bottom-up approach of trying out our favourite approaches and hoping it might get there, which seems to be destined for a loop of adding ever-complex refinements with diminishing returns.
One way forward is not to use the existing tools directly, but make them part of a bigger system which is controlled by a sufficiently powerful proof checker. Checkers like Lean are a good place to start. LLMs and other heuristic tools may suggest answers or directions, but it’s the central checking mechanism which balances the evidence and draws inferences. It makes good engineering sense to separate out the aspects of solutions and get relevant components to handle the bit they do best. Strong proof checking tools will handle the logic side precisely, much stronger than trying to build it in to less reliable tools. And the NL approximations can handle generation of suggestions and plausible leads for the proof checker to try to use.
Read on for the details.
Post-doc: Mathematical Vernacular
As you may have seen in the summary of my thesis, I was somewhat thrown by realising the limits of contemporary NLP work in the 1990s and what I could look forward to, if nothing changed.
At the time (late 1990s), I was very fortunate as a post-doc to join a project looking at “mathematical vernacular” – the semi-formal language used in maths texts, with a view to formalising some of the semantics and possibly building a system to process such texts in a reliable way. (I thank Prof. Luo and colleagues for this great opportunity.)
This was an excellent fit for me. Firstly, it was a deep study of restricted natural language, but also an application area which required reliable tools, and it gave me a chance to work with cutting-edge logics, something I was also very interested in. It also was a way to explore ideas about reliable language processing in a relatively constrained domain.
The context was in a branch of logic known as “dependent type theory”.
Put simply, there’s a powerful language at the type level, enough to encode detailed mathematical structures and propositions, and a language at the term level where you can infer the types of various combinations of terms, and if the type of a term matches some type, then the term is said to “prove” the proposition represented by the type. Eg transitivity of implication is the type “(A -> B) -> (B -> C) -> (A -> C)” – informally if you can get B from A, and get C from B, then you can get C from A. This proposition is proved with the function “lambda g f x = f (g x)”. Literally, function composition.
This connection between programming and reasoning is no coincidence. Search out material on the Curry-Howard-de Bruijn … metaphor if you want to know more.
This family of logics supports computation and reasoning in the same framework, and it’s an excellent vehicle for developing complex proofs. There was much work in 1990s and 2000s to formalise and proof significant results with the tools that implemented various kinds of type theory. There are also many exciting implications in programming too, especially when you try to utilise the power in the logic for NEW WAYS of programming, rather than as a wrapper around traditional styles of programming. It’s a very fascinating area – lots of places where we can do much better than the ideas inherited from assembly-level coding. (Eg using Booleans effectively means _losing_ the info about why something computes to T or to F, and we can program in a way that avoids this loss.)
One consequence of this overlap is allowing a program and its properties to be created in the SAME framework, as opposed to writing a program in language X and then needing a separate checker or test framework to give evidence the original implementation was ok (and hoping the two match up…). With type theory, it’s even possible to encode key properties in a program’s type itself, so that if that program type checks, then it’s automatically a proof that key properties hold – no further checking needed.
Type theory is effectively (most of) the framework used in the tool “Lean” as developed in 2010s, which has been used for a lot of checking of maths proofs and in verification of software. It has been an important component in recent work by the major AI labs, since it allowed proofs generated by their systems to be filtered and verified – as a kind of oracle on whether some piece of reasoning was correct. It may also have been used to help guide the proof construction, as one use is to flag up holes in the overall arguments; but exact details are scarce at present.
Another example: mathematical induction, also known as structural induction. You probably know the pattern, that by showing P(0) and showing P(n) implies P(n+1), then you can conclude P holds for all n. Notice this reflects the structure of natural numbers, where you have a fixed value 0 and an operation which adds 1 to a number. From these two you can build any natural number, eg Z for 0, (S Z) for 1, (S (S (S (S Z)))) for 4 etc. In the setting of dependent type theory, the idea of mathematical induction is a program which operates on the structure of the input X, and generates a proof of P(X). Literally, run the program and you get the corresponding proof term.
Notice that different implementations handle this process differently. Lean says its sufficient to assemble the pieces and then get the conclusion, so you don’t actually need to run the program. More conventional implementations like Rocq or Adga will run the program as far as it is needed to generate any proof terms it needs. There’s some significant debate in the field on whether the Lean approach (with similar predecessors like HOL) is adequate, or whether you need to check in more detail as in Rocq, Agda etc.
Part of the difference relates to your approach to maths – classical or intuitionistic. Classical maths is what most people use, where you can use the idea of “excluded middle” (EM) as an axiom, so for any proposition P, you can take “P or not-P” as always true without further proof needed. This allows arguments like, if you can’t prove not-P, then P must be true. (It’s slightly more complex than this, eg where excluded middle is a consequence of the underlying axiom of choice (AC), but the key point remains.) Intuitionistic maths rejects this idea, and requires proofs to have a more constructive flavour: to prove something, basically you have to show how to build the thing that exhibits the properties. To prove a for-all, you have to show that the result follows for all inputs. To prove an exists, you have to show how to build something satisfying the property. Proofs here are definitely more like programs, namely you run the proof on the inputs to generate the evidence for the conclusion. Compare to EM, which allows a jump without showing how to compute the answer. Intuitionistic maths is more demanding, and not all proofs in classical maths have a proof yet in intuitionistic maths – some because people haven’t found a computational basis for the proof yet, others because the inferences are just incompatible. But classical maths is easier to work with, hence the explosion of activity around Lean.
Be aware – propositional logic in these kinds of logic is NOT equivalent to Boolean logic. We’re not trying to decide whether a statement maps to a binary T or F as we would in a conventional programming context. Instead, we’re looking to see if we can infer a proposition from the axioms and the inference rules.
Tools for mathematical vernacular
So, we were aiming to use type theory in various ways in the mathematical vernacular project.
One part was as the target logic for formalisation work, what we could be translating texts into – and possibly generating text from. (There were a few bits of work at the time looking at converting proof terms back into natural language, but these were quite formulaic and not too useful in practice.)
Another part concerned the semantics of mathematical vernacular, encoding the common operations and concepts in type theory and drawing inferences. (See also the work by Prof. Aarne Ranta and his group, looking at wider use of type theory in grammar and semantics.)
Thirdly, I was looking at using a proof checker as the core reasoning component of a possible assistant for developing proofs via mathematical vernacular.
I developed my own proof checker for this work. It was a kind of meta implementation of a type theory, containing the core mechanisms at a very basic level, like RISC for type theories, with specific end theories implemented by adding relevant definitions. I also looked at making its control of proof state and context much more flexible, as a way to support more open-ended exploration of ideas (say compared to being more strict about working on packaged theories one at a time).
We also used this implementation for experimentation on novel approaches to subtyping via certain functional operations, rather than just extension of structure as in conventional languages (see this blog post for a summary). This “coercive subtyping” was useful in some of the semantics work, allowing some informality of expression rather spelling everything out in detail.
Now’s a good time to explain how proof checkers for dependent type theories can be used. The core operation of this kind of proof checker is to infer the type of some term, and check if its type matches the type claimed for it. But, we can also use the richness of the language to help users develop complex terms to prove some proposition. Sometimes the user can call certain “tactics” to execute operations on the proof state. Other tactics can fill in the gaps automatically. This makes the tools very powerful (for an expert user – or more recent LLM-using tools).
For example, the transitivity result earlier, “(A -> B) -> (B -> C) -> (A -> C)”. We start by claiming that we can prove it – where proving means to supply or build a term (or program) which has that type. This creates a “proof goal” of type “(A -> B) -> (B -> C) -> (A -> C)”. Now, it could be that we already have this or a close relative already proved in our context, and some tactics could search and find candidate theorems which help with the goal. But for simple implications, a good step is to assume all of the hypotheses and then see if you can reach the conclusion by using the hypotheses. Proof state would then look like this.
f1 : A -> B f2 : B -> C x : A ? : C
So we’ve assumed terms f1 and f2 (which happen to be functions, because their type has form X -> Y), and a value ‘x’ of type A. And we’re trying to build a value of type C. The simplest way is to apply f1 to x, then apply f2 to that. We can suggest a term (f2 (f1 x)), and this would get an exact match. Or we could suggest using just f2, then get a new goal to find a value of type B. Or we could (in some systems) suggest a term “? x”, as something applied to x, and then we’d be looking for a term of type “A -> C”. Most checkers have automatic tactics which try combinations of existing hypotheses and could get this automatically, so we’d not need to pick anything ourselves. The key point is – many options for how to attack the outstanding goals.
We can also use existing theorems and operations to rewrite or simplify the current goals. For example, if trying to prove Z, and there’s a theorem which can provide Z given assumptions X and Y, we can invoke the theorem and then will need to show evidence that prerequisites X and Y are also provable in our current context of assumptions and definitions. Applying theorems like this means we eventually have to justify their use, and can’t omit these justifications.
These tools have been used to prove many serious proofs now. Substantial proofs were appearing in the 1990s, and many more added since. Kevin Hartnett’s book from 2026 “Proof in the Code: How a Truth Machine Is Transforming Math and AI” contains further details of other proofs. Plus, there’s the recent use of Lean in maths proofs released by some of the major AI companies, and apparent developments in the tools for converting text to partial formalisations amenable for these proof tools.
These tools are also somewhat fun too. They are powerful enough to manage complex proofs, and manage all of the fiddly details whilst allowing humans to do the interesting part. It’s quite enjoyable to see complex proofs broken down by applying relevant steps and tactics. Kevin Hartnett’s book explains this well, and a popular intro to Lean is presented as an actual game, the “natural number game” at https://cbirkbeck.github.io/natural_number_game/.
One point worth noting. These proof tools are in the style of “assisted proof”. Namely, a human sets the target then via various tactics they develop the proof term to prove the target proposition (or construction), choosing which theorems to try, or which tactics to use to make progress on the outstanding goals. This is in contrast to (traditional) “automated theorem proving”, which does a fully automatic search of relevant combinations to find a proof of some proposition via use of various principles or axioms. Full automation works for some domains, but other domains still needed a human to direct the proof to regions where simpler automation can take over. Recent AI tools are a kind of hybrid, trying (usually over many iterations) to construct a proof term and/or relevant tactic sequences to prove a proposition – though full details on their operation are not fully public yet?
How to use a proof checker inside a mathematical assistant
We were partly thinking about *non-expert users*, particularly mathematicians or students who prefer to interact via more conventional mathematical vernacular rather than the raw controls of a proof checker (though many Lean users pick up the main ideas very quickly).
We didn’t trust an NL system to accurately translate everything the user said. We wanted the end result to be a proof accepted by a proof checker.
What I envisaged is an imperfect NL front end suggesting changes to the proof state in a checker, and the checker being able to explain in reliable terms to its user what had changed. The proof engine would be the core of the system, and the reliability of the whole application would be guaranteed by the central checking. The system being able to clearly and usefully explain proof state back to the user, to ensure they understood the state and that it matched what the human user expected, this was a key check on how reliable the tool was.
Worth noting that naive transformation of proof terms back to NL text is limited, a bit like AI slop, could be repetitive and hard to spot the key details (if any). Much more important to tailor the output to the level of the user, and users will vary a lot. Experts will be happy with a terse explanation that highlights the non-obvious steps, whereas beginners may need steps spelling out in more detail. It’s also possible that the checker could omit steps that beginnners need to see, eg. some equality which is trivial to compute in the checker but it’s critical for the beginner to see that a proof works because two terms are in fact the same thing. Good output needs as much work as handling of input.
A simple prototype was built, and some example proofs developed; but other things got in the way, not least my transition from post-doc to full time lecturer, and a shift in interest towards the topic of coercive subtyping and programming with dependently typed languages. We did use the checker component – called ‘Plastic’ – in various other work in later years.
I also had a brief look at applying such ideas to legal documents and reasoning. Again, there’s a moderately restricted language in use, and it’s also an application where we need reliability and predictability. Using a central proof checking component would certainly help in this important area, and help to avoid inventing fictitious cases!
What’s this got to do with general applications?
Tools like Lean, Rocq, Agda etc are not just for maths and programming. They are strong tools for use when any reasoning is required, including general NL applications. I suggest the same architecture is applicable in many other areas – proof checker as the core, careful NL output to explain state, and flexible NL input being used to drive the checker.
Instead of us having to check the output, and try to convince the LLM-based tool (or whatever) to do something, it’s now for the NL component to convince the proof checker to update its state (possibly with some harness to interact with the NL component), and we read off what the proof checker has developed.
This is certainly one way to get better reliability and predictability from the combination of tools. It separates out various concerns, and isolates the main application from vaguaries of the NL component. The proof component is much stronger on precise logic and reasoning, and the NL component is used to generate ideas for how to change the proof state, guided by the checker itself.
By linking performance to a strong proof checking component, you also get more control over what the overall system can produce – an alternative approach to so-called “alignment” of the LLM-based component.
You could, I suppose, try to train into the NL component some of the functionality of the proof checker, but this seems a step backwards. We understand proof checkers quite well now, and the technology is quite advanced. It seems much stronger to have the less precise component as a client to this central checking. If we’re serious about reliability and so on.
In more detail, how would this work? Instead of formalising some area of maths, we start formalising relevant knowledge around the NL task. Some people might even describe this as a kind of world model. The logic behind these proof tools is generally strong enough to code up the concepts and relationships we need. We’ve also got the machinery (via dependent types) to embellish the semantics with information about plausibility, incompleteness etc, so can compute with the semantics inside a more general framework for processing of information. As a simple example, we could have extensions for dealing with modalities in language. More complicated, the representations could be extended with combinators to support ideas like intuitionistic fuzzy logic.
True, this kind of encoding is a lot of work, but I suspect that the techniques used in recent maths proofs work for automatic formalisation and encoding of parts of maths can be brought to bear. Clearly, we’d need additional human checking and/or proofs on the quality of the developments. Like with big sections of maths, once it is done, it’s reusable with other applications, so potentially a useful thing to have. There’s no excuse not for not trying.
One last word though. A proof via the proof checkers isn’t an absolute guarantee of correctness. We always need to check the formalisation and the statement of key properties to ensure that we’re proving exactly what we think we’re proving. It’s not great to claim a proof of a big theorem if weaknesses in the formalisation mean you’re only proving something relatively trivial instead.
Last words
I still don’t trust NL systems, either in the 1990s or more recently, knowing in detail how they work and what their limits are, especially since I also know in detail how modern proof checking tools also work, and what their capabilities are.
I am very sceptical that, in the current mode of “generate and test”, of building things then looking to see “are we there yet?”, that we’ll ever get close to the reliability we really want, to a point where we don’t need disclaimers on everything.
Maybe some top-down thinking is required, to acknowledge the difficulties of what we’re trying to do, then pick a framework where we play to our strengths and also work to control the weaknesses.
If we’re serious about it, one option is to have a serious proof checking component as the core of a system, with the less reliable NL parts acting as a client which tries to convince the proof checker to develop its state, and we can report progress by careful rendering of the state of the checker into suitable NL. Strong engineering is about using relevant components to the best of their abilities, and not trying to reinvent the wheel, badly.
Let’s try to get rid of those disclaimers, safely.
