From Minimax to MRI: How the Dual-Track Framework Took Shape

It Was Not There from the Beginning

Looking back at the MRI project now, it is easy to tell it as a complete story: first, category theory suggested the idea of cross-domain transfer; then I built a knowledge map, had AI generate research candidates, and finally made the results stand on “two tracks” through formal proofs and engineering reproduction.

That story broadly fits the method that later emerged, but not the order in which the method emerged.

I did not first design an Auto Research paradigm and then use MRI to carry it out. The dual track gradually became a rule as the project moved forward. An earlier project, Minimax, may have influenced it, but at the time I did not deliberately connect the two projects, and Minimax’s records did not use the name “dual track.”

More importantly, the dual track is not “two different pieces of evidence for the same research conclusion.”

It grew out of a classification of problems: logical problems, engineering problems, and problems that are currently indeterminate or metaphysical. Logical problems are ultimately decided through formalization; engineering problems are ultimately decided through reproducible engineering results. The third category lies outside the scope of this method.

What this article asks is how that classification grew out of two different research experiences.

Minimax: A Result That Kept Shrinking

Minimax began with a simple question: if a certain structural prior is placed in a very small model, can it generalize better despite having very few parameters?

AI and I tried six versions of small models in succession. Some produced attractive numbers on particular training sets or in-distribution tasks, but their advantage was unstable on genuinely unfamiliar data. One structured model achieved higher in-distribution accuracy than an ordinary baseline, yet its performance on an unseen distribution was only about 3%.

Continually changing models did not produce stable results, so the project shifted from machine learning to the computable structure of the I Ching: organizing the 64 hexagrams, 384 lines, and traditional concepts as data, and asking how much variation in the texts those structures could actually explain.

At first, an exciting correlation coefficient appeared: r≈0.28.

It would have been easy to write that number as “the structure explained 28%.” But a correlation coefficient is not an explained proportion, and fitting the same body of material does not equal explanatory power over unseen material. After adding cross-validation that held out whole hexagrams, the explanation rate that could be retained stably narrowed to about 14%.

Later, minimum description length was used to ask a different question: by how much did this positional structure actually shorten the description? The conclusion shrank again: under the data, features, and models used at the time, the compression gain was about 0.06–0.11 bit per line.

It was not zero, but it was also nowhere near as grand as it had first sounded.

In the end, the project did not continue piling on more complex models in pursuit of a positive result. Six model classes and several measurement methods roughly converged on a similar range; the remaining question required another angle, and this path stopped there.

Minimax did not prove an upper bound on the structure of the I Ching. It showed only this: under this body of material and testing protocol, the signal I initially saw did not survive stricter extrapolation except as something limited, real, and very small.

Minimax Had Only One Track

In retrospect, it is tempting to describe Minimax as the predecessor of the dual track: one side generates results, while the other looks for reasons those results may fail. That description is not accurate.

Minimax dealt with engineering problems. Whether a model has generalization ability, or whether a structure can stably explain unseen material, cannot be settled by verbal argument alone. Such questions have to be implemented, run, and leave repeatable results under conditions stated in advance.

Cross-validation, random baselines, and minimum description length were different forms of engineering testing in this project. They changed the measurement conditions and repeatedly tightened the conclusion, but they did not constitute another “formal track.”

The real lesson Minimax left behind was this: an engineering problem is not finished until its result is reproducible. AI can propose hypotheses, choose features, write models, run experiments, and then explain why the results matter; that whole chain can be smooth without substituting for reproducibility.

Looking back, it can be understood as the engineering track I encountered first. But at the time, I had no reason to give it a name composed of “two tracks.”

MRI: When Another Kind of Problem Appeared

I began the MRI project in May 2026.

Its conceptual starting point was my intuitive understanding of category theory: objects are defined not only by their internal components, but also by their relations to other objects; if different fields have similar relational structures, a solution that already exists in one field may be transferable to another.

