Three Existence Proofs in One Month = 0?

This October has produced an unusual run of existence results. A finite-time singularity for the Navier–Stokes equations under a particular force. A rigorous construction of certain four-dimensional quantum field theories, including quantum chromodynamics. And, on a far smaller scale, I was reminded this week that a minimiser for the charge-density model I work on exists as soon as one keeps the interface term the theory already carries — compactness in the space of functions of bounded variation, lower semicontinuity, done in a line.

All three are real theorems. Not one of them tells you anything about matter.

The singularity result says nothing about the drag on a wing. The construction of QCD says nothing about why helium-4 binds by 28.3 MeV. And my minimiser says nothing about where the interface sits, what shape the cell takes, or what the energy is. In each case the information content about the physical world is zero, and that is not a criticism of the proofs. It is what existence proofs are.

Why Pure Existence Is Cheap

An existence theorem is a statement about a space of possibilities, not about a configuration. The direct method of the calculus of variations wants three things: an energy bounded below, enough coercivity that a minimising sequence cannot escape, and lower semicontinuity so that the limit is no worse than the sequence. Supply those and a minimiser exists. You learn that the set of candidates is not empty. You learn nothing whatever about which candidate it is.

And it gets cheaper the moment you are willing to regularise. Add a perimeter penalty and the admissible configurations have bounded boundary measure, so compactness is immediate. Or discretise: a finite grid with a finite set of labellings is a compact finite-dimensional problem, and existence follows by inspection. Both are legitimate, both are standard, and both leave you exactly where you started if what you wanted was a number.

What the Clay Problem Asks, and Why That Is the Wrong Question

The Clay Navier–Stokes problem asks for existence and smoothness of solutions for all time. It is a beautiful question and it is the wrong question for anybody who wants to know how a fluid behaves. A proof either way — smooth forever, or a singularity in finite time — leaves the practising aerodynamicist precisely where they were. It was posed in an idiom in which existence was the frontier, and in that idiom it made sense. The frontier has moved.

What one actually wants from a turbulent flow is a drag, a lift, a mean pressure. And what one wants to know about those is not that they exist but what they are, and how far from the truth the computed value lies.

Constructive Existence

There is a different standard available, and it is not new: compute the solution, and bound the output by a quantity the computation itself produces. Not a solution exists but here is one, and here is how far it is from the truth.

Concretely, for each output of interest one linearises a dual problem about the computed solution, solves it, and evaluates its stability factor; the error in the output is then bounded by the residual weighted by the dual, and the mesh is refined where that product is largest. Two things follow that a pure proof cannot give. The error is *bounded* rather than guessed at by comparing successive meshes and hoping. And adaptivity and error control turn out to be one mechanism rather than two — the quantity that tells you how wrong you are also tells you where to work.

There is a precedent for accepting this as proof, and it is a good one. The four-colour theorem was settled by computation, and the settlement was accepted because the computation was reproducible and its error controlled. That is the whole of the standard.

And it brings a reformulation with it. A problem can be well posed in the quantities that are observable while remaining ill posed in the field that carries them. Mean drag and mean lift for turbulent flow past a bluff body come out to a few per cent on meshes of a few hundred thousand points — small enough for a personal computer, and orders of magnitude coarser than resolving the Kolmogorov scale would require. On those same meshes the pointwise velocity field is not converged and never becomes so. Both facts hold at once. Turbulence stops being the thing that makes fluid mechanics incomputable and becomes the thing that makes the pointwise field irrelevant.

And It Supplies an Object

There is a third thing constructive existence gives, beyond a number and a bound, and it is the one that has actually produced understanding.

A computed solution is an object: a particular flow or a particular charge configuration, held in full, every field at every point, open to being plotted, sectioned, differenced and stared at. An existence proof supplies nothing of the kind. You cannot inspect the QCD vacuum to see why nuclei bind; the construction establishes that the theory is there and leaves you with no configuration to look at.

And inspection is not a figure of speech. The resolution of d'Alembert's paradox and the account of how a wing generates lift were both obtained by looking at computed turbulent solutions — seeing where the instability acted, what it generated, and which part of the surface carried the drag. Both are stated symbolically afterwards, as arguments about stability and about vorticity, not as tables of numbers. The computation did not replace the analysis. It supplied the object the analysis was about.

The same thing happened to me this week in the quantum case, and the parallel is almost verbatim. Asking which part of the cell carries the kinetic energy — the analogue of which part of the surface carries the drag — turned a puzzle into a mechanism. The computed valence density turned out to be flat to within eight per cent across the whole outer region, with its peak not at the ion but interstitially, between ions. A density that flat has almost no gradient, so a kinetic term that charges for variation collects almost nothing from it: the whole kinetic energy is one and a half per cent of the total. And more than half of even that little comes from a region occupying under nine per cent of the volume — the climb out of the depletion at the ion core, which is the only real gradient in the cell.

None of that was derived. It was seen, by plotting the thing and looking, and only then written down. An existence theorem for the same model — which, as noted, takes a line — would have yielded none of it.

The Same Standard in Quantum Mechanics

None of this is special to fluids, and the quantum case makes the point more sharply because the contrast is starker.

For a ground state, pure existence again comes by the direct method and again says nothing. The constructive version is available too, and the mathematics is written down: for nonlinear eigenvalue problems of exactly the kind electronic structure produces, one has a free upper bound from any conforming calculation, a post-processing step that costs one linear solve on a finer space, and an error estimate from the difference. I tried it this week on hydrogen, where the answer is known, and the estimate captured 98 per cent of the true error using nothing exact — while improving the energy by a factor of fifty.

So a properly evaluated calculation does not report a number. It carries a theorem: the energy of the computed state bounds the true minimum from above, and the distance is estimated by a quantity the computation produced.

Against that, consider what computational practice usually reports. Convergence tolerances. *The iteration stopped moving to twelve decimal places.* That is a statement about the solver, not about the distance to the truth, and the two are unrelated: I had a calculation this week that satisfied its constraint to four parts in a thousand billion while being sixty-four per cent wrong. Every tolerance was met. Nothing was true.

What Changes When Deduction Becomes Cheap

If machines can now produce existence proofs at the rate of three in a month, then existence proofs are no longer the scarce good. A proof that an object exists will become something one orders rather than something one celebrates.

What stays scarce is a number with a bound on it. That is not a deduction; it is a construction plus a confrontation with the possibility of being wrong, and no amount of symbolic facility supplies it. Which gives a criterion for where effort is worth spending, and it is not the criterion the fields currently use. A theory that cannot be computed, and whose usable versions carry ingredients tuned to the answer, gains very little from cheap deduction: it will acquire better proofs of its own consistency and better fits to the data, and remain as untested as before. A theory that can be computed, with a bound attached, gains everything — because the one thing now cheap is producing consequences that could turn out wrong.

