Skip to main content

The formal loop

The formal loop closes the gap between "we computed a rigorous enclosure" and "a theorem prover agrees." It is the strongest guarantee omnibias offers — and it is deliberately narrow and honest.

The pieces​

  • omnibias.core.proof.lean_check — the bridge.
  • formal/omnibias-verified-kernel — a Mathlib-free Lean 4 kernel with sound ZInterval algebra and a finite rational obligation checker (sorry-free).

What gets checked​

The bridge extracts a certificate's finite, rational obligation — for example, a spectral-gap positivity, the sign of an enclosed quantity, or an error bound below a threshold — and emits Lean that chains the kernel's proven soundness lemmas. It then runs lake build.

from omnibias.core.proof.lean_check import verify_with_lean

verdict = verify_with_lean(certificate)
print(verdict.theorem_prover_verified)   # True only on a genuine kernel pass

The honesty guarantees​

The flag cannot be forged

theorem_prover_verified is set only on a genuine kernel pass. It can never be set by the certificate itself, and asserting the claim without a pass blocks the verdict. There is no path by which a fabricated certificate earns the flag.

  • Graceful degradation. If no Lean toolchain is present, the bridge degrades gracefully and the flag stays False — the rest of omnibias is unaffected.
  • Mathlib-free by design. The kernel uses Lean 4 core only, so CI can kernel-check it cheaply. The infinite analytic obligations (for example, the Clay-class statements scaffolded in formal/yang-mills-mass-gap) stay honestly sorry. We do not claim otherwise.

Why "finite and rational"?​

A Lean kernel can decisively check a finite inequality over rational numbers. It cannot, in a cheap CI pass, discharge an infinite analytic theorem. omnibias therefore reduces a certificate to the finite arithmetic core that a kernel can check, and is explicit that the surrounding analytic obligations remain open.

Reading a verdict​

A Verdict tells you exactly three things:

  1. The certified enclosure (the rigorous interval / Taylor model).
  2. Whether the finite obligation passed the Lean kernel (theorem_prover_verified).
  3. The schema version of the certificate.

That is the complete, falsifiable statement of what was verified — and an honest boundary around what was not.

See also​

Last updated on