This may not be a mathematician’s most rigorous account of category theory. It was, first of all, an intuition for generating questions.

I knew nothing about MRI, nor about the mathematics required to complete this project. The first step was not to have AI write a paper directly, but to build a local knowledge map from authoritative textbooks and literature, marking what was known, what remained disputed, and what were merely candidate seams. Textbooks can also be overturned, but without the ability to reconstruct an entire field, they were the current foundation I had to accept first.

Only then did AI begin moving structures from one field to another in search of possible correspondences.

What differed from Minimax was the presence of many logical propositions: whether a conclusion follows from given definitions and assumptions, whether two mathematical objects are equivalent, and under what conditions a theorem holds.

Even if such questions have been tested numerically many times, that does not yield a final decision. A finite number of experiments can only show that a claim has not failed on those samples; it cannot show that it must hold logically.

So another kind of problem, and its corresponding endpoint, appeared. This was not a matter of appending formal validation to an existing engineering claim. It was a matter of sending different problems down different tracks.

Three Kinds of Problems, Two Tracks

The MRI repository was created on May 5. By May 8, the project’s collaboration rules already stated the principle that “the dual track must stand.” Its central sentence at the time was:

Use formalized proofs for logical problems; use reality to prove engineering problems: build it, and obtain the results we expect.

Today, I would state the principle fully as three kinds of problems:

logical problems                 → formalization   → decide whether they hold under stated definitions and assumptions
engineering problems             → reproducibility → build, run, and accept the actual result under stated conditions
currently indeterminate / metaphysical issues → out of scope → not discussed within this method

Only the first two make up the dual track.

This does not require every conclusion to pass both Lean and an experiment, nor does it mean putting two stamps on the same sentence with two tools. A purely logical problem can end with formalization; a purely engineering problem can end with reproducibility.

A research project may of course contain both kinds of problems. But then the task is to split propositions apart, not to mix evidence.

For example, “a given family of phase couplings is unitarily equivalent under given assumptions” is a logical problem and can be assigned to Lean; “after this coupling is implemented, does the simulator produce the expected numerical behavior?” is an engineering problem and requires construction and reproduction. They are related, but they are not two proofs of the same proposition.

As for “does this analogy point to an important discovery?” or “will it ultimately have clinical value?”, if these have not yet been converted into explicit logical propositions or reproducible engineering problems, one cannot pretend that the dual track has already decided them. They can remain as intuitions, directions, or value judgments, but for now they do not enter the category of results that “stand.”

Here, “metaphysical” is not a dismissal of a question’s value, nor a claim that it will be unknowable forever. It is simply a working boundary: questions that currently cannot be given a formal or reproducible endpoint are not adjudicated by this method.

The Dual Track Is Not Lean Plus Python

Lean and Python are merely the tools currently in use; they are not the definition of the dual track.

The object of formalization is a logical problem. It requires definitions, assumptions, and conclusions to be written explicitly in a formal system, after which a mechanical checker decides whether the conclusion really follows. An informal proof can be an intermediate sketch, but it is not the endpoint of this track.

The object of reproducibility is an engineering problem. It requires stating what was built, under what conditions it was run, what result was expected, and how someone else can obtain it again. If the expectation does not appear, the engineering proposition should be overturned or narrowed rather than rescued by explanation.

The level of reality needed for reproduction depends on the claim itself. A claim about a numerical simulator can be reproduced with public code, data, and a stated model; a claim about an actual MRI machine requires a real machine or a phantom; a claim about clinical effects must enter clinical data and the corresponding experiments. A simulation result cannot substitute for clinical validation that one has neither claimed nor completed.

MRI has so far mainly completed formal proofs and engineering reproductions at the level of public models and software. It has no MRI machine, standard phantom, or clinical validation, so the boundary of its results stops there as well.

The Dual Track Can Still Solve the Wrong Problem

Formalization does not turn a textbook into a universal truth, and reproducibility does not turn a single run into an unconditional fact.

