Hefestus: Language Models Propose Finite-Difference Schemes and Lean Certifies Their Stability

Turning a physical problem into a simulation one can trust requires four decisions: the model, the numerical scheme, whether that scheme is consistent and stable, and the parameters at which it runs. Any of them can fail silently, and a language model can make a wrong one sound plausible. Hefestus makes these decisions as a chain in which every claim carries its evidence, whether a theorem accepted by the Lean kernel, an exact computation or a measurement. The model comes from a closed catalog, a language model proposes the scheme, and Lean 4 certifies its consistency and von Neumann stability at the exact parameters of the run. Asked to prove stability claims about textbook and random schemes, three Claude 5.5 models always chose the true side. With the loop closed inside Hefestus, the kernel certified model-proposed schemes for 219 of 224 generated problems, and where the fixed table of schemes needs many substeps the certified stencils were cheaper: for heat with a large diffusion number they needed 7 point updates per data step instead of 27. When the data come from outside the catalog, a fit with a rejection test usually says so, and a physics-informed network trained on an equation discovered from the data can take over. On held-out problems whose true terms lie in its library, it returned a model in most cases and never a bad one, although it is not yet reliable for ODEs. A public instance returns the model, the scheme, the evidence for each claim, the simulation and a manuscript.