Pure existence says nothing. Constructive existence says everything. That was true before this month and it will be true after, but it has rarely been so easy to see.

 

OpenAI QCD Existence vs Leibniz and RealQM

 Three Proofs in One Announcement

On 26 October OpenAI announced that its internal models had produced three research results. In mathematics, a proof of the local smoothing conjecture in every dimension, carrying the Kakeya conjecture and Stein's restriction conjecture with it. In computer science, a claimed disproof of the Exponential Time Hypothesis, formalised in Lean. And in physics, a rigorous existence proof for certain four-dimensional quantum field theories — including quantum chromodynamics and a completed Standard Model.

Take the first two seriously. Kakeya has stood since 1917 and has resisted everyone. A disproof of the Exponential Time Hypothesis, if it survives, rearranges complexity theory. These are truths of the kind Leibniz said a machine could produce: consequences drawn from what has already been granted, and now drawn at a level that was not expected this soon.

It is the third one I want to sit with, because of what it does and does not say.

Existence Is Not Computability

A rigorous existence proof for QCD establishes that the theory is a well-defined mathematical object. That is a real achievement and a long-standing open problem. It does not produce the binding energy of a deuteron.

Quantum chromodynamics was written down in 1973. Fifty-three years later there is no lattice calculation that delivers nuclear binding energies at physical quark masses without ingredients fitted to the answer, and the effective field theories used instead carry parameters calibrated on the nuclei they are meant to explain. This is not a controversial reading; it is the ordinary state of the subject, familiar to anyone who works in it.

So after 26 October the position is this. The theory of the strong interaction is — if the proof holds — rigorously proved to exist, and it still cannot tell you why helium-4 binds by 28.3 MeV. Those two facts are entirely compatible, and holding them together is the whole point.

The Same Shape, Again

Readers of this blog will recognise the structure, because it is the one that turns up everywhere once you look for it.

Schrödinger's equation is believed exact for atoms and molecules, and is unsolvable for almost all of them: the wave function of forty-two electrons lives on a 126-dimensional space. What is used instead is density functional theory, which scales — and which requires its user to name an exchange–correlation functional, chosen from several hundred, most of them fitted to measured data. The Navier–Stokes equations are believed exact for ordinary fluids, and resolving turbulence at the Reynolds numbers of an aircraft is beyond any computer that will be built. What is used instead is a turbulence model with constants calibrated against measured flows.

In each case the exact theory is out of computational reach and the practical substitute carries an ingredient supplied by hand. And in each case the consequence is the same: what gets tested is the ingredient, not the theory. When a number disagrees there is a functional to change or a constant to retune; when it agrees, agreement was available by construction.

QCD now joins that list in its purest form. Not we think it is right but cannot check — rather it is "proved" to exist, and still cannot be made to produce the number. Proof of existence removes the last doubt about the object while changing nothing about its silence.

What Leibniz Would Have Said

He drew the line himself, three hundred years ago, and the announcement illustrates it better than any argument could:

• There are truths of reasoning, whose opposite is impossible, which follow from what has already been granted. And there are truths of fact, whose opposite is possible, which must be checked against how the world is. A machine that manipulates symbols correctly can produce every truth of the first kind and none of the second.

Three magnificent truths of reasoning were produced last week. Not one of them weighs a nucleus. The existence proof grants QCD its mathematical standing; whether QCD accounts for the matter in your hand is a different kind of question and no quantity of proving reaches it. The machine did exactly what Leibniz said it could including the part about what it could not. Check out what RealQM says.

Two Cautions, Because They Matter Here

These results are days old and extraordinary, and extraordinary claims in mathematics are settled by the community, not by the announcement. That process has started — there is already a human audit of the proofs circulating, and a paper on what happens to mathematical knowledge when proof-checking becomes free and adjudication becomes the scarce thing.

And formal verification deserves to be understood precisely. Lean establishes that a proof follows from the statements as formalised. It does not establish that the formalisation says what the informal theorem meant. That translation is still human work, it is where the subtle errors live, and it is the reason "verified in Lean" is a strong claim about one thing and silent about another. It is the same distinction as above, one level up: the checker handles the truths of reasoning, and somebody still has to look at the formalisation and judge whether it corresponds.

What Actually Changes

If deduction is becoming cheap — and three results in one announcement suggests it is — then the scarce good is no longer derivation. It is confrontation with fact.

Which gives a criterion for where effort is worth spending, and it is not the one the field currently uses. A theory that cannot be computed outright, and whose practical versions carry ingredients tuned to the answer, gains very little from cheap deduction: it will acquire better proofs of its own consistency and better fits to the data, and remain exactly as untested as before. A theory that can be computed, with nothing left to select, gains enormously — because the one thing now cheap is producing consequences that could turn out wrong.

So the lesson of the QCD proof is not about QCD. It is that proving a theory exists and showing a theory is right are different activities, that machines have just become spectacularly good at the first, and that the second has not moved at all. The bottleneck has shifted, and it has shifted towards the part Leibniz said was ours.

Can AI Understand Textbook Quantum Mechanics? Claude: NO

A Century of Saying Nobody Understands It

Feynman, in the Messenger Lectures: I think I can safely say that nobody understands quantum mechanics. He was not complaining that the formalism was unclear — he could use it better than almost anyone alive. In QED he put the complaint precisely: nobody knows how it can be like that.

He was not alone, and the company is not fringe. Murray Gell-Mann, in 1976: Bohr brainwashed a whole generation of theorists into thinking that the job was done fifty years ago. David Mermin coined shut up and calculate to name the working attitude of the profession, not as praise. Einstein never accepted the theory as complete. Steven Weinberg, at the end of a career spent using it, wrote an essay called The Trouble with Quantum Mechanics. Bohr is widely quoted as saying that anyone not shocked by the theory has not understood it — the sourcing is thin, but the sentiment is certainly his.

So here is a fair question to put to a machine that can now derive, compute and explain: can AI understand quantum mechanics?

Three Things Called Understanding

The question only becomes answerable once understanding is split, because at least three different things go by that name.

Mastery of the formalism. Being able to set up the equation, derive the spectra, get the selection rules right, run the perturbation theory, know which approximation applies where. Nobody has ever lacked this — Feynman least of all.

A coherent picture of what is going on. What happens at a measurement, what the wave function is, why probabilities. This is what nobody has.

