When Lean is too heavy — size, wording and stock

A proof that is written on paper sometimes does not go into Lean. The reasons split into three, and which one you are facing decides what to do.

The problem of size can be measured. The problem of form is a problem of design. The problem of stock is a decision between building it yourself and leaving it on paper. None of the three is "it cannot be done"; all three are "it cannot be done at the cost that can be paid now", and the order of magnitude of the cost differs.

A demonstration — the cost of decide is set by the search space

decide enumerates every finite case. The cost is the number of cases itself. Measure it on a small example. Take the graph on the vertices Fin k in which the first 4 points are pairwise adjacent (if 4 points are pairwise adjacent, 3 colours will not do), and have it confirmed that there is no 3-colouring at all by decide. There are 3^k colourings.

def Adj (k : ℕ) (i j : Fin k) : Bool := i.val < 4 && j.val < 4 && i.val ≠ j.val

def Proper (k : ℕ) (f : Fin k → Fin 3) : Bool :=
  decide (∀ i j : Fin k, Adj k i j = true → f i ≠ f j)

set_option maxRecDepth 100000 in
theorem noCol6 : ∀ f : Fin 6 → Fin 3, Proper 6 f = false := by decide

The checking time was measured for different k. A file with nothing but import Mathlib takes 5.01 seconds, so the difference from that is the cost of decide.

Three things can be read off.

• The cost is roughly proportional to the number of cases. 0.4 seconds for 81 cases, 4.2 seconds for 729 — 9 times the cases, about 10 times the time
• The range that passes with the default settings is narrow. At 729 cases the recursion-depth limit is already exceeded. Raising it with set_option maxRecDepth lets it through
• Raise it, and the next limit comes. At 6,561 cases it hits the heartbeat limit (a deterministic bound on the amount of computation). Remove that, and it will not stop

When you hit a wall of this shape, the thing to do is not to raise the limit and wait, but to measure the cost per case and work out the order of magnitude of the whole.

A real instance — 1.48 million decisions come to 100–1000 CPU-hours

In the upper-bound argument for unit-distance graphs, the candidate graphs are dropped by passing them through a sieve in stages. The first stage of the sieve is a decision that looks only at the edge set and drops a candidate for "too many vertices" or "degree too large"; 86% of the candidates fall here. What happens if this decision is run inside Lean was measured.

The next stage is heavier still, and the whole comes to the order of 10²–10³ CPU-hours. The number of certificates (771) is a scale already within reach; what governs the order of magnitude is the number of times the decision is run.

One point of design comes out of this estimate. The reason a decide is fired per candidate is that the number of candidates is fixed outside Lean. Bring the list of candidates into Lean as a term, and decide is run once. But holding the list as a term makes the term of order 10⁶ in size, and the cost may merely move from "the number of runs" to "the size of the term". Which is cheaper is a question that can be measured.

Existence is cheap, non-existence is expensive

There is one asymmetry of cost, and among problems of size it is the one that matters most.

In the same setting as the demonstration above, measure the side that can be coloured. If only the first 3 points are pairwise adjacent, the graph can be 3-coloured. Write down one colouring and hand it over.

theorem col20 : ∃ f : Fin 20 → Fin 3, Proper3 20 f = true :=
  ⟨fun i => ⟨i.val % 3, Nat.mod_lt _ (by norm_num)⟩, by decide⟩

Even with 20 points, 5.21 seconds — 0.2 seconds above the baseline. The search space is 3^20 = 34 hundred million colourings, but hand over a witness and no enumeration happens. It is cheaper than non-existence on 6 points (729 cases).

So when designing a stage of the sieve, look first at which direction that stage is used in. A sieve is a tool for dropping candidates, so every stage is used in the direction of non-existence. "Drop it because it cannot be 3-coloured", written as it stands, is an exhaustive search.

In the real instance, among the stages of the sieve above, the one mark that rests on colouring is the one that cannot be run in Lean. With 15 points and 3 colours it is an exhaustive search over 3^15 = 1,434 ten-thousands of colourings, and it fails on the recursion-depth limit (measured). The statement itself is elementary, and on the lattice it closes in ten lines. The heaviness comes not from the difficulty of the statement but from the direction it is used in.

Take this stage out of the sieve and the whole still closes, but 4.8 times as many candidates flow downstream. Keep, as a variable in the estimate, how many times the downstream count multiplies when one stage is dropped.

An argument that lines up candidates and knocks them down one by one has two parts.

What makes (ii) hard is not a problem of size. The form for setting up the statement is not settled. To write it, at the least the following are needed.

• Holding the whole of "the candidates" as a Lean type. Make the whole of "the graphs on 11 vertices with independence number at most 3" a type, in the form quotiented by isomorphism
• Putting the definition of isomorphism inside Lean. The outside search counts isomorphic graphs as one. That "way of merging" has to be stated inside Lean
• The correctness of the search itself. That the search, pruning included, has left no candidate in the branches it discarded

The third is the substance. The outside search prunes branches for speed, and the reason for pruning exists only inside the code of the search. Moving that into Lean is the same work as rewriting the search in Lean. The division of labour in 07 Having Lean check certificates (search outside, confirm in Lean) does not work here. There is nothing that plays the part of a certificate.

What is in Lean is only the length of the list.

theorem cands_card : cands.length = 117 := by decide

This is "the list has 117 entries", not "the candidates are exactly 117". The difference between the two is Type 2 of 08 Does it say what you meant?.

So the grades are written separately. (i) is Lean, (ii) is computation. The upper-bound claim rests on both (i) and (ii), so the grade of the claim as a whole is computation. Only (i) carries a theorem name, so unless a table is made, this one step gets dropped.

The third source is that the underlying mathematics has not been formalised yet. In this case the cost is the cost of "building it yourself".

Whether the stock exists can be found with grep. These are the results of searching the mathlib source.

This table decides what is left on paper. Where the stock is partly there, as in the fourth and fifth rows, connecting to the part that exists is sometimes the cheaper course. The measure on the sphere was there, so a single theorem was put in showing that the measure defined by its properties agrees with mathlib's definition, and the connection was made (08 §04 (c)).

The criteria for deciding to leave it on paper

When the following three all hold, the decision is to leave it on paper.

Conversely, if any of the following applies, it is not left on paper. It is the new part of your own argument (not something brought in) / it connects if a part of the stock is used / it is a problem of size, not of form.

How to write down that it was left on paper

The part left on paper is placed as a row in the table of results. Three things are written.

The third is what does the work. Write where the seam is, and the reader can inspect just that spot. Write only "part of it is on paper", and there is no telling where to look.

And if the paper row comes right before the conclusion, the grade of the conclusion is paper. However many Lean rows are lined up, that does not change. The procedure for the receiving end to confirm this is ⑦ of 09 How to read a statement.

In all three, the conclusion is not "it does not go into Lean" but "this part is of a different grade". Write the grades separately and the result is usable. Write them without separating, and the Lean rows read as if they guaranteed the paper rows.

Next: 11 Common pitfalls — the messages you see when you hit the limits above, and how to read them. Terms are in the 12 Glossary.