Why this page exists
Software written with AI. Here is how far you can trust the result.
Much of Sheaf's code is written with AI assistance and reviewed, tested and deployed by people. A reader is right to ask what that means for the check itself.
The check has two layers. The outer layer is ordinary software: it collects what the agents said, builds the structure below, and returns the result. It is tested the way any software is. The inner layer is the mathematics that decides whether the information holds together. That layer is written in Lean, a program that accepts a proof only when every step is correct, and it is published here so anyone can run the same check.
The next step, under way, is a certificate with every decision: the engine writes down why it stopped or released an action, and a small program whose correctness is itself proved confirms the certificate. That closes the gap between the two layers for every decision the gate makes.
The statements
Three files. Each backs one part of the check.
Each file names the part of the production code it stands behind. Every main theorem depends only on Lean's three standard axioms, and no proof step is skipped or assumed.
-
Ranking · backs the cycle check on comparisons
A set of items with "A ranks above B" comparisons can be given one consistent ranking exactly when the comparisons contain no loop.
When several agents compare the same items, Sheaf turns their comparisons into arrows and asks whether one global order fits all of them. This theorem says that order exists if and only if the arrows never lead back to where they started. Both directions are proved.
theorem exists_ranking_iff_acyclic : (∃ f : V → ℕ, IsRanking R f) ↔ Acyclic R -
Cycle certificate · backs the loop Sheaf reports
Around any loop of comparisons, every consistent set of positions sums to zero. So a loop whose stated margins do not sum to zero proves the data cannot come from any single set of positions.
When Sheaf stops an action because the agents' comparisons form a loop, it reports the loop. This theorem is what makes that loop evidence: it is a witness anyone can check by adding up the margins, and the check needs no trust in the engine that found it. In the language of the paper, the obstruction is a nonzero class in the first cohomology.
Writing the proof sharpened a sentence in the code. The header had said the obstruction is zero exactly when there is no loop. The precise pair is: a loop gives a witness, and no loop gives a consistent ranking. The header now says that.
theorem not_coboundary_of_cycle_sum_ne_zero (y : E → K) (h : Chain src tgt a a es) (hy : (es.map y).sum ≠ 0) : ¬ ∃ f : V → K, coboundary src tgt f = y -
Laplacian · backs the coherence score
The coherence score is the energy of the sheaf Laplacian. It is never below zero, never above the stated maximum, and it is zero exactly when the agents' positions agree along every comparison.
For positions on a scale, Sheaf adds up the squared disagreement across every pair, weighted by confidence. These theorems say that sum is the quadratic form of the Laplacian the paper describes, that dividing by the maximum gives a number between 0 and 1, and that the positions the Laplacian sends to zero are exactly the ones that agree, which is the agreement space the paper calls H⁰. A further theorem shows that the part of any disagreement that no single set of positions can explain is unique.
theorem dotProduct_lap (x : V → K) : ∑ v, x v * lap src tgt w x v = energy src tgt w x theorem energy_le_max (hw : ∀ e, 0 ≤ w e) (hx : ∀ v, |x v| ≤ a) : energy src tgt w x ≤ ∑ e, w e * (2 * a) ^ 2 theorem lap_eq_zero_iff (hw : ∀ e, 0 < w e) (x : V → K) : lap src tgt w x = 0 ↔ cob src tgt x = 0
Outside the proofs
What the files do not cover.
A precise small claim is worth more than a large vague one. These are the parts of the check the proofs say nothing about.
- Reading the agents' words. Which claims overlap, and what each agent's position is, are extracted by AI models. How well that works is measured in use. No theorem covers it.
- The spectral gap. The engine also reports the second eigenvalue of the Laplacian as a robustness reading. It is computed in floating point and is never the score. Nothing about eigenvalues is proved here.
- The count of agreement components. The files prove which positions the Laplacian sends to zero. The count the engine reports as the number of independent agreements is a later pass.
- The rule check. Sheaf's logical axis decides whether a set of rules can all hold at once. Lean ships a proved checker for the standard proof format those solvers produce, and wiring it in is the next step.
- The software around the mathematics. Network, storage, prompts, and the code that builds the structure from the agents' output are tested, and covered by the certificate work described above, but they are software, and software is not proved this way.
How the checking works
Run it yourself.
The files are Lean 4 modules on Mathlib, the community library of formal mathematics. Download the three files, or the whole project from the repository, and run the build. Lean either accepts every proof or reports the exact line that fails. The same bar applies as to the institute's own record: no skipped steps, no extra axioms, and the axiom list printed at the end of every file.