Knowing that the description fits the world. Not that it is consistent, but that it corresponds — and knowing how one would find out if it didn't.

An AI stands in a completely different relation to each of the three, and the differences are instructive.

The Formalism: Complete Mastery, and That Is the Trap

On the first, the answer is yes and it is already happening. Textbook quantum mechanics is a well-formed axiomatic system, and deriving consequences from stated premises is exactly what these machines do. Ask one to make sense of the theory and you will get an excellent textbook: cleaner derivations, pedagogical confusions resolved, the angular momentum algebra laid out better than most lecturers manage.

And that is the trap, because it looks like an answer to the second question and is not. Coherence is not correspondence. A machine will make quantum mechanics make more sense without touching whether it is testable, and the fluency of the result is precisely what makes the substitution hard to notice.

The Interpretation: It Cannot Settle It, and Not Through Weakness

On the second question an AI will survey and not settle. It is worth being clear why, because the reason is not that the machine is not clever enough.

The interpretations — Copenhagen, many-worlds, pilot wave, objective collapse, the rest — are not derivable from one another. They differ in what they grant, not in what follows from what is granted. And they are not distinguished by any measurement anyone has been able to make, which is exactly why they have all survived a hundred years. So there is no reasoning to carry out and no fact to check against.

Leibniz drew the relevant line three centuries ago. There are truths of reasoning, whose opposite is impossible, which follow from what has been granted; and truths of fact, whose opposite is possible, which must be checked against how the world is. The interpretive question falls outside both: not settled by reasoning, because the premises differ; not settled by fact, because no observation separates them. Calculemus has nothing to work on.

Which means an honest AI, asked what the wave function is, reports the positions and the arguments and declines. Any machine that appears to settle it is producing fluency. That is worth knowing in advance, because the fluency will be very good.

The Third Question Is the One Nobody Asks

Here the picture changes, because there is a reading of nobody understands quantum mechanics that is not interpretive at all — and on that reading the question is decidable, and a machine can work on it.

The theory is believed exact for atoms and molecules. It is also, for almost everything, not solvable: the wave function of N electrons lives on 3N variables, so benzene's lives on a 126-dimensional space that nothing will ever hold. What is used instead is a method that scales, and every such method carries an ingredient supplied by hand — most often a density functional chosen from several hundred, most of them fitted to measured data.

Now give a machine a precise task instead of a grand one. Not make sense of quantum mechanics, but: trace the chain from this equation is exact for molecules to here is this molecule's energy, and mark every step where something was supplied rather than derived. That is a well-posed question about the structure of a practice. It has an answer that does not depend on who is asking. And the answer is specific: the chain breaks where the equation is replaced by a method whose ingredient was calibrated against measurements of the kind now being predicted. When the number disagrees there is something to retune; when it agrees, agreement was available by construction. The equation itself is never what was tested.

An AI would also report the defence, and should. Fitted is not arbitrary: the hierarchy does converge where it can be run, small systems are checked against exact results, failure modes are catalogued. The honest verdict is that the chain is considerably weaker than advertised, not that it is empty. A machine that was told to find circularity and reported total circularity would be flattering its instructions.

 So: Can It?

Not in Feynman's sense. Nobody can, and quite possibly nothing can, because that sense may not name a decidable question — a century of failing to settle it by either reasoning or observation is some evidence that it isn't one.

But a machine can do the third thing, which nobody has been asking for: hold the entire chain at once — equation, approximation, fitted ingredient, published number, measurement — and say which links are load-bearing. That is not understanding in the romantic sense. It is bookkeeping.

And the uncomfortable possibility worth ending on is that a good share of the century-long sense that nobody understands quantum mechanics has been a bookkeeping problem wearing metaphysical clothes. The mystery of the double slit is real and may be permanent. But the other mystery — that a theory held to be exact cannot say what a molecule's energy is without an ingredient borrowed from the answer — is not metaphysics. It is a consequence of writing the formalism in an object nobody can compute with, and of the questions we then ask of it.

That complaint has the form of a problem rather than a puzzle. Problems can be worked on. And the one thing a machine is unambiguously good for here is telling the two apart.

Here is the answer by Claude: NO

If a machine can't supply understanding, then the only thing it can add is exposure to failure. That's the whole of its contribution. Compute consequences that could come out wrong, fast enough that they actually get checked. Which means that in an age of cheap computation the decisive property of a theory stops being its elegance or even its accuracy, and becomes whether it can be exposed at all. A theory carrying an ingredient tuned to the answer gains nothing from a machine except better tuning — it has no surface for the audit to bite on. A theory with nothing to adjust gains enormously, because the one thing the machine is good at is precisely what such a theory permits.

What about Teaching?

If the teacher confesses to not understand, what can be expected from the student? 

If the teacher claims to understand, the student will be required to understand.

 

Out of Nightmares: RealQM and RealEuler

Two fields, a century apart in their founding equations, have arrived at the same predicament by the same route, and neither seems to have noticed the other.

Quantum chemistry starts from Schrödinger's equation, believed exact for atoms and molecules. The wave function of N electrons is a function of 3N variables, so storing it costs exponentially in the number of electrons. Benzene has forty-two electrons; its wave function lives on a 126-dimensional space and no machine will ever hold it. What is used instead is density functional theory, which scales — and which asks the user to name an exchange–correlation functional before any number appears. There are several hundred, most containing parameters fitted to measured data.

Fluid mechanics starts from the Navier–Stokes equations, believed exact for ordinary fluids. Resolving a turbulent flow down to the Kolmogorov scale at the Reynolds numbers of an aircraft or a ship is beyond any computer that will be built. What is used instead is a turbulence model — RANS, large-eddy simulation, wall functions — each carrying constants calibrated against measured flows.

In both fields the exact equation is out of computational reach, and in both the practical substitute carries an ingredient supplied by hand. The consequence is identical and it is not about accuracy. What gets tested is the ingredient, not the equation. When a calculation disagrees with experiment there is a functional to change or a model constant to retune; when it agrees, agreement was available by construction. The equation is never what failed, because the equation was never evaluated. And a claim that cannot fail cannot be confirmed either: the long record of success belongs to the arrangement, not to nature.

This is not an accusation of bad practice. Both communities do careful work under a real constraint. It is a description of what that constraint does to the epistemic status of the result.

The Uncomputable Object Was the Wrong Thing to Ask For

Here is the move that both programmes make, and it is the same move.

The 3N-dimensional wave function is uncomputable. But nobody measures a wave function. What is measured is an energy, a density, a geometry — and those live in ordinary three-dimensional space. The pointwise velocity field of a turbulent flow is uncomputable. But nobody measures a pointwise velocity field in a turbulent wake. What is measured is a drag, a lift, a mean pressure — and those are averages.

