This post answers a claim you have probably heard: that AI cannot really reason. It is written for someone who has used a chatbot, watched it confidently invent things, and drawn a reasonable conclusion from that. The conclusion is right about chatbots and wrong about the field.
Spend an afternoon with a general-purpose chatbot and the claim looks obvious. It invents a citation. It states something false with the same fluency it states something true. If that is your evidence, "AI cannot reason" is a fair reading of it.
The trouble is the word AI. It also covers the software that planned a spacecraft's day in flight, the classifier that organises the medical terminology your hospital runs on, and the tool that proved an operating system kernel always follows its specification. A claim that holds for one of those can be flatly wrong about the others.
The question that has no single answer
"Can AI reason" is built like "can vehicles carry cargo." The only honest response is to ask which one you mean.
Reasoning research split into separate traditions decades ago, and each produces a different kind of guarantee. A proof assistant returns a proof another program can check line by line. A description logic classifier works out how formal definitions relate to one another, which is how large medical vocabularies stay consistent. A planner returns a sequence of actions where every precondition holds. A language model returns text that is likely given its training.
The first three carry a mathematical guarantee attached to the procedure. The fourth carries a tendency to be right, which is something you measure rather than rely on.
What reasoning means when someone is engineering it
Computer science uses a narrow definition. Reasoning is deriving conclusions from premises by rules you can state and check.
Two properties make that testable. Soundness means the procedure never derives anything false from true premises. Completeness means it derives everything that follows, so when a complete program finds nothing, there was nothing to find. Both are theorems, proved about an algorithm or not.
For a description logic reasoner the answer is yes, with a proof. For a language model producing a chain of steps the answer is no, because nothing in the architecture prevents a step that does not follow.
The deployments
Beginning 1999-05-17, NASA's Remote Agent software commanded the Deep Space 1 spacecraft for 29 hours, generating its own activity plans onboard and compensating for four simulated failures without help from the ground. NASA reported it met all its objectives.
It also failed, which is the more useful part. A timing bug left the ion engine on when it should have shut off, because two tasks running at the same time were allowed to interfere. Before flight, the SPIN model checker had found five errors of exactly that class in a neighbouring subsystem. The module that deadlocked was the one that had not been model-checked.
In 2009 Gerwin Klein and twelve colleagues published a machine-checked proof of the seL4 operating system kernel: 8,700 lines of C, 200,000 lines of proof script, about 20 person-years. They proved the implementation always follows its specification, and stated their assumptions plainly: the compiler, the hand-written assembly and the hardware. In a DARPA programme a professional red team spent six weeks trying to break out of one software compartment on a Boeing helicopter in flight, and could not.
In 2003 the Astrée analyser examined 132,000 lines of C in the Airbus A340's flight control software and proved a specific list of failures cannot occur: division by zero, arithmetic overflow, reading past the end of an array. It does not prove the aircraft flies correctly. It proves those failures are impossible across every execution the software could ever have, which is more than testing can establish.
Who did the reasoning
There is a fair objection here. People wrote the seL4 proof, and twenty person-years of human effort went into it. If a person did the reasoning and the machine only checked it, that example proves less than it looks like it proves.
Two things answer it. A 200,000 line proof is far past what any person can verify by reading, so the checker's verdict is the reason anyone trusts the result. And the other examples have a different shape. The Deep Space 1 planner worked out its own action sequences in flight with nobody in the loop, and Astrée is not handed the cases to examine, since finding which executions could fail is the work.
So the field holds both: systems that check human reasoning, and systems that derive conclusions on their own.
Where language models fit
The useful pattern pairs a language model with something that has guarantees. One system proposes an answer and a second checks it, and the checker carries the guarantee. When a model suggests a proof step and a proof assistant verifies it, the resulting proof is correct whether or not anything understood it.
The philosophical objection, which is real
There is a serious position holding that machine reasoning can never be like human reasoning, because understanding requires consciousness that a formal procedure does not have. John Searle argued a version of this in 1980 and answered the standard replies in the same paper. Hubert Dreyfus argued that expert skill is largely not propositional at all, and he was right about the rule-based programmes of his day.
These arguments deserve better than a wave, and they are about a different question from the one facing anyone choosing a system. That question is whether a system produces correct, checkable conclusions at a known error rate, and it has measurable answers. The seL4 proof is valid regardless of what its authors' tools understood. The Airbus analysis either covers those 132,000 lines or it does not.
What to ask
Ask what the output is grounded in, and whether a specific claim can be traced to a specific source.
Ask what the confidence numbers mean. That word covers at least three things: a probability that matches reality, so answers rated 0.8 turn out right about eighty percent of the time; a guarantee about a set of possible answers rather than a single one; or a grade on the source behind the answer. A vendor who cannot say which one applies has not built the thing the number implies.
Ask whether the system can decline to answer. Ask who can override it, which for high-risk uses in Europe is now a legal requirement under Article 14 of the EU AI Act.
The concept bundle
The vocabulary in this post comes as files: twenty-six short concepts in Open Knowledge Format, each a plain Markdown file. Hand the included agent.md to your own assistant and it will place them in your notes, link them to material you already have, and explain each one as you read, without overwriting anything you own. It is also instructed that if you ask whether AI can really reason, it should not answer yes or no. It should ask which system you mean.
Download the concept bundle. Give agent.md to your assistant, or open the readme and do it by hand.
The full research report carries the detail and the citations, including the parts that cut against the argument.
Sources
NASA JPL, Remote Agent Experiment Meets All Objectives, 1999-06-07: https://www.jpl.nasa.gov/news/remote-agent-experiment-meets-all-objectives/
Klaus Havelund et al., Formal Analysis of the Remote Agent Before and After Flight: https://ntrs.nasa.gov/api/citations/20000055731/downloads/20000055731.pdf
Gerwin Klein et al., seL4: Formal Verification of an OS Kernel, SOSP 2009: https://sel4.systems/Info/Docs/seL4-paper-sosp09.pdf
John Searle, Minds, Brains, and Programs, Behavioral and Brain Sciences 3(3), 1980: https://www.law.upenn.edu/live/files/3413-searle-j-minds-brains-and-programs-1980pdf