Proof Artifacts for A Zero-Knowledge Formal Proof of FeMoco's Active-Space Ground-State Energy

Abstract

Abstract A Groth16 zero-knowledge formal proof is published certifying a ground-state energy for the standard FeMoco active-space Hamiltonian (113 electrons, 76 orbitals). For the public LLDUC FCIDUMP [1], the certified E_FCI is E_FCI = −22,140.967 Ha certified to sub-micro-Hartree precision (bracket width 1.907 × 10⁻⁶ Ha). Both bounds of the eigenvalue bracket are certified by exact rational arithmetic checked by the Lean 4 kernel against mathlib with no custom mathematical axioms: an LDLᵀ certificate for the lower bound and a Rayleigh-quotient certificate for the upper bound. The proof is verifiable in under one second by any party in possession of the proof artifact and verification key, with no access to the FCIDUMP or to any aspect of the method.