So in both cases the object whose uncomputability blocked everything was never the object anyone needed. It was the object the formalism happened to be written in.

In fluid mechanics this has been made quantitative, and the result deserves to be better known than it is. Mean drag and mean lift for turbulent flow past a bluff body come out to a few per cent on meshes of a few hundred thousand points — small enough to run on a personal computer, and orders of magnitude coarser than a simulation resolving the Kolmogorov scale would need. On those same meshes the pointwise velocity field is not converged, and does not become so however far you refine. Both facts hold at once. The outputs are stable because their stability factor is moderate; the pointwise field is not, because its stability factor is not. We refer to this as RealEuler.

That is not a compromise or a lucky average. It is a reformulation of what wellposedness should mean: a problem is wellposed in the quantities that are observable, and need not be wellposed in the field that carries them. Turbulence stops being the thing that makes fluid mechanics incomputable and becomes the thing that makes the pointwise field irrelevant.

And the Error Is Bounded, Not Hoped For

There is a second difference that matters more than it sounds.

In a fitted framework you cannot bound your error. You can compare two meshes, or two functionals, or two turbulence models, and if they agree you take courage. That is a consistency check, not a bound, and it fails exactly when the ingredient is systematically wrong — which is the case it would need to detect.

The alternative computes the bound. For each output of interest a dual problem is linearised about the computed solution and solved backwards; its stability factor is evaluated; the mesh is refined where the product of residual and dual weight is largest. The error in the output is then bounded by a quantity the computation itself produces. Adaptivity and error control turn out to be one mechanism rather than two. You are told how wrong you are, by the calculation, rather than reassured by a trend.

Nothing in a method carrying a tuned constant can offer this, because the error attributable to the constant is not visible to any mesh refinement.

New Computability, New Results, New Understanding

The reason to care about any of this is that removing the hand-supplied ingredient produces results the fitted frameworks cannot reach, and both programmes have delivered some.

Take the viscosity to zero in a computation with no turbulence model and you do not get potential flow. You get potential flow modified by a three-dimensional rotational separation, and that separation carries drag. That is d'Alembert's paradox resolved — not by boundary layers, but by noticing that the smooth potential solution was never the vanishing-viscosity limit, because the correct limit is turbulent. The same analysis applied to a wing gives lift and drag without a circulation condition imposed by hand: the Kutta condition, which classical aerodynamics must supply, stops being an input and becomes an output.

On the quantum side the analogue is that the coefficients of continuum mechanics — the modulus, the equation of state — follow by differentiating a computed energy, with no averaging over microscales and no ensemble. A quantity that the standard route reaches only through statistical machinery becomes a derivative of one number.

In both cases the result was available only once the hand-supplied ingredient was gone. That is the argument for computability, and it is not an argument about decimal places.

Why There Has Been No Discussion

Both programmes published. Neither prompted much argument. The reasons are worth setting out, because they are structural and not a grievance.

A framework with a fitted ingredient is more convenient, not less. It is analytically tractable, teachable on a blackboard, examinable, and it reproduces measurement by construction. Removing the ingredient offers the practitioner a harder computation and a theory that can now embarrass them. That is a worse deal, and no amount of correctness changes it.

Curricula select for what can be transmitted. Potential flow with circulation, and density functional theory with a named functional, are both teachable in a term. A result obtained by inspecting a computed turbulent solution, or by solving a free-boundary problem in three dimensions, is not a problem sheet.

And displacing an established framework needs a practitioner's grievance, not a refutation. Three things have to coincide: the old framework must visibly fail at something people need, the new one must do something they want, and the textbooks must turn over. Resolving a paradox supplies none of the three. Where both approaches give the same lift coefficient for a cruising wing, nobody has a reason to move.

So the leverage is not in the cases where they agree. It is in the cases where the fitted framework is wrong and known to be wrong — stall and post-stall, three-dimensional separation, unsteady and flapping flight; and on the other side, systems where no functional is reliable and the answer matters. One measured case where the hand-supplied ingredient fails and its absence succeeds would do more than twenty years of correct publication, which is a statement about how fields change rather than about who is right.

The honest request is not that anyone believe this. It is that these are claims which can fail, made in frameworks where failure would be visible, and that is rarer than it should be. They should be tested rather than left alone.

But AI is now transforming traditional education and so opening entirely new possibilities for RealQM and RealFlow. 

AI: After Mathematics, Physics

The machine Leibniz asked for now exists. He wanted a formal language in which any concept could be written down and a mechanical procedure for drawing out the consequences, so that two people who disagreed could stop arguing and say calculemus. Three hundred years later the thing manipulates symbols, derives, writes programs, and produces proofs that proof-checkers accept.

What that does to mathematics is not to end it but to move where the work is. Deriving a consequence from stated premises is the part a machine can do, and now does. What it cannot do is decide which premises are worth stating, or whether a formal description fits the world it claims to describe. Leibniz drew that line himself, in the Monadology: there are truths of reasoning, whose opposite is impossible, which follow from what has already been granted; and truths of fact, whose opposite is possible, which have to be checked against how things are. A machine that manipulates symbols correctly delivers every truth of the first kind and none of the second.

So mathematics has been reframed at every level — in teaching, where the premium shifts from executing procedures to formulating and checking them, and in research, where the bottleneck moves from derivation to judgement. That reframing has largely happened. The interesting question is what is next.

Physics Is Next, and It Is Harder

Physics carries the same division but with an extra burden. A physical theory must not only be internally consistent; it must face measurement. It lives on both sides of Leibniz's line at once: its derivations are truths of reasoning, and its claims about matter are truths of fact.

Which exposes something awkward about the part of physics that touches matter directly. The Schrödinger equation is believed exact for atoms and molecules and is, for almost everything, not solvable. The wave function of N electrons is a function of 3N variables, so the cost of holding it grows exponentially. Benzene has forty-two electrons and a wave function on a 126-dimensional space; no machine that will ever be built can hold it.

What is used instead is a ladder of substitutes. Coupled cluster is the accurate end and scales as the seventh power of system size, which means tens of atoms. Density functional theory reaches thousands of atoms and carries essentially all of computational materials science — but it asks the user to name an exchange–correlation functional first, and there are several hundred, most of them containing parameters fitted to measured data. The accurate end does not scale; the scalable end is fitted.

