Human and machine in one research process

A human and a machine can participate in the same inquiry without performing identical roles. Either may suggest a representation, locate an analogy, or expose an inconsistency. A formal checker performs a different task from both: it evaluates a precisely encoded derivation under its rules. The collaboration becomes useful when these contributions can be connected without confusing their authority.

The essential separation is between generating a candidate and establishing its status. An idea can be worth pursuing before there is evidence that it is true. A machine may propose many such ideas, and a human may recognize which ones bear on the real difficulty. The direction of assistance can also reverse. What matters is that the resulting claim eventually confronts the same mathematical requirements, regardless of who first proposed it.

Realization Calculus suggests a way to make that confrontation less dependent on persuasive prose. A candidate transformation can declare its input and output types, the questions it preserves, and the defects it introduces. A proposed repair can state its correction space and protected data. A proof obligation can specify which of these assertions has not been established. The object passed between collaborators is then more than an answer. It contains the conditions under which the answer could be used.

There is a substantial possibility here. If a reasoning system can inspect these objects, it can search for a missing comparison map rather than restart an entire problem. It can reuse a proved correction principle where the required hypotheses match. It can recognize that a failed experiment has isolated a narrower question. This is a route toward machine-suited mathematics whose operations remain mathematically legible.

That route does not demand unfamiliar mathematics merely for the sake of unfamiliarity. Reconstructing a classical result in a shared calculus can demonstrate that the language preserves the intended structure and supports reuse. New results within the same language test its capacity to go further. These are complementary contributions. Whether a particular theorem is historically new remains a question about that theorem and its relation to prior work, not about the novelty of every symbol used to state it.

Permalink · Source line 310

The practical danger is not simply that a machine may be wrong. Any collaborator may be wrong. The danger is that the production of plausible claims can outpace the work needed to inspect them. If candidate arguments accumulate faster than their definitions, dependencies, and evidence can be checked, a research program can become larger without becoming more reliable.

A disciplined workflow therefore limits what unverified material is allowed to support. Candidate results may guide exploration, but they do not silently become certified premises. The current research state should make the next unresolved obligation visible. After a substantial revision, the applicable tests and dependent arguments should be revisited. A continuation record should identify an actual restart point rather than merely report that much progress has been made.

This discipline also protects continuity. A new session, a different collaborator, or an external reader should not have to infer the accepted statement from a long conversation. The source artifact, claim map, and scoped evidence should carry that responsibility. Reproducible Python calculations, formal sources, explanatory manuscripts, and visual accounts can provide different views of the same work, provided the correspondences among them are maintained.

For the running example, the durable record is short but specific. The task is to reproduce retained observations of the full evolution from the declared initial state. The failed candidate is iteration of \(A\) alone. The counterexample occurs at the second observation. The replacement is the memory law, with its initial-state hypothesis and induction proof. A later researcher can now change the question intelligently: ask for a shorter memory, a bound on a truncated history, or a sufficient statistic that can be updated cheaply. Keeping only the final matrix product would conceal this direction of inquiry.

An inspectable grammar is not a promise that every problem becomes easy, or that every missing realization can be generated from a finite menu. It is a way to make many important operations composable. Its strength should appear in the quality of those compositions: fewer hidden changes of meaning, more useful reusable components, and sharper accounts of what fails.

Human judgment is not removed from such a process. Choosing a question, recognizing significance, and deciding which representation deserves investigation remain consequential. Nor is machine contribution reduced to transcription. Exploration, construction, formalization, and criticism can all materially change the mathematics. The method should make those changes available for examination rather than resolve the collaboration through a story about which participant deserves all the intelligence.

The strongest account of the work is therefore carried by its artifacts. What was constructed? What was proved? Which incorrect route was rejected, and why? Which result can another researcher now use? Those questions provide a basis for discussing both mathematical achievement and the effectiveness of the collaboration without relying on the volume of generated text as evidence of either.

Permalink · Source line 322