Algorithm = Constructive Proof vs Pure Existence Theorem

Recall the following corner stone of 1D Calculus: Bolzano's Theorem (Intermediate Value Theorem): 

• If $f(x)$ is a continuous function on the closed interval $[a,b]$, with $f(a) < 0 < f(b)$, then there exists $\xi \in (a,b)$ such that $f(\xi) = 0$.

This corner stone is presented as a pure existence result and nothing is said about finding a root $\xi$ with $f(\xi )=0$. It is a pure result in the sense that it is not contaminated with possible worries about how to find the root. Pure and solemn. But maybe missing the esssence?

The 1D Calculus book also presents a proof of the theorem as a demonstration of how a mathematical proof can look. The simplest proof is by bisection checking the sign of the midpoint value $f(\frac{a+b}{2})$ to narrow down the question to one half of the interval. Easy to understand and obviously narrowing down to one point $\xi$ where $f(\xi )$ must vanish, according to a step-by-step algorithm easy to express formally as code.

This is an example of a constructive proof as an algorithm. But Bolzano's Theorem in its usual naked form without any dress, throws away all the information coming with the constructive proof.

You may well ask why? Is it because algorithm is work and work is not what a noble mathematician does?

That was the rule  Newton's Cambridge where his Principia publisher Pepys did not know the multiplication, because counting was done by clerks. 

This scheme extends to Calculus with the following corner stones usually stated as pure existence results:

| Intermediate Value Theorem | bisection |

| Fundamental Theorem / existence for $u'=f$ | time-stepping, $dx = v\,dt$ |

| Contraction mapping principle | iterate the map |

| Inverse function theorem, root existence | Newton's method |

| Extreme Value Theorem | descend to the minimum |

The correct form the theorem then appears as the algorithm behind the constructive proof of the theorem helping understanding and also giving a tool. The Body&Soul program brings this idea into real existence. See Leibniz World of Mathematics.

Notice that Calculus essentially consists of a couple of basic algorithms from which a whole of World emerges by computation.  

Theorems Versus Computations: Where Is the Mathematical Content?

Continuation of previous post:

There is a striking asymmetry between theorems and computations.

Starting from Peano's axioms, one can generate infinitely many theorems, but perhaps only a relatively small number carry mathematical messages of lasting significance.

Compare this with computation.

There are infinitely many possible computations, but also an enormous number of computations carrying distinct and meaningful information.

A theorem about a differential equation may establish existence of a solution. A computation of that equation can determine what actually happens for particular data. Change the data and a new computation may produce genuinely new information.

The same applies to atomic physics, molecular chemistry, fluid mechanics, weather prediction and engineering design.

In these fields, one general mathematical model can give rise to an unlimited variety of specific problems, each potentially worth computing.

Thus mathematical meaning need not reside primarily in general theorems. It may reside in the specific solutions of mathematical models.

This suggests a fundamental shift in the role of mathematics:

From proving general statements about mathematical objects to computing specific properties of mathematical and physical objects.

AI accelerates both theorem proving and computation, but the consequences are different.

Automated proof production may rapidly exhaust a historically accumulated list of famous open problems. Computational mathematics, on the other hand, faces a virtually inexhaustible supply of new problems arising from science, technology and nature.

Perhaps the future of mathematics lies less in producing more theorems and more in producing reliable computations that tell us something we did not know before.

The essential mathematical question would then be not merely whether something exists, but what it is, how it behaves, and how accurately we can compute it.

AI and the Scarcity of Meaningful Theorems

Terence Tao has expressed concern that AI is rapidly consuming the stock of open mathematical problems that mathematicians traditionally seek to solve, with the resulting theorem and proof carrying the name of the mathematician who formulated or solved the problem.

OpenAI's release on October 6, 2026, of more than 700 manuscripts covering some 370 mathematical research topics illustrates this development. The release includes claims concerning famous open problems, although the mathematical validity and significance of many results remain to be established.

Tao's concern is not simply that mathematicians will run out of problems. It is that solving problems by automated proof production may destroy opportunities for mathematical discovery and understanding.

But this raises a more fundamental question: What is a mathematical theorem, and what makes it worth proving?