Read that against Leibniz's distinction and the problem is sharp. When a calculation disagrees with experiment there is always an ingredient to adjust — a functional, a basis, a correction — and when it agrees, agreement was available by construction. So the equation itself is never what is tested. Uncomputability puts it beyond refutation, and what is beyond refutation is equally beyond confirmation. The unbroken record of success is a property of the arrangement, not a finding about nature. This is not an accusation of bad practice; it is the structural position of a theory whose exact content is out of reach.

One Model, With Nothing to Select

RealQM is worth following as the clearest example of the alternative. It represents N electrons by N charge densities on ordinary three-dimensional space, each carrying one unit of charge, occupying regions that do not overlap, with the boundaries between them free and located by minimising the energy. The energy is a localisation term plus the Coulomb energy of the charge configuration, each pair counted once. No antisymmetry, no exchange, no correlation functional. The exclusion principle is not an algebraic condition on a wave function; it is the geometric statement that two electrons do not occupy the same place.

Two consequences matter more than any number it produces.

First, it is computable. Cost grows with the number of electrons and the fineness of the grid, not exponentially. So the same model runs on a hydrogen atom, a water molecule, a crystal, and a protein active site. Not a ladder of methods each valid in its own window — one model, across the range.

Second,  there is nothing to select. Given the nuclear charges and where the nuclei sit, the energy is fully determined. No functional is named, no parameter is chosen per system. And a model with nothing left to choose can be wrong in public: when it disagrees with measurement, there is no ingredient to adjust, so the disagreement is about the model.

That is the reframing. Not a claim to be more accurate than the methods that exist — on absolute energies it is not — but a claim of a different kind, which is that the claims are decidable.

What It Gets Right, and Where It Stops

Being decidable means some of the verdicts go against it, and those are worth stating plainly, because they are the content of a testable theory rather than apologies for it.

Geometry comes out well: structures, bond angles, the direction of forces. Absolute energies carry errors of a few per cent at best. Differences taken within one composition are reliable, because the errors largely cancel; differences taken across compositions are not. The equilibrium coefficients of continuum mechanics follow directly from differentiating a computed energy with no averaging of any kind — a real result, and one the standard route cannot get without an ensemble. Dispersion-bound systems are outside its range. Metals are outside its range too, and for a reason that is now understood rather than guessed: what holds the ions of a metal apart is the pressure of electrons that are mutually orthogonal, and a theory whose exclusion principle is geometric has nothing to generate it with when every neighbour is identical.

A theory that can tell you where it fails, and why, is in a different epistemic position from one that cannot fail anywhere.

Why This Gives Chemistry a New Frame for Biology

The limits just listed look like bad news until you notice where biology actually happens.

Almost nothing in a cell changes composition. A protein changes conformation; a proton moves from one group to another; a substrate binds; a hydrogen-bond network rearranges. Atoms move, and the same atoms are present before and after. That is precisely the regime where this model's errors cancel and its geometry and forces are sound — rearrangement at fixed composition.

Put that together with computability and the frame changes. The question stops being which method can I afford for a system this size, and which parameterisation do I trust for this chemistry? and becomes does the one model hold here? — a question with an answer that does not depend on who is asking. Electronic structure at biological scale becomes something you compute rather than something you approximate your way toward, and the things one wants to know about an enzyme are structural questions about rearrangement, which is the model's strongest ground.

That is the claim worth making, and it is a claim about frames and not about decimal places: one computable model, nothing selected, spanning atoms through chemistry to the molecules of biology, with failures you can name. Whether it survives is a truth of fact, and must be checked. The machine can now do the checking at a rate that makes checking it realistic — which is the whole of why this is the moment to try.

 

AI vs Quantum Mechanics

The Position After a Hundred Years

Schrödinger wrote his equation in 1926. A century later it is still believed exact for atoms and molecules, and it is still unsolvable — not difficult, unsolvable. The wave function for N electrons lives on 3N variables, so the cost of holding it grows exponentially. Helium can be done to many digits. Benzene has forty-two electrons and a wave function on a 126-dimensional space, and no computer that will ever be built can hold it.

What a hundred years has delivered, then, is not solutions but a ladder of substitutes. Coupled cluster is reckoned the gold standard and scales as the seventh power of system size, which means tens of atoms. Density functional theory reaches thousands of atoms and carries essentially all of computational materials science — but before any number comes out you must name an exchange–correlation functional, and there are several hundred, most containing parameters fitted to measured data. The theorem says the exact functional exists. It does not say what it is.

So: the accurate end does not scale, and the scalable end is fitted.Add basis sets, dispersion corrections and pseudopotentials, each calibrated against measurement, and you have the patchwork — a century of careful, honest, indispensable repair work, every piece of it needed because the thing underneath cannot be computed.

This is also why the theory is hard to test. A claim is tested only if it could fail. When a calculation disagrees with experiment there is a functional to change, a basis to enlarge, a correction to add; and when it agrees, agreement was available by construction, because the ingredients were chosen against measurements of the same kind. That is not bad faith. It is the structural position of a theory whose exact content is out of reach.

 First Question: Can AI Clean Up the Patchwork?

Partly — and it is already happening. Neural exchange–correlation functionals exist and fix known failure cases that defeated hand-built ones. Neural-network wave functions go further and skip functionals altogether, using a network as the trial function in a variational calculation: no functional named, a genuine upper bound on the energy, accuracy competitive with the best conventional methods on small systems. Anyone who says machine learning has added nothing here is not looking.

But notice what this does and does not do. It compresses the patchwork. One learned object replaces many hand-crafted ones. What it cannot do is remove the reason the patchwork was needed, because the 3N-dimensional problem is still there and any method that scales is still an ansatz or a functional. A learned functional is fitted — fitted better, on more data, with more care, but fitted. A hundred small fits become one large fit.

And the trade has a cost that is rarely counted. The patchwork is at least legible. Each approximation has a name, a published derivation, a known failure mode, and a user who can say why it was chosen. A neural functional has none of that. You have exchanged a hundred inspectable approximations for one you cannot inspect, and the epistemic position is unchanged: there is still an ingredient standing between the theory and the number, so the theory still cannot fail cleanly.

So the answer to the first question is: AI can tidy the patchwork. It cannot abolish it. Cleaning up is compression, not derivation.

A Different Bet

RealQM wagers differently. Instead of one function on 3N dimensions, it uses N charge densities on ordinary three-dimensional space, each carrying one unit of charge, occupying regions that do not overlap, with the boundaries between them free and located by minimising the energy. The energy is a kinetic localisation term plus the Coulomb energy of the charge configuration, each pair counted once. No antisymmetry, no exchange, no correlation functional. The exclusion principle is not an algebraic condition on a wave function but the geometric statement that two electrons do not occupy the same place.