The definitions and assumptions in MRI come from the authoritative textbooks, literature, and domain knowledge maps available at the time. What Lean can decide is whether a conclusion holds within those stated definitions and assumptions. It cannot guarantee for me that those premises will never be revised by future domain knowledge.

Engineering reproduction is likewise valid only within the stated model, data, equipment, and conditions. Change the conditions, and the conclusion may change with them.

The more fundamental risk comes before either track begins: if AI or I translate a domain problem incorrectly, the formal system may rigorously prove the wrong problem, and the engineering system may stably reproduce the wrong target.

This is not a third validation track, but a boundary of classification and modeling. The dual track answers, “How should we decide a problem that has already been stated clearly?” It does not answer, “How do we ensure that our initial understanding is the world’s actual problem?”

Correct Can Still Be Meaningless

The dual track also leaves another question unresolved.

A logical proposition can be proved correctly, and an engineering proposition can be reproduced accurately, yet still be trivial, already known, or of no new use to the target field. Some cross-domain transfers in MRI ultimately recovered only familiar condition-number relations; some rigorously valid interfaces still cannot see the null space in underdetermined cases.

They are not false results.

But “true” and “worth continuing to study” are not the same question.

Minimax’s eventual decision to stop adding complexity had already faintly touched this boundary: the presence of a tiny signal does not mean that investing more resources is necessarily worthwhile. After MRI made logical and engineering problems stricter in their respective ways, the issue became even clearer.

Originality, importance, and resource priority belong to research-admission judgment. They determine which questions are worth sending into the dual track, but they are neither a third criterion of truth nor a substitute for the tracks’ endpoints.

That calls for another gate, not another kind of “proof.”

A Method Shaped by the Convergence of Two Experiences

I am still proud of the dual track, but not because any of its components belong to me. Knowledge graphs, cross-validation, random baselines, Lean, and numerical reproduction all existed long before.

In retrospect, Minimax can be placed on the engineering track: build it, and reproduce the result under stated conditions. In MRI, logical propositions appeared in large numbers, and formalization was then explicitly written down as another kind of endpoint.

I cannot prove that Minimax directly caused the dual track in MRI; at the time, I did not consciously link the two. I can only say that, in retrospect, the two experiences happen to converge: the dual track is not a combination of two kinds of evidence, but a classification rule. First determine what kind of problem something is, then give the authority to decide it to the mechanism that matches it; if a problem can currently be neither formalized nor reproduced, honestly leave it outside the boundary.

raise a question
→ decompose a complex problem into subproblems that can be decided separately
→ determine whether each subproblem is logical, engineering, or temporarily undecidable
→ send logical problems to formalization and engineering problems to reproduction
→ treat the way subproblems combine as a new problem, and classify and decide it again
→ declare a higher-level problem to stand within its boundary only after the higher-level proposition itself, its necessary subproblems, and their composition relations have each reached their respective endpoints
→ then use gates of originality and significance to decide whether further investment is worthwhile

The same governance unit can operate on a minimal proposition, or recursively on modules, systems, and a complete research project. Local validity does not automatically imply overall validity, because “how these local parts compose into a whole” must itself re-enter the dual track. The fractal here is not a strict claim in the geometrical sense, but structural self-similarity: whether a problem is reduced or enlarged, the same rules of classification, decision, and composition recur.

Whether this constitutes a new Auto Research method cannot yet be declared by me alone. It needs to be repeated in more fields and compared with other automated research workflows.

But at least in my own research, it has solved a very specific problem: when I enter a completely unfamiliar field and cannot personally review all of AI’s output, I no longer ask any individual to believe the result on my behalf. Large problems can be continuously decomposed, and multiple local parts can advance in parallel, while the question of whether each layer is qualified to recombine is governed by the same basic unit.

I first ask what kind of problem it is, and then require it to reach the endpoint that belongs to it.