vibe-qc/Documentation

Mathematical specifications and Lean proofs

vibe-qc’s formalization connects published working equations to precise mathematical definitions, machine-checked theorems and numerical checks of the implementation. The first example covers the real, closed-shell RHF finite-basis core. The remaining methods have an inventory of definitions and proof obligations to develop.

Resource	Purpose
Method inventory	Coverage of the method map, feature matrix and selected dispatch registries
RHF derivation and proof scope	Equations, assumptions, theorem names and implementation correspondence
Developer instructions	Reproduce the proof and implementation checks
Machine-readable inventory	Method families, variants, source entry points and open obligations

What each kind of evidence establishes

A mathematical proof establishes a stated consequence of explicit definitions and hypotheses, in exact arithmetic. The RHF project uses Lean 4 and mathlib, pinned by lean-toolchain and lake-manifest.json. Its proof audit checks the transitive axioms of every exported theorem.

An implementation check exercises the imported native library and compares its answers with an independently written expression of the specification. It uses finite tolerances, records the native module digest and includes deliberate errors to check that the comparison is discriminating. Passing these checks does not constitute a formal refinement proof of C++, its compiler, BLAS or the floating-point executable.

Scientific validation compares a calculation with a matched independent reference. It addresses a different question from exact algebra. Neither a formal proof nor an isolated energy match establishes the general physical accuracy of an approximate method, the convergence of every SCF iteration, or that a stationary solution is the global minimum.

Coverage therefore attaches to a named claim and route. A proof of the closed-shell density identity does not cover UHF, fractional occupations, periodic complex orbitals, gradients or density fitting. The normal method-status labels continue to describe scientific maturity.

Reproducing the checks

From the repository root, with Lean’s lake command available:

python formal/check_inventory.py
cd formal/rhf
lake exe cache get
python ../check_proofs.py

The proof audit builds the project and checks each theorem’s axiom list. Unfinished proofs and additional axioms are rejected. The allowed logical foundations are Lean’s propositional extensionality, classical choice and quotient soundness. The kernel and these foundations remain part of the trusted base. There is no scientific axiom asserting the desired RHF result.

From the repository root, using Python from a qualified vibe-qc installation:

python formal/check_rhf.py --output rhf-synthetic.json

This default command runs small synthetic tensor checks. The complete water/STO-3G example adds --molecule; run that mode through the calculation scheduler when collecting scientific acceptance. The matching independent reference input is reference_h2o.inp. Reports include environment paths, so inspect them before sharing them.

Related work and publication scope

Bobbin and colleagues formalized adsorption theories, thermodynamics and equations of motion in Lean in Formalizing chemical physics using the Lean theorem prover, Digital Discovery 3, 264-280 (2024), first published online in November 2023, doi:10.1039/D3DD00077J. Their LeanChemicalTheories project is relevant prior art for mathematical formalization in chemical physics. Physlib and SciLean provide related work in physics and scientific computing.

The contribution here is the explicit connection between selected RHF working equations, checked Lean theorems, an existing quantum-chemistry implementation and reproducible numerical checks. The present scope supports that description. It does not establish a priority claim such as “the first formally verified quantum-chemistry code”, or a proof of the entire program.

Extending the formalization

Each extension should supply the source equation and its conventions, a precise definition, a theorem with explicit hypotheses, the implementation entry points and a discriminating numerical check. Retain unresolved approximations and implementation gaps beside the corresponding claim. The inventory supplies the starting obligations. Shared matrix, tensor and metric results can then support UHF, density fitting, MP2 and later periodic and correlated methods.

Extensions in progress

UHF, density fitting and canonical MP2 add 13 checked algebraic claims. Selected implementation checks and the UHF/MP2 independent references pass; see each page for runtime identities and remaining proof obligations. The combined audit currently covers 28 theorems.