Solving hard problems

We help companies solve hard problems in mathematics, statistics, and computing. Let’s explore how we might work together.

Bayesian OCR

Posted on 10 September 2026 by John

The Greek letter β (beta) and the German letter ß (eszett) look similar, especially in some fonts.

Now suppose an OCR program sees some character that could be a beta or could be an eszett. It could calculate some kind of distance between between the pixel pattern of the character and the pixel patterns of beta and eszett. But that would be discarding context.

If you’re scanning a Greek document and run into a beta-like symbol, it’s very likely a beta. If you’re scanning a German document and run into a beta-like symbol, it could be a beta. For example, it could be a scientific paper that mentions beta particles or beta carotene. But most likely the symbol is an eszett.

The previous paragraph is saying you should compute the conditional probability of a set of pixels representing a character given the language of the document. You could be more sophisticated and look at the position of the symbol in a word as well. For example, if you see a symbol at the end of a Greek word that could either be ο (omicron) or σ (sigma), it’s likely an omicron because Greek has a different symbol ς for final sigma.

This post is a follow-on to my earlier post on the error rate in Google’s Ngram database. OCR errors are fairly common in that database, so why don’t they “just” fix the errors by using some sort of Bayesian method? OCR software probably does use some sort of Bayesian method, but it’s not that simple.

In that post I looked at the use of the word grok in English. The Ngram database shows the word being used before it was coined in 1961 due to OCR errors. Why didn’t Google compute the probability of a word being “grok” conditional on the publication date? That would be circular. We happen to know exactly when grok was coined, but in general we might try to determine when a word was coined by looking at a large set of scanned books, like the Ngram database!

Now we could compute the probable value of an ambiguously scanned word by conditioning on the language of the surrounding text. That would be a reasonable thing to do in general, but it could also lead to exactly the kind of errors we see in the Ngram data for grok.

Suppose you see an ambiguously scanned word in a book written in English. There is a higher prior probability that the word is an English word than a German word. Now suppose you see “gro?” where ? could be β, ß, or k. Without any context, perhaps the probability of the symbol being a k is small. But grok is an English word and groß is a German word which may lead you to conclude “?” is a k and the ambiguous word is grok.

Assigning higher prior probability to English words in English texts is the best thing to do on average, but in particular instances it will lead to errors. That’s life.

The Ngram database includes millions of scanned books. Google had to use OCR algorithms that work well on average. A linguist with a special interest in a particular word can be more careful and create a more sophisticated probability model (explicit or implicit) customized for their interests. Google did what they could operating at such a large scale.

A 50-year-old computer-assisted proof

Posted on 9 September 2026 by John

The idea of using computers to assist with proofs is not new. The first major computer-assisted proof was published in 1976, the proof of the four color theorem by Kenneth Appel and Wolfgang Haken. The authors reduced the proof of the four color theorem to verifying calculations on 1,834 configurations, each checked by a computer program.

The proof was simplified over the years, and formalized in Coq in 2005. Everyone is satisfied that the theorem is true, but there has never been a satisfying proof, one that a human could read and say “I see now why any map can be colored using only four colors.” And there may never be one, but see this post for a contrary prediction.

The IBM mainframe that ran the calculations completing the proof of the four color theorem did not generate the proof. It simply executed the FORTRAN program that Haken and Appel (and Koch [1]) gave it.

I don’t see the recent proof of finite-time blowup for solutions to the Navier-Stokes equations as entirely different. Computers did higher-level tasks for the OpenAI team than the mainframe did for Haken and Appel, and these tasks were not as directly programmed as the tasks that were given to the mainframe, but still machines do what they are told to do.

[1] John A. Koch was a programmer who worked on the four color proof with Haken and Appel. I don’t know how much credit he deserves, but I suspect it may be more than he was given.

AI is an intelligence multiplier

Posted on 9 September 2026 by John

A rising tide may lift all boats, but the AI tide lifts some boats much more than others.

By all accounts, the best programmers have had the biggest productivity boost from AI. And top tier mathematicians are using AI to settle long-standing mathematical conjectures. AI is a powerful tool, but tools don’t come to life and make things on their own.

I routinely have naive amateurs [1] send me proofs of open conjectures, and naturally more recent such proofs involve AI. I’ll get an email saying something like “I’ve solved the Collatz conjecture using ChatGPT, but I’m not a mathematician so I need some help verifying the proof.” And of course the supposed proof is rubbish.

The recent Navier-Stokes proof is impressive, but AI didn’t initiate the proof any more than LaTeX did. Nor did a child steer AI into proving the conjecture. Professional mathematicians were able to use AI to pursue their ideas at superhuman speed. But someone without an understanding of the Navier-Stokes problem, and familiarity with recent ideas for approaching the problem, could not have directed AI to produce a proof.

