FARMS tests whether formal mathematics can become reusable knowledge for scientific AI

FARMS evaluates whether formal mathematics can be reused as computational knowledge.

An October 29 preprint proposes a pipeline called FARMS for turning source material in computational mathematics into structured knowledge that AI systems can reuse. The researchers link formal statements to the assumptions, algorithmic meaning and quantitative guarantees behind them. They test the approach on material from randomized numerical linear algebra and numerical partial differential equations. [FARMS preprint](https://arxiv.org/abs/2610.40560)

A checked statement needs its assumptions

A numerical method can offer a guarantee under assumptions about the inputs, tolerance or operating conditions. A model that retrieves only the conclusion can recommend a method in a setting where the guarantee no longer applies. FARMS ties formal statements to their source and puts them through semantic review. The paper describes Lean-checked implications connecting selected statements to computational tasks, illustrated through a heat-flow solve and a wave-response compression example.

Lean checks the implications encoded with the stated premises. A separate step still has to establish that a formal statement matches the intended claim and that a downstream task satisfies those premises. In this setting, preserving provenance and explaining why a statement applies are part of making the knowledge useful. [FARMS preprint](https://arxiv.org/abs/2610.40560)

What the evaluation counts

The authors say 157 of 171 targets passed their pipeline, with mean estimated costs ranging from $0.85 to $2.29 per target across sources. Those figures describe the authors’ selected inputs, acceptance criteria and costing. They do not establish how much it would cost to formalize a whole discipline or verify every claim a science agent might use.

The more practical next question is whether a second team can reuse the structured result in a new computation and identify when it no longer applies. For a scientist, a traceable proof component can be valuable even when the final computation still needs ordinary checks against numerical error, input quality and physical assumptions. [FARMS preprint](https://arxiv.org/abs/2610.40560)