Few biological parameters suffice to reproduce measured dynamics in systems biology models: local sensitivity-based reduction with formally verified mathematical guarantees

This research presents a reproducible framework for identifying minimal parameter subsets that preserve the observable behaviour of biological dynamical models described by ordinary differential equations. The method combines sensitivity information derived from the Fisher information matrix, control of parameter redundancy, progressive elimination, and re-estimation of the selected parameters. Its purpose is not to establish complete identifiability of the original model, but to determine which parameters are sufficient to obtain a reduced and predictive representation of its measurable outputs.The framework was evaluated on 34 problems from the public Benchmark-Models-PEtab collection and on a social cognitive theory model fitted to real physical-activity data. Reduced subsets were obtained for 32 benchmark problems, generally containing two biological parameters in addition to the corresponding calibration parameters. Validation included parameter perturbations, re-estimation, robustness analyses, comparisons between the full and reduced models, prediction of held-out experiments, and independent verification of the simulations.The mathematical foundation was formalised in Lean 4 through 31 modules containing 289 theorems and lemmas. The formalisation establishes guarantees concerning the relationship between the Fisher-information-based energy criterion and output error, the differentiability of ODE solutions with respect to parameters, and the conditions required to apply these guarantees to specific ODE models. The relevant dynamical hypotheses were verified for 28 benchmark models. These guarantees are conditional: they do not establish global identifiability of the nonlinear models or convergence of the numerical optimisation algorithms.The repository contains the Python analysis code, Lean 4 formal proofs, model files, selected parameter subsets, and the results of the validation, robustness, and sensitivity analyses. It also provides instructions for reproducing the simulations, regenerating the tables, and compiling the formal proofs. Taken together, these materials make it possible to trace the main scientific claims to the data, numerical computations, and machine-checked mathematical results that support them.