Computer scientists have been saying “garbage in, garbage out” from the beginning. A variation on this aphorism for the age of AI would be “mediocrity in, mediocrity out.”

***

[1] Amateurs can and do make contributions to mathematics. For example, in 2022 David Smith, a retired print technician, discovered a single shape that can be used to create an aperiodic tiling of the plane. By “naive amateurs” I mean people who literally do not know what they are talking about.

The part of Navier-Stokes no one is talking about

Posted on 9 September 2026 by John

Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.

Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.

Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote

To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.

That was the rule of thumb: forty hours per page. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.

Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.

I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.

Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.

Navier-Stokes in the news

Posted on 8 September 2026 by John

There are rumors that a long-standing math problem, one of the Millennium Prize problems, has been solved.

The problem concerns technical properties of solutions to the Navier-Stokes equations [1], a set of equations that describe the dynamics of fluid flow. Popular accounts of the problem are often oversimplified and misleading.

Some reports will speak of the problem as “solving the Navier-Stokes equations.” The task is not to write down a closed-form solution, which can’t be done, or solve the equations numerically, which has been done for decades. The problem is to prove theoretical properties of solutions which are of little interest in practice.

There has been progress toward settling the Navier-Stokes problem. Terence Tao wrote a post on this yesterday.

What’s also interesting is the intrigue around the possible solution. A post this morning says

If I am reading this correctly, Tristan Buckmaster is alleging OAI has a resolution of Navier-Stokes … which maybe used info from Buckmaster and Levent Alpöge’s private Codex sessions.

Buckmaster asked OpenAI whether they used his private sessions and they have not responded. Update: Statement from OpenAI.

Personal note

This topic connects parts of my career spanning decades. My graduate work was in PDEs and I had some interest in the Navier-Stokes equations. Here are some notes I wrote back in the day.

Now I work more with privacy than with PDEs. The question of whether OpenAI uses private data, contradicting their stated policy, is more relevant to my current work than whether the Navier-Stokes equations have global regular solutions.

[1] I never know whether to say equation or equations. You’ll hear both. You could think of Navier-Stokes as one vector-valued PDE or three scalar-valued equations.

Ngram error rate

Posted on 7 September 2026 by John

The Online Etymological Dictionary gives the following etymology for grok:

grok (v.)

“understand empathically,” 1961, an arbitrary formation by U.S. science fiction writer Robert A. Heinlein (1907-1988) in his book “Stranger in a Strange Land.” In the book it is a transliteration of a Martian word and is said to mean etymologically “to drink.” It attained popular use in 1960s-70s counterculture but is perhaps obsolete now except in internet technology circles.

I don’t believe anything in the statement above is disputed. And yet Google’s Ngram Viewer tells a very different story.

The plot implies that use of the word grok had been increasing before Heinlein’s book came out and is now much more common than it was in the 1970s. Note that the plot ends before the Grok AI came out in late 2023.

Apparently the Ngram data is unreliable, mainly for two reasons: OCR errors and inaccurate date attribution. Presumably the blip around 1900 was due to the former, OCR causing words like crok or grog to be cataloged as grok. And presumably the rise in usage before 1961 was due to the latter, misattributing the date of sources published after 1961.

The supposed rise in usage before 1961 is interesting. You’d expect some lag between the time a word circulates in conversation and when it appears in books, but apparently this lag can be smaller than the effect of date misattribution.

Etymonline speculates that grok is “perhaps obsolete now except in internet technology circles.” That matches my experience. Even in technological circles, the word was uncommon before Grok was released. Maybe it was more common in print than in conversation.

Previous posts with Ngram stats. The effects are so large that they’re probably directionally correct after adjusting for a substantial error rate.

Proof of the rank-trace theorem

Posted on 5 September 2026 by John

The previous post discussed the motivation for and application of the rank-trace theorem. This post will give a proof.

Suppose A is a real symmetric matrix. The rank-trace inequality says

$\operatorname{rank}(A)\ge\frac{(\operatorname{tr} A)^2}{\operatorname{tr}(A^2)}$

where tr is the trace operator, the sum of the elements along the diagonal of the matrix.

Terse proof

Here’s the proof in a nutshell: diagonalize A and use the Cauchy-Schwarz inequality.

Detailed proof

Now let’s unpack that. Any real symmetric matrix A is similar to a matrix D with the eigenvalues of A along the diagonal.

$A = PDP^{-1}$

The trace of a matrix stays the same under a similarity transformation, i.e. multiplying by P on one side and its inverse on the other side. So without loss of generality we may as well assume A is diagonal.

