How much certainty is worthwhile?

digitado ⋅ 8 de March de 2026

A couple weeks ago I wrote a post on a composition table, analogous to a multiplication table, for trig functions and inverse trig functions.

$renewcommand{arraystretch}{2.2} begin{array}{c|c|c|c} & sin^{-1} & cos^{-1} & tan^{-1} \ hline sin & x & sqrt{1-x^{2}} & dfrac{x}{sqrt{1+x^2}} \ hline cos & sqrt{1-x^{2}} & x & dfrac{1}{sqrt{1 + x^2}} \ hline tan & dfrac{x}{sqrt{1-x^{2}}} & dfrac{sqrt{1-x^{2}}}{x} & x \ end{array}$

Making mistakes and doing better

My initial version of the table above had some errors that have been corrected. When I wrote a followup post on the hyperbolic counterparts of these functions I was more careful. I wrote a little Python code to verify the identities at a few points.

$renewcommand{arraystretch}{2.2} begin{array}{c|c|c|c} & sinh^{-1} & cosh^{-1} & tanh^{-1} \ hline sinh & x & sqrt{x^{2}-1} & dfrac{x}{sqrt{1-x^2}} \ hline cosh & sqrt{x^{2} + 1} & x & dfrac{1}{sqrt{1 - x^2}} \ hline tanh & dfrac{x}{sqrt{x^{2}+1}} & dfrac{sqrt{x^{2}-1}}{x} & x \ end{array}$

Checking a few points

Of course checking an identity at a few points is not a proof. On the other hand, if you know the general form of the answer is right, then checking a few points is remarkably powerful. All the expressions above are simple combinations of a handful of functions: squaring, taking square roots, adding or subtracting 1, and taking ratios. What are the chances that a couple such combinations agree at a few points but are not identical? Very small, maybe even zero if you formalize the problem correctly.

In the case of polynomials, checking a few points may be sufficient. If two polynomials in one variable agree at enough points, they agree everywhere. This can be applied when it’s not immediately obvious that identity involves polynomials, such as proving theorems about binomial coefficients.

The Schwartz-Zippel lemma is a more sophisticated version of this idea that is used in zero knowledge proofs (ZKP). Statements to be proved are formulated as multivariate polynomials over finite fields. The Schwartz-Zippel lemma quantifies the probability that the polynomials could be equal at a few random points but not be equal everywhere. You can prove that a statement is correct with high probability by onlt checking a small number of points.

Achilles heel

The first post mentioned above included geometric proofs of the identities, but also had typos in the table. This is an important point: formally verified systems can and do contain bugs because there is inevitably some gap between what it formally verified and what is not. I could have formally verified the identities represented in the table, say using Lean, but introduced errors when I manually transcribe the results into LaTeX to make the diagram.

It’s naive to say “Well then don’t leave anything out. Formally verify everything.” It’s not possible to verify “everything.” And things that could in principle be verified may require too much effort to do so.

There are always parts of a system that are not formally verified, and these parts are where you need to look first for errors. If I had formally verified my identities in Lean, it would be more likely that I made a transcription error in typing LaTeX than that the Lean software had a bug that allowed a false statement to slip through.

Economics

The appropriate degree of testing or formal verification depends on the context. In the case of the two blog posts above, I didn’t do enough testing for the first but did do enough for the second: checking identities at a few random points was the right level of effort. Software that controls a pacemaker or a nuclear power plant requires a higher degree of confidence than a blog post.

Rigorously proving identities

Suppose you want to rigorously prove the identities in the tables above. You first have to specify your domains. Are the values of x real numbers or complex numbers? Extending to the complex numbers doesn’t make things harder; it might make them easier by making some problems more explicit.

The circular and hyperbolic functions are easy to define for all complex numbers, but the inverse functions, including the square root function, require more care. It’s more work than you might expect, but you can find an outline of a full development here. Once you have all the functions carefully defined, the identities can be verified by hand or by a CAS such as Mathematica. Or even better, by both.

The post How much certainty is worthwhile? first appeared on John D. Cook.

Like 0

Liked Liked