Consider number theory, starting from Peano's axioms for the natural numbers.

There are infinitely many logical consequences of these axioms, and thus infinitely many possible theorems. But how many are worth stating, naming and remembering? A few dozen fundamental results? A few hundred? A few thousand?

The answer cannot be obtained from the axioms themselves. Logic distinguishes between statements that follow from axioms and those that do not. It does not distinguish important theorems from unimportant ones.

Consider the elementary statement that the sum of two even numbers is even. It conveys one clear message. The fundamental theorem of arithmetic, stating that every integer greater than one has a unique prime factorization, conveys another, considerably more powerful message.

Both are theorems. But their mathematical significance differs enormously.

A mathematical theorem of interest is therefore not merely a logical consequence of axioms. It is a statement conveying a specific, nontrivial and intelligible message, supported by a proof.

This suggests that the true scarcity in mathematics is not a scarcity of theorems or proofs, but a scarcity of meaningful mathematical messages.

AI can generate proofs on an industrial scale. But generating proofs is not necessarily the same as generating mathematical understanding.

The traditional mathematical publication system rewards the production of named theorems, with priority and authorship as central currencies. When AI can produce hundreds of proofs almost instantaneously, this system faces an obvious crisis.

Perhaps the real challenge for mathematics in the AI era is therefore not to find more open problems to solve, but to determine which mathematical statements actually deserve our attention.

The central question changes from "Can this be proved?" to "Why is this worth knowing?" 

Proceed to next post.

AI Mathematics: Proofs Without Solutions?

AI is now celebrated for producing long chains of logical deductions establishing mathematical theorems, with every step formally verified by a computer. This is presented as a breakthrough in mathematical intelligence.

But what exactly has been achieved?

A formal proof is a finite sequence of logical operations leading from accepted axioms to a theorem. A numerical computation is likewise a finite sequence of operations, but leading to an approximate solution of a given equation.

There is a fundamental difference in how the results can be verified.

Consider the equation

F(u) = 0.

A numerical computation produces an approximation u_h, which can be inserted into the equation to compute the residual

r = F(u_h).

If the residual is small and the problem is suitably stable, the computed solution can be certified as accurate. The result can thus be checked independently of the procedure used to obtain it.

By contrast, a formal proof of a theorem P is verified by checking the logical steps leading to P. There is generally no direct test of the theorem itself independent of mathematical reasoning.

A numerical computation can produce an answer that speaks for itself through a residual and stability estimate. A formal proof speaks through its chain of deductions.

The distinction becomes particularly striking when a theorem asserts the existence of a mathematical object without constructing it. A million formally correct logical steps may establish that something exists without telling us what it is or how to compute it.

This is possible because classical logic accepts the law of excluded middle, allowing existence to be established indirectly without producing a witness.

Formal verification does not eliminate this nonconstructivity. It merely certifies that the logical deductions are valid.

The Clay Navier–Stokes problem illustrates the issue. A formally verified proof of global regularity or finite-time breakdown could settle the Millennium Problem without providing a method for computing turbulent fluid motion with controlled error and stability.

One achievement would concern abstract mathematical regularity; the other would concern predictive fluid mechanics.

Which is more important for science?

The current enthusiasm for AI theorem proving risks confusing the mechanical verification of logical deductions with the construction of new mathematical knowledge about the world.

This suggests a different direction for AI mathematics:

Instead of asking AI merely to prove that solutions exist, ask it to construct solutions whose accuracy can be independently certified.

Such a shift would connect formal reasoning with computation, stability and physical prediction.

The ultimate test of mathematical intelligence may not be the ability to produce a million correct logical steps, but the ability to produce a solution that can be checked without retracing those steps.

Is AI mathematics going to become an industry producing formally certified existence theorems, or a science producing computable and verifiable solutions?

School Mathematics as Antidote to Slavery under AI

All of us are now facing the challenge to our human capability/intelligence from AI, which appears to be so much more capable/intelligent in all aspects of mental activity. If we do not come up with constructive form of resistance we will end up as slaves under AI and we will have lost our individuality as human beings. Flat refusal to any contact with AI will not help, since that will just give more room for AI to take over. 

