5 Experiment, conjecture, and proof
On this page · Permalink · Source line 195
Mathematical experimentation is most useful when it asks a question that competing explanations answer differently. More data are not automatically more insight. In the returning-coordinate example, the decisive experiment was not greater precision at the first step. It was a second step. The experiment succeeded because it challenged the assumption that the retained state was sufficient for continuation.
Exact computation is particularly valuable when the phenomenon itself is exact. Integer, rational, and finite-field arithmetic can distinguish a true cancellation from a small floating-point remainder. Symbolic manipulations can expose the invariant behind a numerical pattern. But exactness of the calculation and generality of the conclusion are different matters. A correct computation on finitely many inputs establishes those instances. To establish an unbounded statement, one still needs an argument covering the remaining cases, or a proved reduction showing that the finite cases are exhaustive.
The tradition of experimental mathematics has long treated computation as an instrument for discovering patterns, rejecting conjectures, and identifying routes to proof. Bailey and Borwein describe this active role explicitly. The Komorebi approach belongs in that tradition, while emphasizing the representation and obstruction structure carried from one experiment to the next.[6]
An arithmetic pattern with its mechanism exposed
On this page · Permalink · Source line 203
A small generating-function calculation illustrates the movement from pattern to explanation. Define the signed Euler numbers by the formal power series identity over \(\mathbb Q\),
The initial coefficients are \(1,0,-1,0,5,0,-61,0,1385\). Multiplication by \(e^t\) gives transformed coefficients
Their initial values are \(1,1,0,-2,0,16,0,-272,0\). A finite computation suggests that every positive even index has disappeared. The reason is not hidden in the numerical list:
The series \(\tanh t\) is odd. Thus \(b_{2j}=0\) for every \(j\geq1\). Multiplication by \(e^{-t}\) recovers the original coefficients, so the disappearance is a reorganization of information, not the destruction of the sequence.
The calculation does not prove a prime-power divisibility theorem. It establishes a parity statement through an invertible change of realization. A valuation claim would require a further arithmetic argument. This is an instructive boundary: a useful identity can be both completely proved and insufficient for the next conjecture.
Residue selectors make the mechanism more general. Let \(F(t)=\sum_{n\geq0}a_nt^n\) be a formal series over \(\mathbb C\), let \(\zeta\) be a primitive \(m\)-th root of unity, and choose \(0\leq r<m\). Then
For the coefficient of \(t^n\), the multiplier is the average of \(\zeta^{j(n-r)}\). It is one when \(m\) divides \(n-r\), and zero otherwise by the finite geometric-sum identity. The filter selects a lane of coefficients exactly. Because the argument is coefficientwise, it needs no analytic convergence assumption.
This is also where changing the coefficient setting matters. The displayed average uses roots of unity and division by \(m\). Transporting it into an integral or \(p\)-adic argument requires control of those operations, especially when \(p\) divides \(m\). A valid identity over \(\mathbb C\) does not by itself supply the integral estimate one hopes to extract from it.
Let the experiment challenge the explanation
On this page · Permalink · Source line 232
A productive experiment records the exact input, the proposed rule, and the observation that could separate it from an alternative. In arithmetic, this may mean moving beyond the first nonzero valuation, changing a residue class, or testing the boundary index where a conjectured formula begins. In an operator problem, it may mean composing once more or changing the protected subspace. The design follows the suspected failure mechanism.
Positive and negative cases both belong in the record. An example outside the hypotheses can explain why a hypothesis is needed. A degenerate example can reveal that a program is silently dividing by zero. An independent calculation can detect an indexing error that a symbolic derivation inherited from its own input. These are different kinds of evidence, and their usefulness depends on preserving the difference.
The resulting loop is not simply calculation followed by proof. A calculation suggests a structure. A counterexample refines it. A proof identifies why the structure works. New tests then challenge the implementation and the translation of the proof back into the original problem. Each stage asks the others a more precise question. Formal verification becomes valuable at exactly this interface.