FARMS FOR COMPUTATIONAL SCIENCE
Turning mathematical literature into faithful, reusable knowledge for scientific computing.
University of Maryland, College Park
The University of Tennessee, Knoxville
SOURCE CONTEXT
Objects · assumptions · algorithms
FORMAL REPRESENTATION
FARMS∀ t : ℝ, 0 ≤ t →
totalEnergy Ω u t =
totalEnergy Ω u 0 := by sorryCOMPUTATIONAL USE
Source premises + checked connecting implications
* Includes 3 source-warning outcomes. Acceptance is about statement construction, not completed proofs. See reported results →
01 / THE IDEA
A formula alone does not tell you when an algorithm can be trusted.
Its guarantee depends on the objects, assumptions, sampling rules and error measure around it. FARMS brings this context into a formal representation, so the conditions for computational reuse are available for inspection.
02 / THE METHOD
Preparation recovers context. Formalization makes it explicit. Compilation and semantic review examine different parts of the result.
Recover the context behind a claim.
Construct, check, review and repair.
Explicit assumptions.
Source-linked meaning.
Documented limitations.
Checks whether the claim has enough definitions, assumptions and algorithmic context to be interpreted.
03 / WHY FAITHFULNESS MATTERS
See how restoring an assumption changes a guarantee, and how a counterexample disproves a source claim.
CASE A / RECOVERING CONDITIONS
The success event must include existence of a valid output, as well as its approximation quality.
The rank and logarithm-domain conditions determine when the algorithmic guarantee applies.
CASE B / A SOURCE DEFECT
This claim is false on the stated probability domain, which allows zero probability on nonzero matrix contributions.
04 / FROM STATEMENTS TO COMPUTATION
Selected source premises and Lean-checked connecting implications guide two numerical applications.
When is an iterative solve accurate enough?
Heterogeneous conductivity · schematic
A Gaussian sketch supplies a preconditioner. The original system’s residual determines whether the relative energy-error target of 10⁻⁶ has been reached.
The sketch is an auxiliary operator; it does not reduce the number of unknowns.
Explore the Gaussian-bound premise →Can a smaller response library meet a fixed error bound?
Prescribed excitation family · schematic
Energy conservation and a checked matrix residual bound control response error for all allowed combinations and nonnegative times under the stated model assumptions.
A saved-factor check supports reuse within this prescribed family, not arbitrary excitations.
Explore the wave-energy premise →Connecting proofs establish implications from explicit source premises and application assumptions. They do not supply omitted proofs of those source statements.
View the application figure (PDF) ↗05 / RESEARCH RESULTS
Randomized numerical linear algebra and numerical PDEs, drawn from four mathematical sources.
| Mathematical source | Targets | Accepted | With warning* | Not accepted |
|---|---|---|---|---|
| Drineas & MahoneyLectures on randomized numerical linear algebra | 32 | 28 | 1 | 4 |
| Halko, Martinsson & TroppFinding structure with randomness | 35 | 32 | 1 | 3 |
| Martinsson & TroppRandomized numerical linear algebra: Foundations and algorithms | 20 | 16 | 1 | 4 |
| Larsson & ThoméePartial differential equations with numerical methods | 84 | 81 | 0 | 3 |
| Total | 171 | 157 | 3 | 14 |
* The 3 source-warning acceptances are included in the 157 accepted statements. The sampling-optimality source defect is excluded from the accepted results.
Across 171 targets, FARMS produces 157 accepted formal statements. Explore accepted statements and the assumptions that connect them to computation.
Explore the statements →START WITH THE MATHEMATICS
Explicit assumptions. Source-linked meaning. Computational use.