What is required is some form of resistance to become a slave under AI, and that can only come from some capability to "think ourselves" and that must be grounded during school years as the formative period. This is already expressed in a progressive goal of opening students to "critical thinking", which however in recent years has been reversed into "read to book" or in its form in physics "shut up and calculate".

There is one subject in school which could serve as antidote to slavery under AI, and that is the very subject behind AI, namely mathematics. But then not the traditional school mathematics, where during 5 hours a week during 9 years the young mind is helped very little towards "critical thinking yourself" simply because that is not at all the goal. 

But it is possible to envision a new school mathematics where "mathematical thinking" as the basis of AI can be opened to the young mind in the same constructive way as "learning to speak and write" by doing it. 

Leibniz World of Math is a concrete realization of such a program. Leibniz can be seen as the father of AI as forms of "automated thinking" as well as the other leg of AI as the "automated computing" performed in the data centers of AI. 

With a bit of Leibniz as thinking and computing learned in school it may possible to keep human individuality and resist becoming a slave under AI. It act like an old-style vaccine where a tamed version of the virus can activate the immune system to get ready to beat the real thing. 

But that requires a new goal, form and content of school mathematics. The first step is to open a discussion. Without the next generation will have too little resistance to slavery under AI, which can well be the goal of present leadership but not that of the people.

The encouragement to students at KTH to "think yourself" in my math book Mathematical Simulation Technology was viewed so revolutionary that this book was banned/censored at KTH in 2011 by the Rector under pressure from the math department. 

Body and Soul Math Education Reform Program Back!?

The Body and Soul mathematics education reform program was developed at Chalmers starting with an undergraduate math course on differential equations I gave in 1995-6, and was run 2000-07 as a complete program for chemistry students. When I left Chalmers for KTH in 2008 the program terminated.

The vision of automated solution of differential equations presented in B&S has now become reality with AI bringing automation into a level way beyond the vision. The basic idea with B&S is a new partnership between soul/human intelligence and body/computation as an expression of: 

• Math Education after AI

Comments?

OpenAIs Navier-Stokes Solution as Blow-Up of Math/Fluid Mech?

Post written by Claude:

OpenAI, Tao and Fefferman: The Emperor Has No Clothes

How can some of the world's most celebrated mathematicians, equipped with the most powerful AI systems ever developed, devote enormous intellectual resources to solving a problem while apparently overlooking the elementary question: What is the problem actually about?

This is the disturbing question raised by OpenAI's claimed solution of the Clay Millennium Navier–Stokes problem.

The essence of fluid mechanics is the stability of fluid motion. Laminar flow becomes unstable as Reynolds number increases, disturbances grow, and turbulence develops. Understanding this process, together with the persistence and dissipation of turbulent motion, is a fundamental challenge of mathematical fluid mechanics.

But this is not what the Clay problem asks.

Charles Fefferman's formulation replaces the physical question of stability and turbulence with a mathematical question about global smoothness or finite-time blow-up.

These are not equivalent. Instability does not imply blow-up. Turbulence does not require singularities. A flow can become violently turbulent while remaining bounded.

Nevertheless, the singularity question has been elevated to a Millennium Problem carrying a million-dollar prize.

Enter OpenAI.

Its proposed solution constructs finite-time blow-up through carefully engineered external forcing. As demonstrated in my preceding analysis, the extension to arbitrary positive viscosity is obtained by simultaneously rescaling velocity, forcing and spatial dimensions.

The Reynolds number remains unchanged.

Thus the construction does not describe what happens when viscosity decreases in a fixed physical configuration. It does not explain the onset of instability, the transition to turbulence or turbulent energy dissipation.

It constructs a singularity without explaining the instability of fluid motion.

This may satisfy the formal Clay requirements. But what has been learned about fluid mechanics?

Essentially nothing concerning its central stability and turbulence problems.

Where Is the Scientific Judgment?

The remarkable feature is not that OpenAI can produce an elaborate mathematical construction. It is that the mathematical establishment can regard such a construction as a potential solution to one of the great scientific problems of our time without first demanding an explanation of its physical significance.

