ProveCalc: The LLM Never Computes
The model may explain the math. The math engine owns the answer.
Chapter 24 - ProveCalc: The LLM Never Computes
Part: VI - AI-Native Case Studies From The Mnehmos Ecosystem
Thesis
Engineering calculation software is a domain where model arithmetic errors can cause real harm. ProveCalc solves this by enforcing a hard boundary: the model explains and interprets, the deterministic engine computes. The answer always comes from the engine.
Key Line
The model may explain the math. The math engine owns the answer.
The Problem With LLM Arithmetic
This part of the book is six case studies. Each one sits in a different domain: numeric computation, tabletop rules, chess, civic narration, generated video, and the infrastructure that carries constraints across all of them. Every chapter in this part closes with the same eleven-question architecture card, so the systems can be compared directly against each other. The answers change because the domains change. Introduction II’s claim does not: the model creates possibilities, and something outside the model decides which possibilities belong.
Models can perform arithmetic. They can also get it wrong.
A model can describe Bernoulli’s equation, set up a pipe flow problem, explain the assumptions, and produce a numerical answer. That answer may be correct. It may also be wrong by a factor of ten, with units silently mismatched, and with the error invisible until someone uses the result.
Engineering calculations are not a domain where close enough works. A pipe pressure calculation that is twelve percent wrong is not a useful answer. It is a liability.
The obvious solution is to route numerical computation away from the model entirely.
The ProveCalc Architecture
ProveCalc is a desktop engineering calculation app that makes the boundary explicit by design.
The model handles:
- Interpreting the user’s calculation intent in natural language.
- Explaining which formula applies and why.
- Describing assumptions and naming where they come from.
- Walking the user through what the inputs mean.
- Generating a human-readable explanation of the result.
The engine handles:
- Every numerical operation.
- Unit consistency checks.
- Constraint validation.
- The actual computed result.
The model never runs the math. It describes the math. The engine runs it.
Two Lanes With A Hard Boundary
The key design decision is that the proposal lane and the computation lane do not share a result.
The model can propose a calculation structure: “this is a pipe flow problem, we need to apply the Darcy-Weisbach equation, and we need values for pipe diameter, flow velocity, and friction factor.” That proposal is useful. It frames the problem, identifies the formula, and names the inputs.
But the model’s answer to “what is the result?” is not the answer.
The result comes from evaluating the formula deterministically, with validated units, against the confirmed input values.
If the model’s explanation and the engine’s answer diverge, the engine is right. There is no workflow in which the model’s arithmetic overrides the computed result.
Hallucination can exist in the proposal lane.
It cannot exist in the answer lane.
The engine is not a second opinion. It is the source of truth for the number. The model’s explanation, however fluent, stays a proposal until the engine agrees with it.
The Assumption Ledger
Engineering calculations depend on assumptions. Some assumptions are explicit. Many are not.
ProveCalc tracks assumptions explicitly: what values were assumed, what sources they came from, and what range of values would change the output meaningfully.
The model can propose an assumption. The assumption ledger records it. The user sees it. The user confirms or changes it.
This removes a category of silent error: the model assuming a value, the user not noticing, and the calculation proceeding on an unexamined premise.
Every assumption that enters the calculation is a record, not a hidden variable.
The ledger does double duty. It is specification, because a confirmed assumption becomes an input that later steps read directly, instead of a detail the model has to remember and restate correctly from earlier in the conversation. It is also durable state, because it persists after the session ends and outlives the chat log that produced it. Neither role belongs to the conversation. An assumption that exists only as something the model said forty messages ago is not an assumption. It is a hope that the context window kept it in view.
The Audit Trail
Every calculation produces a traceable record: inputs, formula, assumed values, unit conversions applied, and computed result.
This serves two purposes.
First, reproducibility. Another engineer can follow the same path and arrive at the same result without relying on the model conversation.
Second, accountability. If a result is used in a downstream decision and later questioned, the calculation can be reconstructed. The answer does not live in a chat log. It lives in a structured record that names every step.
Control Mapping
| Risk | Control |
|---|---|
| Model arithmetic error | Deterministic solver owns all computation |
| Hidden unit mismatch | Unit library validates consistency before evaluation |
| Unstated assumption | Assumption ledger captures and exposes all premises |
| False explanation | Audit trail separates explanation from computation |
| Incorrect formula selection | User confirms formula before engine evaluates |
Chapter 10 treats verifiers directly. The deterministic solver here is that chapter’s argument, built once, for one domain.
What This Teaches
ProveCalc is the cleanest version of the core doctrine in this book.
Trust AI to propose. Let the model explain, frame, interpret, and describe.
Verify before commit. Let the engine compute, validate, and produce the answer.
The model is useful in the proposal lane. In a domain where the answer matters, the model cannot own the answer.
The architecture makes that principle structural.
The model cannot produce a wrong engineering answer because the model does not produce the engineering answer.
That is not a limitation of the model. It is a design decision about which lane owns what.
The boundary has an edge worth naming. The engine can prove the arithmetic is correct once a formula is chosen. It cannot prove the formula was the right one for the physical situation it was chosen to describe. If a user waves through a pipe-flow question modeled as laminar when the real flow is turbulent, the unit system stays satisfied and the number is still wrong. That check has not been converted into an engineering control. It depends on the user’s domain judgment at the confirmation step, and naming that dependency is more honest than pretending the boundary covers everything.
Practical Artifact - Computation Boundary Checklist
Use this checklist when an AI-assisted workflow includes numerical outputs or consequential decisions.
| Question | What it protects |
|---|---|
| Does the model produce the final numerical result, or does a deterministic system? | Prevents arithmetic hallucination from entering outputs |
| Are units validated before the computation runs? | Prevents silent unit mismatch errors |
| Are assumptions made explicit and user-confirmed? | Prevents hidden premise errors |
| Is there an audit trail linking inputs to result? | Enables reproducibility and review |
| Can the computation be re-run without the model conversation? | Prevents chat-log dependency |
| If the model’s explanation and the engine’s result disagree, which one is used? | Forces clarity about which lane owns the answer |
The computation boundary is not just for engineering software. Any workflow where the model produces a number that a person or system will act on deserves a version of this design.
Practical Artifact - Architecture Card
The same eleven questions this part asks of every system, answered for ProveCalc.
| Field | ProveCalc |
|---|---|
| Model may propose or interpret | Problem framing, formula choice, assumption values, plain-language explanation of the result |
| Source of truth | The deterministic solver and unit system |
| Assumed model capability | Recognizing the calculation domain, naming the applicable formula, explaining it in plain language |
| Specification (ex ante) | The user’s problem statement, the assumption ledger’s already-confirmed entries, the formula library |
| Verifier (ex post) | Unit consistency checker, constraint validator, the solver’s own evaluation |
| Durable state | The assumption ledger and audit trail, not the chat log |
| Commit boundary | The engine evaluates the formula against validated units and confirmed inputs and records the result |
| Randomness & reproducibility owner | None needed; the solver is fully deterministic, so identical inputs always produce an identical result |
| After rejection | A unit mismatch or unconfirmed assumption blocks evaluation; no result is produced until it is resolved |
| Trace preserved | Inputs, formula, assumed values, unit conversions, and the computed result, reconstructable without the model |
| Escape metric | Any number reaching a downstream decision that did not pass through the solver and unit checker |