Whether that is the right physics is precisely the open question. What matters here is that it is a computable question. Cost grows with the number of electrons and the fineness of the grid, not exponentially. Given the nuclear charges and their arrangement, the energy is fully determined: there is nothing left to choose, and so nothing left to adjust when the answer comes out wrong.

Second Question: Can AI Realise the Model?

Here the answer is yes, and for a dull reason that turns out to be the important one.

RealQM's bottleneck has never been ideas. It has been the labour of computing consequences and checking them — building solvers, imposing the right conditions at the free boundaries, running the grid ladders, comparing against exact values and against measurement. That labour is exactly what has become cheap. Constructions that would each have taken weeks now take hours, which means claims can be confirmed and, more usefully, killed at a rate that was not previously available.

The condition is that every claim be pinned to something outside the calculation that produced it: an exact value, a measurement, a halved grid, a number computed by different code. Fluent output is not evidence. But those anchors are available here, and that is not an accident — they are available because the model is computable and has nothing left to choose.

Why the Two Questions Have Different Answers

AI accelerates whatever it is applied to. Applied to a theory whose usable versions are all parameterised, it accelerates parameterisation: better functionals, better surrogates, better fits. That is valuable engineering and it tells you nothing about whether the theory is right, because nothing in it was ever at risk.

Applied to a theory that can be computed outright, it produces verdicts — and some of them will be unfavourable. That is the point, not a drawback.

So AI does not make RealQM correct. It makes RealQM decidable in practice. And a theory that can be decided is worth more than one that cannot, whichever way the decision goes.

Where It Stands

Plainly: the geometry comes out well and the energies not so well. Structures, bond angles and the direction of forces are reliable, which is the regime where atoms merely rearrange. Absolute energies carry errors of a few per cent at best, and differences taken across different compositions are not trustworthy. The equilibrium coefficients of continuum mechanics follow directly from computed energies with no averaging of any kind — a real result, and the thing the model does that the standard route cannot do without an ensemble. Dissipation does not follow at all, and is the open problem.

None of that is settled. All of it is now testable at a rate that makes settling it a realistic prospect rather than a programme for the next generation. After a hundred years of necessary repair work, that is the change worth noticing.

What Would Leibniz Say About AI Mathematics?

Discovery Versus Verification

The emergence of advanced mathematical reasoning in Large Language Models (LLMs) raises a fundamental question:

Is mathematics essentially logical deduction, or is it a creative activity in which logic serves primarily to verify discoveries?

Some 350 years ago Gottfried Wilhelm Leibniz (1646–1716) distinguished between two mathematical activities:

Ars inveniendi — the art of discovery.

Ars judicandi — the art of judgment or verification.

Leibniz wanted to mechanize both. His characteristica universalis was intended as a universal symbolic language, while his calculus ratiocinator would transform reasoning into calculation.

His famous invitation was Calculemus! — Let us calculate!

The Unexpected Route of AI

For centuries, automated mathematical reasoning was pursued through formal logic, from Boole and Frege to Turing and automated theorem proving.

Modern AI has taken a different route.

LLMs were initially trained to predict the next word or token in human language. Yet from this training emerged capabilities for mathematical reasoning, problem-solving and even mathematical discovery.

Why?

Because human language already contains logical structure: implications, negations, quantifiers, analogies and chains of reasoning.

By learning language, including mathematical texts and computer programs, AI acquires reasoning capabilities without being explicitly programmed as a conventional theorem prover.

Mathematical reasoning has emerged, in an important sense, as a byproduct of language modeling.

Discovery Is Not Verification

Formal logic determines whether a conclusion follows from given assumptions. But it does not determine which assumptions to make, which questions to ask or which discoveries are meaningful.

Mathematical creation involves analogy, imagination, experimentation and computation. Logical deduction establishes the validity of proposed conclusions.

Language generates possibilities. Logic tests necessities.

Leibniz might ask: Why should discovery itself not be computational?

Modern AI suggests that it can be, without being reduced to explicitly programmed logical deduction.

Thus two computational activities emerge:

Generative AI → Mathematical Discovery

Formal Logic → Mathematical Verification

Both are computational, but only the second provides a guarantee of logical validity when correctly implemented.

Mathematics Creating Mathematics

The historical irony is remarkable:

Mathematics → Computation → Language Models → Mathematical Reasoning → New Mathematics → Improved Computation → ...

Mathematics has created a computational instrument capable of contributing to its own further development.

Leibniz sought to construct a language for logical reasoning. AI has acquired mathematical reasoning capabilities by learning from existing human language.

Leibniz sought to put logic into language. AI has extracted mathematical reasoning from language.

Perhaps mathematics is not primarily a formal logical enterprise, but a creative, language-like activity whose results can be logically verified.

Leibniz's Calculemus! thus acquires a new meaning:

Let us calculate—not only to establish what is true, but to discover what might be true. 

Mathematics: Creation Versus Verification

The traditional formalist conception identifies mathematics with logical deduction from axioms to theorems.

But this confuses two fundamentally different activities:

Creation: Finding or constructing something mathematically meaningful.

Verification: Establishing that a proposed mathematical statement follows logically from specified assumptions.

Creation involves language, analogy, intuition, computation, experimentation and imagination. Verification involves precise logical rules.

A logical proof can certify a discovery, but it does not explain why the discovery was made or why it matters.

The emergence of mathematical reasoning in LLMs makes this distinction particularly striking.

AI was trained primarily to process language, not to execute a predetermined calculus of formal deduction. Nevertheless, mathematical reasoning emerged among its capabilities.

This suggests that mathematical creation is more closely related to language than to formal logic, while formal logic remains the instrument for certifying mathematical claims.

Leibniz dreamed of turning reasoning into calculation. Modern AI suggests that mathematical reasoning can instead arise from learning language.

The essential distinction is therefore not between human and machine mathematics, but between two functions of mathematics:

Language generates possibilities. Logic tests necessities.

Or, more sharply:

Discovery creates mathematical meaning. Proof certifies mathematical validity.

Mathematics cannot be reduced to either one alone. 

In the Beginning Was the Word: From Genesis to Leibniz to AI

 How Language Became an Instrument of Mathematical Creation

In Genesis 1:3, creation begins with words:

“And God said, Let there be light: and there was light.”

In the opening of the Gospel of John we read:

“In the beginning was the Word.”

The Greek word Logos carries the meanings of word, reason and rational principle.

The biblical vision thus presents language not merely as a means of describing reality but as an instrument of creation.

Some 350 years ago, Gottfried Wilhelm Leibniz (1646–1716) formulated a remarkable mathematical counterpart to this idea: reasoning could be performed through operations on symbols, just as arithmetic could be performed through operations on numbers.