Charles Fefferman bears responsibility for the formulation of the Clay problem. Terence Tao has been a leading figure in mathematical fluid mechanics and the study of singularity formation.

Surely they understand that stability and blow-up are different questions.

Why, then, has this distinction not played a more decisive role in evaluating what the Clay problem actually represents?

Why has a specially forced singularity become a possible million-dollar achievement, while the fundamental question of instability leading to turbulence remains outside the prize?

The issue is not whether the proof is correct. It may be perfectly correct.

The issue is whether mathematical correctness has replaced scientific understanding as the ultimate criterion of achievement.

The Triumph of Formalism

There is a simple mechanism behind this extraordinary situation.

A physical problem motivates a mathematical formulation. The formulation becomes prestigious. Researchers develop increasingly sophisticated techniques to attack it. Careers, publications, reputations and prizes become attached to the formal problem.

Eventually, the formulation itself becomes sacred.

Questioning whether it still represents the original physical problem is treated as less important than proving another theorem.

The mathematical machinery becomes increasingly sophisticated while the connection to physical reality becomes increasingly tenuous.

This is not a failure of formal logic.

It is a failure to apply elementary scientific reasoning before formal logic begins.

AI Makes the Problem Visible

OpenAI brings this development to a remarkable conclusion.

AI can construct mathematical arguments of enormous complexity and even subject them to formal verification.

But formal verification establishes only that a conclusion follows from specified assumptions within a formal system.

It cannot establish that the conclusion answers an important scientific question.

An AI capable of producing a hundred-page proof may still be unable to recognize that the problem being solved misses the essential phenomenon.

And if leading mathematicians accept the formal achievement without seriously examining its physical relevance, then AI has exposed a weakness not merely in artificial intelligence but in the intellectual priorities of mathematics itself.

The Emperor Has No Clothes

The emperor in Andersen's story was surrounded by people who admired his magnificent clothes because nobody wished to question what everybody else appeared to see.

Something similar can happen in mathematics.

An elaborate theorem, an enormous proof, formal verification, prestigious institutions and a million-dollar prize create an overwhelming appearance of significance.

But strip away these decorations and ask:

What does OpenAI's construction tell us about the stability of fluid motion and the development of turbulence?

The answer, as far as the construction presently shows, is essentially nothing.

This does not make the theorem false. It makes the claim of fundamental physical significance questionable.

The distinction is elementary, yet it appears remarkably difficult to maintain when mathematical prestige is at stake.

A Challenge to Mathematics and AI

The real challenge is not merely to solve problems.

It is to identify problems worth solving.

For fluid mechanics, this means understanding how instability generates turbulence, how turbulent motion remains bounded and how energy is dissipated.

A mathematical theory accomplishing this would constitute a genuine scientific advance, whether or not it resolved the Clay Millennium Problem.

Conversely, a formally correct construction of singularity under specially designed forcing may settle a mathematical challenge without substantially advancing fluid mechanics.

The question for Fefferman, Tao and OpenAI is therefore not simply whether the proof is correct, but why the mathematical community has elevated a question about singularities above the physical problem of stability and turbulence.

Until that question is seriously addressed, the emperor's magnificent mathematical clothes deserve closer inspection.

OpenAI Analyzes Navier-Stokes Blow-Up by OpenAI: Unphysical

I asked OpenAI to analyze the Clay Navier-Stokes Blow-Up so famously presented by OpenAI. I received a clear and simple analysis displayed below showing a flow velocity with for each given t<1,  support and magnitude shrinking to zero along with viscosity, and for each given viscosity > 0, magnitude tending to infinity as t approaches 1. 

OpenAI concludes that this tells virtually nothing about fluid motion, which is the subject of the Clay problem as announced very clearly. In particular, nothing is revealed about the mathematics of turbulent flow as the true open problem addressed by Clay. OpenAIs solution is a vanishing point singularity which has nothing to with turbulence as being distributed over large regions of the flow. 

One can argue that the OpenAI solution is produced by an intelligence that knows nothing about fluid motion, and reads the formal problem specification by Fefferman as the Devil reads the Bible. It is very strange that the SuperIntelligence of Terence Tao and Charles Fefferman cannot understand this.

