The trick usually comes before the proof. That is not how most AI demos are staged, of course. The demo asks a model a difficult question, the model produces a long answer, and everyone pretends length is evidence of thought. Mathematics is less polite. A proof can be long, fluent, and wrong. It can also be short because the solver noticed the one move that makes the rest almost mechanical. ...
Cost is usually where AI miracles become accounting problems. A frontier model can look brilliant when it is allowed to spend enormous inference compute, rely on undisclosed training data, and hide the machinery behind a clean demo. Very convenient. Also very hard to reproduce. For businesses, that matters because a capability that cannot be inspected, budgeted, or adapted is not really a capability. It is a vendor promise with a nice interface. ...
When Less Proves More: The Case for Minimalist AI Theorem Provers Proof is a good place to test AI humility. In ordinary business writing, a model can sound confident, cite familiar patterns, and still be quietly wrong. The error may not surface until the contract is signed, the policy memo is circulated, or the spreadsheet has already acquired the authority of a sacred object. In formal theorem proving, the arrangement is less polite. The model writes code. Lean compiles it. The compiler either accepts the proof or sends it back covered in red ink. ...
A theorem prover is a terrible place to let an LLM improvise Code review is forgiving compared with theorem proving. In ordinary software, a language model can produce code that looks clean, passes a few tests, and still hides a slow-burning defect somewhere behind an edge case. Annoying, yes. Catastrophic, sometimes. But the social contract is familiar: tests catch some errors, humans catch others, production catches the rest. Very elegant. Very modern. Very expensive. ...