What Lean Proved—and What It Did Not

2026-09-05 AI · Research · Formalization

Why I Need Lean

In the MRI project, I faced a very direct dilemma: I do not understand MRI, nor do I understand much of the mathematics involved. The code and proofs were produced mainly by AI. On what grounds should I trust them?

I could, of course, ask one model to review another, or have them debate repeatedly. But if, in the end, a passage of natural language still tells me that “there is no problem with the proof,” I have merely transferred my trust from one model to another.

I could also look for domain experts. At least today, experts remain indispensable for checking whether a problem was translated incorrectly, whether a conclusion already exists, or whether an abstract model leaves out decisive physical conditions. But if Auto Research works, the speed and volume at which AI produces logical propositions may eventually exceed any person’s capacity to read them one by one. Experts cannot forever be the human signatories for every derivation.

What I need is a mechanism that does not require me to pretend that I understand every step, nor require someone else to guarantee all the results on my behalf.

That is where Lean finds its place in the project:

A logical problem does not end when someone finds the proof plausible; it ends when a formal system has completed a mechanical check.

This does not mean Lean understands MRI better than a mathematician does. It does not understand MRI at all. It merely turns the question “does this statement follow from those premises?” from a matter of reading judgment into a check that a small kernel can execute repeatedly.

Lean Checks Formal Objects, Not Papers

Natural-language proofs permit omissions. Authors write “obviously,” “similarly,” or “after a simple calculation,” and readers fill in the intermediate steps with their own knowledge. AI is especially good at producing derivations that appear coherent in this way: every sentence resembles mathematics, yet there may be no genuine logical connection between them.

Lean does not accept appearances.

For a proposition to enter Lean, it must at least be broken down into several things:

definitions: what exactly are the objects under discussion?
assumptions: which premises may be used?
conclusion: exactly which statement is to be proved?
proof term: how is the conclusion constructed from the definitions, assumptions, and existing theorems?

Lean’s kernel checks whether the proof term really has the type required by the target proposition. If the check passes, the derivation is closed within the world that has been formalized.

It has not read the paper’s abstract, nor does it understand what the author “originally meant to say.” Two adjacent sentences in natural language do not become connected automatically in Lean merely because they sound smooth; they must be written as a formal relation.

So formalization does not first make a conclusion grander. It makes it narrower and more specific.

Lean never proves the vague claim that “MRI is like this.” It proves that this exact conclusion holds for the objects defined here, under these explicit assumptions.

A Limited but Genuinely Proved Example

The MRI project studied a set of phase-coupling candidates for multi-shell HARDI.

The initial engineering observation was that, after changing certain phases, spectral metrics from numerical scans appeared unchanged. But no matter how many finite scans were run, they could show only that these configurations had not differed; they could not establish that every permitted phase pattern must behave that way.

The question was therefore recast as a logical proposition: in the project’s defined finite-dimensional sheaf model and this particular family of phase couplings, are candidate E and candidate C related by a unitary transformation, and therefore do they have the same sheaf bandwidth?

Lean ultimately established this restricted conclusion:

For every phase pattern permitted by the formal model, the two candidates have equal sheaf bandwidth.

It advances a numerical observation that found no difference in finitely many cases into a general conclusion within this formal candidate family. Here, “every” does not come from running more samples; it comes from the proof holding for the variables themselves.

But this theorem does not prove that:

It closes one path within a precisely defined family of candidates, not every path in the field of MRI.

That is the power of formalization, and also its boundary: it can pin down a small conclusion very firmly, but it will not quietly expand the conclusion’s range of application for the author.

Which Kind of “Unique Recovery” Is It?

Another example is even easier to misread.

In a finite-dimensional HARDI sampling model, the project formalized a relationship among the vanishing of zeroth cohomology, a sampling operator having a zero kernel, and that sampling operator being injective. Put plainly, in this abstract model, no two distinct coefficient vectors produce exactly the same measurement result.

This can be abbreviated as “unique recovery.”

But if one sees only those two words, it is easy to expand them into “Lean proved that MRI can be recovered uniquely.” That would be wrong.

The finite-dimensional signal space, measurement method, and sampling operator in the formal model have already been defined. What Lean proves here is that the vanishing of zeroth cohomology is exactly equivalent to this sampling operator being injective; the equivalence itself does not assume full rank in advance. Only when separately considering positivity of the sheaf bandwidth and the singular-value ratio are nonzero dimension and a positive minimum singular value needed—that is, the corresponding full-column-rank condition.

None of these theorems proves that a real scanner satisfies the conditions of the formal model, handles every source of noise and model error, or establishes that a finite-dimensional representation contains all information in real tissue.

Still less can one infer from them that a particular clinical scan is necessarily reliable.

The same phrase, “unique recovery,” can sit at entirely different levels of reality:

injectivity in an abstract finite-dimensional operator
≠ stable reconstruction in a numerical implementation
≠ recoverability on a phantom or real machine
≠ effectiveness in a clinical task

Lean ends only the layer among these that has been formalized as a logical problem. If the later layers are to hold, each must in turn be written as an engineering problem and reproduced under its corresponding real-world conditions.

What It Means for lake build to Pass

The project set several hard surface-level standards for the formalization track: lake build must pass, and the code must not leave incomplete proofs through sorry or admit.