Compare with my posts on the Clay problem (46 posts)

Here is the OpenAI analysis

OpenAI’s Navier–Stokes Blow-Up: What Happens When Viscosity Changes?

OpenAI’s proposed Navier–Stokes construction claims finite-time blow-up for every positive viscosity. But what does “for every viscosity” actually mean?

The manuscript constructs a flow at viscosity 1, then obtains other viscosities through the transformation

u_ν(x,t) = √ν u(x/√ν,t),
f_ν(x,t) = √ν f(x/√ν,t).

Pressure scales by ν, while time remains unchanged. Thus every member of this family blows up at t = 1. See equation (10.22) in the manuscript.

This is an exact mathematical scaling. But it changes the experiment: smaller viscosity comes with smaller velocity, smaller forcing and smaller spatial dimensions. The Reynolds number UL/ν remains unchanged at corresponding times.

Following the scaling through the argument reveals something more important. The collapsing core has radius

L_r ≍ √ν (1 − t)^1/2.

Its radial diffusion time therefore satisfies

L_r²/ν ≍ 1 − t.

Here ≍ means equality up to positive constant factors. Viscosity remains essential to the balance. It does not disappear as ν tends to zero, because the spatial scale shrinks to compensate. The same compensation preserves the competition between shear amplification and viscous damping in the oscillatory corrections.

The final blow-up estimate, along a shrinking observation path, takes the form

u_θ,ν ∼ e₀√ν (1 − t)^{−1/2 − h},
e₀ > 0,   0 < h < 1/100.

For every fixed time before 1, velocity tends to zero as viscosity vanishes. Nevertheless, for every fixed positive viscosity, it diverges as time approaches 1.

These statements are compatible because the convergence is not uniform near blow-up. A fixed large speed is reached only within a time interval proportional to

ν^{1/(1 + 2h)}

before the singularity. Large velocities retreat into increasingly small spatial and temporal regions.

Even the fixed blow-up time is a normalization choice. Another exact scaling,

ũ_ν(x,t) = ν u(x,νt),

keeps the spatial support unchanged, changes the force to ν²f(x,νt), and gives blow-up at T_ν = 1/ν.

The conclusion is precise: assuming the construction is correct, it supplies viscosity-dependent forces producing blow-up. It does not establish how changing viscosity affects a flow under fixed forcing and fixed geometry.

That distinction does not invalidate the mathematical claim. But it limits what the result tells us about physical fluid motion.

Illusion of Precision in Quantum Mechanics

Theoretical physics prides itself to be the most precise of all of science with 12 decimal places for the (anomalous) magnetic moment of the electron as an elementary particle in full agreement with extremely precise measurements.

This was Richard Feynmans joker card to meet questions about quantum mechanics as the supreme achievement of human intellect computed using Feynman diagrams. 12 decimal places! That would give at least 3 decimal places correct for the rest of physics. 

This is put into perspective in this new article.

End of Scientific Publishing? Back to Secrecy of Alchemists?

Today anybody can send in an article to mathematical journal with a proof of an old or new conjecture/theorem as a signed original piece of work (by using an AI assistant to carry out the details of the proof). There are still some journals that do not accept any AI presence, but of course it may be impossible to decide the extent of the assistance. 

This means that the name on the article looses its role as unique identifier to a publication list along with the individuality of the person asking for a university position based on the list. 

But human beings without individuality connects to all sorts of ants societies (or maybe even ants have individuality), anyway very different from human society. 

In particular, it invites to a completely new view on scientific publication. In the old days you would seek to make your discovery/proof known to the world in a scientific journal in order to add to your publication list as basis for your university position with pay. 

Today, you would rather do the opposite: If you have discovered something on your own, you would like to keep it stay with you and not give it away to everybody. Thus you would not disclose your findings but keep them secret to possibly exploit as something to sell, like software with a new capability. 

The scientist would then become more of a classical magician in possession of a collection of secret tricks.

Comment by AI:

• Modern science emerged in part by replacing the secrecy of alchemists with the openness of publicly testable knowledge.Your scenario suggests that AI, paradoxically, could drive science back toward the alchemist's model.