The rank of a matrix equals the number of non-zero eigenvalues, so a vector containing the non-zero eigenvalues of A

$v = [\lambda_1, \lambda_2, \ldots, \lambda_r]$

has length r where r is the rank of A. Define w to be the vector of dimension r consisting of all 1’s.

$w = [1, 1, \ldots, 1]$

Then by the Cauchy-Schwarz inequality we have

$\operatorname{tr}(A)^2 = \langle v, w \rangle^2 \leq \langle v, v \rangle \, \langle w, w \rangle = r \operatorname{tr}(A^2)$

Cyclic trace property

Why should a matrix A and its diagonalization D have the same trace?

The trace of a matrix product AB equals the trace of the product BA. To prove this, write out matrix products and the traces, then note that the two expressions are equal.

$\begin{align*} \operatorname{tr}(AB) &= \sum_i(AB)_{ii}=\sum_i\sum_k A_{ik}B_{ki} \\ \operatorname{tr}(BA) &= \sum_j(BA)_{jj}=\sum_j\sum_k B_{jk}A_{kj} \end{align*}$

Therefore

$\operatorname{tr}(A) = \operatorname{tr}((PD)P^{-1}) = \operatorname{tr}(P^{-1}(PD)) = \operatorname{tr}(D)$

More generally, trace has the cyclic property

$\operatorname{tr}(ABC) = \operatorname{tr}(CAB) = \operatorname{tr}(BCA)$

However, not all permutations preserve the trace. For example, let

$A=\begin{pmatrix}0&1\\0&0\end{pmatrix},\quad B=\begin{pmatrix}0&0\\1&0\end{pmatrix},\quad C=\begin{pmatrix}1&0\\0&0\end{pmatrix}.$

Then

$\operatorname{tr}(ABC) = \operatorname{tr}\begin{pmatrix}1&0\\0&0\end{pmatrix} = 1$

but

$\operatorname{tr}(ACB) = \operatorname{tr}\begin{pmatrix}0&0\\0&0\end{pmatrix} = 0$

Computing a lower bound on matrix rank

Posted on 4 September 2026 by John

Suppose you want to know the rank of an n × n matrix A, the number of linearly independent rows of A, or equivalently the number of linearly independent columns. There are at least three difficulties.

Difficulties in computing rank

First of all, rank is not a continuous function of a matrix. Since rank is an integer, an arbitrarily small change in the matrix could cause a discrete change in the rank [1]. A small error in computing A could produce a matrix with a different rank.

Second, finding the rank takes O(n³) operations, which may or may not be an issue depending on context.

Third, you may not have the matrix A in an explicit form. Maybe you’re able to compute products Av for vectors v but it’s not practical to form the entire matrix A.

Rank-trace inequality

If you don’t need to know the rank of A per se, but only need to know whether it is above a certain size, a lower bound on the rank may enough.

Suppose A is a Hermitian matrix. If A is real, this means A is symmetric. If A is complex, this means A equals its conjugate transpose. Then the rank-trace inequality says

$\operatorname{rank}(A)\ge\frac{(\operatorname{tr} A)^2}{\operatorname{tr}(A^2)}$
The quantity on the right hand side is known as the stable rank of A. It’s not a rank in any algebraic sense, but it gives a lower bound on rank. And it solves the three problems listed above. See the next post for a proof of the rank-trace theorem.

Stability

First of all, trace is a continuous function of a matrix, and so stable rank is also a continuous function of a matrix, provided the denominator isn’t zero. A small change to a matrix only makes a small change to its stable rank. That’s why stable rank is called stable.

Efficiency

Second, although computing rank takes O(n³) operations, computing stable rank takes only O(n²) operations, though this isn’t immediately obvious.

The trace of A takes n operations: simply sum the elements on the diagonal of A. But how do you take the trace of A²? Squaring A takes n³ operations, and so if you had to square A to find the trace of A² the rank-trace inequality would have no efficiency advantage over finding the rank of A. But you can compute the trace of A² via

$\operatorname{tr}(A^2) = \sum_{i=1}^n \sum_{j=1}^n |a_{ij}|^2$

Formation

Now suppose you don’t have the matrix A per se but you do have a way of probing A, computing the product of vectors with A. Maybe A is too large to fit into memory, or explicitly computing the elements of A would take too long.

There are Monte Carlo algorithms for estimating the traces of A and A² that could be used together to estimate the stable rank of A.

Demonstration

The following Python code illustrates the discussion above.

import numpy as np

np.random.seed(20260904)
n = 5
B = np.random.randn(n, n)
A = B.T @ B + 1e-8 * np.eye(n)  # Gram matrix plus a tiny shift => SPD