sorry and admit can temporarily make Lean accept a proof that has not actually been completed. During exploration, they can serve as placeholders; when declaring that a logical proposition stands, they can no longer remain.

When I reran the current MRI formal library, I did not build only the base framework. I explicitly included the two DWI targets used in this article:

lake build MRI DWI.HARDIBandwidth DWI.HARDIMultiShell

This build completed 8,328 tasks. The output contained one style warning about a line of code exceeding 100 characters, but no proof failures. The project’s Lean source also contains no actual use of sorry, admit, or locally declared axioms.

These checks can show that:

But “zero placeholders” still does not mean “zero premises.” Formal proofs always operate over some set of definitions, axioms, existing theorems, and software implementations. Which axioms a particular theorem depends on still requires inspecting its axiom dependencies; the Lean kernel, compiler, mathlib, and build environment themselves also form a computational foundation that must be trusted and governed.

Formalization does not eliminate trust. It compresses a large body of difficult-to-audit natural-language derivation into a smaller, clearer, repeatedly checkable trusted boundary.

Lean Does Not Check Whether the Written Problem Is the Right One

This is the most important limitation.

Lean is strictly faithful to the definitions actually written into the system—not to the intention in my mind, nor to the MRI world itself.

If AI translates “sampling,” “recoverability,” or “physical correspondence” incorrectly, Lean may still prove the translated proposition perfectly. In that case, the formal derivation has no flaw, yet the research may have gone astray at its first step.

It cannot make at least the following judgments for me.

First, whether the semantics are faithful. Was anything silently substituted as the work moved from natural language to textbook concepts and then to formal definitions?

Second, whether the premises fit reality. Textbooks and papers provide the current foundation of knowledge, not cosmic axioms that will never be revised; ideal conditions added to make something provable may not be met in reality at all.

Third, whether the engineering has actually happened. A theorem cannot substitute for a program being run, much less for experiments on a real machine, a phantom, independent data, or clinical studies.

Fourth, whether the result is novel and important. A theorem can be entirely correct yet be merely an instance of a known conclusion, an unfolding of a definition, or something that changes no prediction or decision.

Fifth, whether the scope of formalization is sufficient. The MRI repository explicitly does not formalize the complete category-theoretic packaging, three physical correspondences, or empirical propositions. Parts that have not entered the formal system do not automatically acquire proofs because a neighboring Lean file passes its build.

Therefore, “Lean-verified” must come with a scope statement. A formalization label without scope may become another rhetorical appeal to authority.

Lean Is Not a Substitute for Domain Experts

If Lean cannot judge semantics and reality, are experts still needed?

They certainly still have value today, but that does not mean every current result must have an expert’s signature as a precondition for standing.

Experts can identify a definition that is internally consistent but does not express the object the field actually cares about; recognize that an allegedly new conclusion is only common knowledge; or point out a physical constraint the model omits. Lean lacks this domain judgment, developed through long practice. The formal propositions and software-layer reproductions currently completed in the MRI project did not depend on experts signing off on each one; experts have a more important role in the semantic review, physical mapping, and final mile into the real world that remain unfinished.

A more scalable division of labor may be this: experts help build and audit semantic interfaces, specify which real-world conditions must enter the model, and sample anomalous and high-risk results; formal systems adjudicate at scale the propositions that have entered the formalization track. People remain responsible for rules, boundaries, value conflicts, and real-world interfaces, rather than pretending they can read every derivation that grows without limit.

Formal systems, too, must be governed. Versions must be pinned, dependencies recorded, axioms audited, and results reevaluated when the verifier changes. One cannot claim that people cannot verify AI item by item while treating the verifier itself as an oracle that can never be wrong.

Lean does not replace “trusting experts” with “trusting software.” Its value is that it separates responsibilities: logical closure is checked by the kernel, semantic correspondence is governed by domain knowledge and specifications, engineering facts come from real-world reproducibility, and value choices are determined by goals and resource constraints.

It Did Not Eliminate My Ignorance; It Layered It

At the start of the MRI project, I wanted to find a boundary: when I cannot personally review all of AI’s output, what can I still guarantee?

Lean’s answer is much narrower—and much more useful—than “AI proved an MRI theorem.”

I can make a narrower claim: a precise proposition has been written into a formal system; under public definitions, assumptions, and dependencies, its proof term has passed mechanical checking. I can also state clearly that the translation from domain language to formal definitions may still be wrong; while some results have been reproduced at the model and software layers, real-world validation at the machine, phantom, and clinical layers has not yet occurred; and originality and significance have not thereby been answered automatically.

This is not complete truth.

It is a map that does not mix different unknowns together:

here, logic is closed
here, semantics still await review
here, some results have been reproduced at the model and software layers
here, evidence from real machines, phantoms, and clinical settings does not yet exist
here, value still requires judgment

For Auto Research, this layering matters more than a single blanket stamp saying “validated.” It allows a system to know which problems have reached their own endpoints, which must remain at the boundary, and which need to be sent to another track or another governance mechanism.

Lean did not prove that I understand MRI, nor did it prove that the MRI project as a whole is correct.

It proved something more modest: in a formal world that has been explicitly written down, we do not treat a statement as a proof merely because it sounds like one.