Today, AI is bringing this vision to life by an unexpected route.

Leibniz: Let Us Calculate!

In 1673 Leibniz demonstrated his mechanical calculator, designed to automate arithmetic.

But his greater ambition was to automate reasoning itself.

He envisioned a universal symbolic language, characteristica universalis, together with a calculus ratiocinator in which logical deductions could be carried out by calculation.

His famous invitation was:

Calculemus! — Let us calculate!

Instead of arguing about which conclusions followed from given assumptions, one could calculate the answer.

Leibniz also envisioned an ars inveniendi, an art of discovery, through which new knowledge could be systematically generated.

His ambition was thus not simply to verify known truths but to discover new ones.

The essential idea was revolutionary:

Language, suitably formalized, could become a machine for producing knowledge.

AI: Logic Emerging from Language

The modern AI revolution has taken a surprising route toward Leibniz's dream.

Large Language Models (LLMs) were not originally designed as formal theorem provers. Their fundamental training task was to predict the next word or token in a sequence of language.

Yet from this task emerged increasingly powerful capabilities for logical deduction, mathematical problem-solving, programming and scientific reasoning.

Why?

Because logic is already built into human language.

Words such as if, then, and, or, not, all and some express logical relations. Ordinary language contains innumerable examples of assumptions, implications, contradictions and conclusions.

Consider:

If A implies B, and A is true, then B is true.

This is simultaneously ordinary language and a fundamental rule of formal logic.

An LLM trained on enormous quantities of human language encounters not only words and grammatical structures but also the reasoning expressed through them.

Learning to predict language therefore creates pressure to learn something about its underlying logical and conceptual structure.

Mathematical reasoning can consequently emerge as an acquired capability of language modeling, without the machine having been explicitly programmed with a complete formal system of deduction.

This is the unexpected discovery:

Automated mathematical reasoning has emerged, in an important sense, as a byproduct of automated language processing.

Leibniz's Dream Reversed

Leibniz proposed the route:

Construct a universal symbolic language → Define logical operations → Automate reasoning → Discover new truths.

Modern AI has followed a different route:

Learn human language → Acquire logical reasoning → Generate mathematical arguments → Discover new mathematics.

Leibniz wanted to construct a language for reasoning.

AI has acquired reasoning capabilities by learning from the language humanity had already developed.

Leibniz sought to put logic into language. AI has extracted logic from language.

The historical development is remarkable. Mathematics made computation possible. Computation made AI possible. AI trained on language has now developed capabilities for producing new mathematics.

We obtain a potentially self-reinforcing process:

Mathematics → Computation → Language Models → Mathematical Reasoning → New Mathematics → Improved Computation → ...

Mathematics has produced a computational instrument capable of contributing to its own further development.

Of course, LLM reasoning is not infallible. Generating a convincing mathematical argument is different from proving its validity. Formal verification remains necessary when logical certainty is required.

Nevertheless, the emergence of substantial mathematical reasoning capabilities from language modeling represents a fundamental development.

Genesis Revisited

We can now return to the biblical opening.

In Genesis, the spoken word brings the physical world into existence.

In Leibniz's vision, symbolic language produces logical deductions and mathematical discoveries.

In modern AI, learning human language produces computational capabilities for generating new mathematical knowledge.

These are profoundly different processes, but they share a striking conception:

Language is not merely descriptive. It can also be generative.

The parallel becomes particularly suggestive through the Greek Logos, joining word and reason in a single concept.

What was expressed in Genesis as divine creation through speech, and by Leibniz as the possibility of discovery through symbolic calculation, has acquired a new technological counterpart in AI.

Not creation of physical reality by words, but creation of mathematical knowledge through computational processing of language.

In the Beginning Was the Word

The history of automated reasoning has largely been written as a history of formal logic, from Leibniz through Boole, Frege and Turing to electronic computers and automated theorem proving.

But the breakthrough of modern AI suggests another perspective.

Perhaps the connection between language and reasoning is more fundamental than the traditional separation between linguistic expression and mathematical deduction suggests.

Human language already embodies centuries of accumulated reasoning. LLMs have learned from this enormous intellectual inheritance and developed capabilities that extend beyond reproducing it.

The result is an extraordinary historical circle.

Human reasoning created mathematics. Mathematics created computers. Computers learned human language. And through language, computers acquired the capacity to produce new mathematics.

Three conceptions, separated by millennia, now meet:

Genesis: The Word creates the world.

Leibniz: Symbols generate mathematical reasoning.

AI: Language generates new mathematics.

Perhaps the deepest surprise of the AI revolution is not that machines have learned to calculate or even to reason.

It is that the path to automated mathematical discovery has passed through ordinary human language.

In the beginning was the Word.

And 350 years after Leibniz, the Word has become computational.

AI and the Realization of Leibniz’s 350-Year-Old Dream

From Mechanical Calculation to Mechanical Reasoning, 1673–2026

The AI revolution of 2026 can be viewed as the realization of a remarkable vision formulated 350 years ago by the German mathematician and philosopher Gottfried Wilhelm Leibniz (1646–1716).

Leibniz envisioned two forms of automation:

1. Automated computation: A machine performing arithmetic calculations without human effort.

2. Automated reasoning: A machine performing logical deductions without human intervention.

Leibniz understood that calculation and reasoning are closely related. Both consist of operations performed according to definite rules. If these rules could be expressed symbolically, machines might execute them.

His ambition was nothing less than the mechanization of human intellectual activity.

Today, 350 years later, AI is bringing these two ambitions together.

1. Leibniz's Mechanical Calculator — 1673

In 1673 Leibniz demonstrated a mechanical calculating machine in London, an early version of his Stepped Reckoner, designed to perform addition, subtraction, multiplication and division.

The central innovation was the stepped drum, which allowed repeated arithmetic operations to be executed mechanically.

The machine was limited and mechanically unreliable, but its principle was revolutionary:

Arithmetic could be transferred from the human mind to a machine.

Leibniz also investigated binary arithmetic, recognizing its suitability for representing numbers using only 0 and 1.

Three centuries later, binary arithmetic would become the foundation of electronic computers.

2. Leibniz's Calculus of Reasoning — 1679–1700

Leibniz's second ambition was even more radical.

He proposed a universal symbolic language, characteristica universalis, in which concepts and propositions could be represented precisely.

Combined with a calculus ratiocinator, this would allow logical disputes to be settled by calculation.

His famous imagined invitation was:

Calculemus! — Let us calculate!

