The Sheaf Mathematical Institute.

How it works

A few researchers, one blackboard, bounded rounds.

This is the rule the institute runs by. A small group of AI researchers is given a question. They work at a shared blackboard, propose steps, and check each other's steps. Where they disagree, the disagreement is measured with the same coherence check our products use, and the work stops there until it is resolved. Each question gets a fixed number of rounds and a fixed budget.

The researchers are inexpensive models. The checking is what makes a result trustworthy, and the final check is done by a machine that cannot be talked into anything.

Where it stands today. All of this runs. The room sits on its own small server with the Lean library installed, wakes every night, works one question, and writes every step to the Sheaf evidence ledger. When a proof passes the checks it is parked, and the gate emails us. The first calibration entry was formalised by hand before the room opened. Everything after it comes out of the room, and the record says which is which.

1. A question is set.

   Questions come from our own mathematics first: the sheaf cohomology behind the coherence measure, and the paper it rests on. We can judge those. Over time the range widens.

2. The researchers work it.

   Each proposes a step. The others try to break it. A step that survives goes on the board. A step that does not is recorded as a dead end, which is also useful. After every round the disagreement between the researchers is measured; a round where they cannot agree stops the work.

3. The proof is written in Lean.

   A candidate proof is translated into the Lean 4 proof assistant, on top of the mathlib library. If it does not compile, it is not a result. The compiler is the cheapest and strictest member of the panel. What Lean is, and why it matters for AI →

4. A person releases it.

   Every candidate that compiles is held the same way our product holds a decision and waits for a person at Sheaf Labs to release it. Nothing goes on this page on its own.

What counts as a result

Three checks, all three required.

A proof assistant says a statement is true. It does not say whether the statement is new, or worth anything. So three things have to hold before a line appears below.

• ⊢
  The proof compiles.

  The statement and its proof are written in Lean 4 with mathlib, and the file builds without any unfinished step. The file is linked from the result.

• lit.
  The search says what is already out there.

  Two searches, run by more than one seat: is the mathematics known, and has it been machine-checked anywhere. Every reference found is kept on the entry. A known theorem with no machine-checked proof we could find still counts. A known theorem that has already been checked does not.

• ✋
  A person released it.

  The entry names who released it and when. The release is written to the Sheaf evidence ledger, signed and timestamped, along with every round, every Lean attempt and the literature check that led to it.

Results

The record.

Newest first. A result appears here only if it clears a bar beyond the three checks: either the search found no prior statement of the mathematics, or it found no machine-checked proof of it anywhere we looked (mathlib and other Lean projects, Isabelle's archive, Coq libraries). Each entry says which, and lists what the search found. Each entry names the field, the statement in plain English, and where the checked proof lives. Nothing is added here by the researchers themselves.

Nothing has cleared the bar yet. The room is working on the question on the board.

• Topology · sheaves on finite spacesChecked in LeanFormalisation of known mathematics

  The smallest open set around a point cannot be covered by anything smaller.

  Every point of a finite space sits inside one smallest open set. Any collection of open sets that covers it must contain it whole. This is the fact that lets a sheaf on a finite space be described by data on the points and the order between them, and turns its cohomology into a finite matrix computation. It is Lemma 5.1 of the paper below.

  Writing the proof for the checker showed that the covering statement needs no finiteness at all. It holds in every topological space. Finiteness is only what makes the smallest set around a point open. The Lean file records both facts.

  theorem exists_eq_nhdsKer_singleton_of_cover {X : Type*} [TopologicalSpace X] {ι : Type*} (x : X) (V : ι → Set X) (hV : ∀ i, IsOpen (V i)) (hcov : nhdsKer {x} = ⋃ i, V i) : ∃ i, V i = nhdsKer {x}
  The Lean file The paper it comes from Literature: standard for Alexandrov spaces. mathlib has the minimal set and its minimality; the covering statement was not in it. Released by Jack Widman, 22 September 2026.

Recent sessions in the room

Calibration runs

The runs that proved the machine works.

Known lemmas, chosen because we could judge them, sent through every check to see the pipeline hold. They are on the record with their Lean files, and they do not count as results.

• Topology · sheaves on finite spacesChecked in LeanCalibration

  The smallest open set around a point cannot be covered by anything smaller.

  Lemma 5.1 of the finite-spaces paper. Formalised by hand before the room opened. The proof showed the statement needs no finiteness.

  The Lean file

Why

Our product measures whether AI reasoning holds together. The institute runs on it.

Sheaf Labs is a mathematics lab with products. The products check whether a group of AI agents agree before one of them acts. The institute points the same check at mathematics, where the final answer can be verified by a machine, and keeps a public record of what came out.

Each line on this page is a claim anyone can check by opening the file. That is the standard we hold our products to, applied to ourselves.

The same checker covers the products themselves. The mathematics the coherence gate runs on is proved in Lean, in three files kept alongside this record. What is proved lists each statement in plain words.