rank_A = np.linalg.matrix_rank(A)
tr_A = np.trace(A)
tr_A2 = np.trace(A @ A) # matrix product 
sum_sq = np.sum(A * A) # element-by-element product
stable_rank = (tr_A ** 2) / tr_A2

print(f"A =\n{A}\n")
print(f"rank(A)              = {rank_A}")
print(f"tr(A)                = {tr_A:.12f}")
print(f"tr(A^2) direct       = {tr_A2:.12f}")
print(f"tr(A^2) indirect     = {sum_sq:.12f}")
print(f"stable rank          = {stable_rank:.12f}")

The code above produces the output below.

A =
[[ 1.09945682  0.4899665   0.98901845  0.66983113 -1.35006341]
 [ 0.4899665   0.98531254  0.35067791  0.89757603 -0.72037507]
 [ 0.98901845  0.35067791  4.31233926  0.94556225 -0.54819048]
 [ 0.66983113  0.89757603  0.94556225  1.3494295  -1.33840786]
 [-1.35006341 -0.72037507 -0.54819048 -1.33840786  3.54858332]]

rank(A)              = 5
tr(A)                = 11.295121449420
tr(A^2) direct       = 51.035447533673
tr(A^2) indirect     = 51.035447533673
stable rank          = 2.499826585688

[1] Topological argument: A map from a connected space (such as ℝ^n×n) onto a discrete space (such as ℤ) cannot be continuous, otherwise the inverse images of the points in the range would partition the connected space into disjoint open sets, violating the definition of a connected space.

Hugging Face Easter Egg

Posted on 3 September 2026 by John

NVIDIA has offered to buy Hugging Face for $12,930,300,000.

129303 is the Unicode code point for the Hugging Face emoj (U+1F917), which you can verify with the following Python code.

>>> import unicodedata
>>> 129303 == 0x1F917
True
>>> unicodedata.name(chr(0x1F917))
'HUGGING FACE'

Hugging Face emoji

New RSA number factored

Posted on 3 September 2026 by John

Eric Lu announced on X today that he has factored RSA-260, a number N with 260 digits (862 bits) that is the product of two large primes [1].

RSA numbers are challenge problems posed to gauge the security of RSA encryption, which rests on the difficulty of factoring large numbers [2]. The naming scheme is confusing because RSA-n might have n digits or n bits. For example, RSA-768 is smaller than RSA-260 because the former has 768 bits and the latter has 260 digits.

RSA-260 is the largest RSA number factored so far. What does the news of its factorization say about the security of RSA?

Based on equations here, an RSA key with 862 bits would have a security level of 74 bits, i.e. the same security level as symmetric encryption with a 74-bit key. The minimum recommended RSA key size now is 2048 bits, which has a security level of 107 bits.

Security levels are on a logarithmic scale: each additional bit of security doubles the effort required to break the encryption by brute force. So breaking a 2048-bit RSA key would take 2³⁴, roughly 10¹⁰, times more effort than factoring RSA-260. All this depends on numerous assumptions, such as the state of factorization algorithms and the non-existence of CRQC [3].

Update: A week after the initial announcement, Eric Lu released an article explaining how he factored RSA-260. He says “In total, I estimate that this factorization cost about 4,900 GPU-days, or 13.5 GPU-years, which is about $400k at current market prices.”

[1] N = pq = 22112825529529666435281085255026230927612089502470015394413748319128822941402001986512729726569746599085900330031400051170742204560859276357953757185954298838958709229238491006703034124620545784566413664540684214361293017694020846391065875914794251435144458199

p = 4397328654844826923795068102505872571721883526553349659561256924505973939597593482272505698004801207988043088656411102133523080581

q = 5028695206842569864686141618253083416610081090075366674776775706538324961364412200138116378509733307971876652984898985905923678379

[2] The ability to efficiently factor large primes would break RSA. It’s possible that there’s a way to break RSA without being able to factor large numbers. More on that here.

[3] Cryptographically-relevant quantum computer. Quantum computers exist, but so far they’re cryptographically irrelevant. So far quantum computers cannot factor 21 without cheating.

Solving hard problems

Bayesian OCR

Related posts

A 50-year-old computer-assisted proof

Related posts

AI is an intelligence multiplier

The part of Navier-Stokes no one is talking about

Related posts

Navier-Stokes in the news

Personal note

Related posts

Ngram error rate

Related posts

Proof of the rank-trace theorem

Terse proof

Detailed proof

Cyclic trace property

Computing a lower bound on matrix rank

Difficulties in computing rank

Rank-trace inequality

Stability

Efficiency

Formation

Demonstration

Hugging Face Easter Egg

Related posts

New RSA number factored

Related posts