Komorebi MethodologyReading edition

A scientific method for mathematics?

Reading tools
Reading library
Switch work

Saved reading

Read side by side

Start reading

Resources & source

Read and explore

Proofs and implementation

About this work

Original TeX with line links · Download TeX

The wording and mathematics follow the retained manuscript. This reading format does not add a proof review or extend Lean coverage.

Skip contents and start reading

9 A scientific method for mathematics?

There is a serious sense in which this is a scientific method for mathematical inquiry. It begins with questions, forms candidate explanations, designs discriminating tests, records failure, revises representations, and demands evidence that can be inspected by someone other than the discoverer. It also requires a limit on the analogy. The final justification of an abstract theorem is not the same kind of achievement as the experimental confirmation of a physical model.

For a universal mathematical claim, a valid counterexample is decisive. Successful tests on many inputs are not generally decisive in the opposite direction. They may justify further investigation or reveal the correct statement, but they do not supply the missing universal deduction. A computation can nevertheless be a complete proof of a finite claim, and a finite computation can complete an unbounded theorem when a proved reduction makes it exhaustive. The relevant distinction is logical coverage, not whether a computer was used.

An existing conversation, a particular synthesis

Pólya's How to Solve It places the activity of finding a solution beside the presentation of a finished one. Its questions encourage the solver to understand the task, seek related problems, examine a plan, and reconsider the result. The heuristic tradition is already concerned with making discovery teachable without pretending that useful advice guarantees success.[4]

Lakatos's Proofs and Refutations studies how conjectures and proposed proofs develop under criticism. Counterexamples can expose weaknesses in a statement or in the concepts used to formulate it, making revision part of mathematical development rather than merely an interruption. This provides an important precedent for treating failed arguments as sources of sharper mathematics.[5]

Experimental mathematics contributes methods for turning computation into an active instrument of inquiry. Formal verification contributes an exact language in which specified claims can be checked. Neither practice is invented by Komorebi. The methodological proposal is to connect them to a mathematical account of realization, preservation, obstruction, repair, and the retained field surrounding a proof.[6], [7]

The contribution should be assessed at these connections. Does a change of realization carry a proved interpretation? Does the obstruction identify the exact admissible correction problem? Does a refinement preserve the original task? Can a certificate be traced to the statement in the manuscript? Does the archive preserve a construction another inquiry can actually use? A shared vocabulary matters when it makes these connections easier to establish and harder to fake.

The intended gain is cumulative. A correction lemma proved for a specified class of maps becomes available wherever that class is realized. A preserved obstruction rules out the same inadmissible repair in another setting. A formal correspondence prevents a translation from silently changing the target. These are concrete ways in which one inquiry can reduce the work of the next. The methodology asks that this transfer be exhibited, not merely described as unification.

There is no need to present the synthesis as a replacement for the rest of mathematics. A calculus earns its place by organizing relationships productively. Classical reconstructions can demonstrate breadth and coherence. New theorems, sharper reductions, and informative impossibility results can demonstrate further reach. The methodological argument is strongest when both are visible and neither is mistaken for the other.

A research cycle, not an automatic theorem-producing pipeline. A candidate realization can lead to a construction, an obstruction, or a revised question. Certification governs which claims may enter the reusable mathematical record.
Figure 3. A research cycle, not an automatic theorem-producing pipeline. A candidate realization can lead to a construction, an obstruction, or a revised question. Certification governs which claims may enter the reusable mathematical record.

View full-size figure (new tab)

The method must also be answerable to evidence

Whether this workflow improves mathematical research is itself a testable question. The validity of the displayed identities does not answer it. Neither does the existence of a substantial research collection. Those establish ingredients and examples. A claim of practical advantage requires a comparison designed to reveal both benefits and costs.

A credible evaluation would declare its tasks before selecting successes. One comparison could give two groups the same tools, starting material, and resource budget. One group would retain its ordinary working notes. The other would also maintain explicit realization contracts, scoped evidence, and the key failed obligations. Both would then receive a related task whose protected observation or admissible correction has changed. The prediction is specific: the structured record should help researchers identify which old results still apply and which must be revised.

Time spent creating and auditing that record belongs in the cost, not outside it. Tasks should include cases where a conventional method is already efficient. Independent reviewers should assess the resulting claims without being told which workflow produced them. Assignment and order should be controlled where practicable, and failed attempts should remain visible. A further comparison could retain the same source material but remove its dependency links, testing whether the organization adds value beyond simply keeping more notes.

The evaluation should count distinct outcomes separately. A completed theorem, a valid counterexample, and a proved reduction to an unresolved obligation have different meanings. Timeouts are unresolved cases, not zero-cost successes or invisible exclusions. Verification time, source recovery effort, incorrect claims admitted, and useful components transferred to later tasks also matter. An approach that produces fewer proposals but more independently usable results may be better than one that fills an archive rapidly. An approach that adds administrative burden without improving discovery or reliability may be worse.

Independent checking should include the statement, not only the proof file. Failed attempts should remain in the sample. Reused lemmas should be credited for the work they save without counting the same lemma as a new discovery each time. A small successful study would support a claim about its task family, not about all mathematics. The protocol should be capable of showing that some parts of the methodology help and others do not.

This is the point at which the scientific analogy becomes strongest. The method contains mathematical components that can be proved sound within explicit hypotheses, and practical claims that can be tested against alternatives. Those two forms of accountability reinforce one another. A sound calculus with poor search procedures may be difficult to use. An efficient search procedure without reliable certification may produce little durable knowledge.

The proposal is therefore not a single recipe imposed on all discovery. It is a discipline for exposing the objects, choices, and obligations through which discovery proceeds. It asks that successful transformations become reusable mathematics and that unsuccessful ones leave more than an anecdote. Its ambition is to make discoveries accumulate as usable structure, rather than only as isolated answers.

Source and conversion record

Source SHA-256: 525944d3003bfb588248e92c85c0c5b43eeac69be6c2d44d7d38a2f168606f1f

Unsupported prose commands stop the build. The mathematical expression sequence is checked against the source, with manuscript macros expanded for display.

Conversion records

Notation in Komorebi Methodology

Look up a symbol without leaving this chapter. Select text before opening help to search for it.

Search this work’s notation.

    Symbols can have different meanings in different passages. Read each result in its own context.

    Open the full notation index