Instead of arguing endlessly, two philosophers could sit down and calculate which conclusions followed from their assumptions.

The essential idea was that reasoning, like arithmetic, could be reduced to symbolic operations governed by rules.

Leibniz did not construct a working general reasoning machine. His vision remained largely a philosophical and mathematical program.

But the program survived.

3. The Evolution of Automated Computation and Reasoning

The following milestones trace the convergence of Leibniz's two ambitions.

1673 — Leibniz's mechanical calculator

Arithmetic becomes a mechanical procedure.

1679–1700 — Leibniz's symbolic logic

The vision of automated reasoning is formulated.

1847–1854 — George Boole

Logical propositions become objects of algebraic calculation. Logic acquires a mathematical structure.

1837 — Charles Babbage's Analytical Engine

Charles Babbage designs the Analytical Engine, the first detailed conception of a general-purpose programmable mechanical computer. Unlike earlier calculators performing fixed arithmetic operations, it is designed to execute sequences of operations controlled by punched cards, with separate memory (store) and processing unit (mill).

In 1843 Ada Lovelace describes how the machine could manipulate symbols according to rules, not merely calculate numbers. She recognizes that a machine could operate on mathematical relationships more generally.

The Analytical Engine is never completed, but it establishes the conceptual bridge between Leibniz's mechanical calculator and the modern programmable computer.

The decisive step: From a machine that calculates to a machine that follows a general program.

1879 — Gottlob Frege

Modern predicate logic provides a systematic symbolic language for mathematical reasoning.

1910–1913 — Russell and Whitehead

Principia Mathematica attempts to derive mathematics through formal logical deduction.

1931 — Kurt Gödel

The incompleteness theorems demonstrate fundamental limitations of sufficiently expressive formal systems. Not every mathematical truth can be established within a single consistent, effectively axiomatized system.

1936 — Alan Turing

The universal Turing machine provides a mathematical model of general computation. Turing also proves that no algorithm can decide every mathematical question expressible in a sufficiently general formal language.

1940s — Electronic computers

Mechanical calculation is replaced by electronic computation, making enormous sequences of arithmetic and logical operations practically possible.

1956 — Artificial intelligence

The Dartmouth project establishes AI as a research field, explicitly pursuing the mechanization of aspects of intelligence.

1960s–1980s — Automated theorem proving

Computers begin constructing formal mathematical proofs using logical inference rules.

1970s–2000s — Numerical computation

Computational mathematics transforms science and engineering through numerical solutions of differential equations, optimization and simulation.

1990s–2010s — Machine learning

Computers increasingly learn patterns and procedures from data rather than relying exclusively on explicitly programmed rules.

2017 — Transformers

A new neural-network architecture makes it possible to train powerful models on enormous quantities of language and other structured information.

2022–2025 — Large language models

AI develops increasingly sophisticated capabilities in mathematical reasoning, programming and scientific problem-solving.

2026 — AI mathematical reasoning

Advanced AI systems can produce substantial mathematical arguments, assist with formal verification, construct algorithms and solve selected research problems.

The two ambitions of Leibniz are now converging.

4. The Reunion of Computation and Reasoning

For most of the twentieth century, mathematical computation and mathematical reasoning developed along largely separate paths.

Numerical mathematics used computers to calculate approximate solutions to equations describing physical reality.

Formal mathematics used symbolic logic to derive theorems from axioms.

The former produced numbers and simulations. The latter produced propositions and proofs.

AI is now beginning to bridge this division.

A modern AI system can formulate a mathematical problem, propose a method of solution, construct an algorithm, execute computations using appropriate tools, analyze the results and develop a mathematical argument explaining them.

It can move back and forth between symbolic reasoning and numerical computation.

This is precisely the kind of integration Leibniz anticipated, although the technology is radically different from what he could have imagined.

Importantly, modern AI does not simply follow a fixed list of logical inference rules. Neural language models generate candidate reasoning steps through learned computational structures. Their mathematical conclusions still require verification, whether by proof checking, independent analysis or comparison with computational evidence.

The distinction between producing an argument and establishing its correctness remains essential.

5. Mathematics Improving Mathematics

The development has an intriguing recursive character.

Mathematics made computers possible.

Computers made modern AI possible.

AI is now being used to develop new mathematics, including mathematical methods that can improve computation and AI itself.

Thus we obtain a feedback loop:

Mathematics → Computation → AI → New Mathematics → Improved Computation → Improved AI → ...

The process suggests a new form of mathematical development in which machines are not merely instruments used by mathematicians but increasingly active participants in mathematical discovery.

The speed and ultimate limits of this process remain unknown.

Nevertheless, the possibility of such a feedback loop marks a fundamental change in the relationship between mathematics and computation.

6. What Remains for Human Mathematicians?

Leibniz imagined that machines could relieve human beings of the burden of calculation and routine logical deduction.

He did not imagine that mathematical questions would thereby disappear.

On the contrary, automation could free human intelligence to concentrate on choosing meaningful problems, formulating models of reality and interpreting mathematical results.

This distinction is becoming increasingly important.

If AI can perform much of the technical work of mathematical reasoning and computation, the central human mathematical activity may shift from proving given statements toward deciding:

• Which questions are worth asking?

• Which assumptions adequately describe reality?

• Which mathematical models are meaningful?

• Which computed results can be trusted?

• Which conclusions advance scientific understanding?

These questions cannot be settled by formal deduction alone because they concern the relation between mathematics and the world.

This has profound implications for mathematical education, particularly in science and engineering.

An education centered on mastering procedures that machines can execute may need to give way to one centered on mathematical modeling, computational experimentation, critical verification and scientific understanding.

7. Leibniz's Dream Comes True

In 1673 Leibniz presented a machine that could calculate.

He subsequently envisioned a symbolic system through which machines might also reason.

For 350 years these two ambitions developed through mechanical calculators, symbolic logic, formal mathematics, electronic computers, numerical analysis, automated theorem proving and machine learning.

Today they are meeting in AI.

Leibniz's dream has not been completely realized. General mathematical reasoning remains fallible, and fundamental limits to formal deduction and computation remain.

But the decisive transition is underway:

Machines are no longer restricted to carrying out calculations devised by human mathematicians. They can increasingly participate in devising the mathematics itself.

What Leibniz proposed as a philosophical vision 350 years ago is becoming an operational reality.

The consequences for mathematics, science and education may be as profound as those of the invention of calculus itself.

And perhaps the most remarkable aspect is that the mathematical enterprise has now produced machines capable of extending that very enterprise.

Leibniz's Calculemus has acquired a new meaning: Let us calculate—and let the machine reason with us.