willvieiraForestIPM

📦 R package - Bayesian hierarchical Integral Projection Model (IPM) for forest trees in eastern North America

forestIPM

R-CMD-check codecov Lean proofs

{forestIPM} is an R package implementing a Bayesian hierarchical Integral Projection Model (IPM) designed to study tree population dynamics in eastern North America. It combines growth, survival, and recruitment models, each parameterized as a function of climate and competition using forest inventory data. The package provides two engines to compute population growth rates () for 31 tree species and to simulate plot-level community dynamics over time.

This framework enables users to explore how demographic processes scale up to community patterns. More broadly, {forestIPM} can be used to investigate the effects of climate warming on tree performance, evaluate the sensitivity of to climate and competition (📄), examine how stochastic influences species range limits (📄), provides a foundation for studying the mechanisms driving species coexistence, and many more.

Documentation

A complete description of the methodology, ranging from fitting hierarchical Bayesian demographic models to constructing the IPM and applying it to ecological questions, is available in the companion book:

📓 Forest Demography IPM Book

Basic usage

The package website provides the function reference. The workflow is structured around 5 constructor functions used to define the key components of the model:

  • stand() representing a forest plot
  • species_model() defining which species to model
  • env_condition() specifying climate drivers
  • parameters() defining a single reproducible parameter realization from Bayesian posteriors
  • control() Configure IPM projection settings

These components are then passed to two main IPM engines:

  • lambda() computing population growth rate (lambda) per species
  • project() projecting population or community dynamics through time

For a step-by-step introduction to the package, see the Get Started vignette in the IPM Book.

Installation

# install.packages("devtools")
devtools::install_github("willvieira/forestIPM")

Mathematical Specification (Lean 4)

The mathematical model underlying {forestIPM} has been formally verified using Lean 4 and Mathlib. Each component of the model pipeline has a corresponding Lean module that proves key mathematical properties — such as convergence, non-negativity, and boundedness — hold by construction, independent of any numerical implementation.

These are not tests of the R code; they are machine-checked proofs that the mathematical model is internally consistent. The source files live in lean/.

ComponentModuleTheoremsProvedSorryStatus
Demographic modelsGrowth440fully proved
Survival440fully proved
Ingrowth9811 open
CovariatesCompetition550fully proved
Climate770fully proved
Population modelMidpointRule440fully proved
GaussLegendre4222 open
Kernel6511 open
EnginesAsymptoticLambda6155 open
CommunityDynamic7611 open
Total564610

Table auto-generated by lean/proof_status.sh. "Sorry" indicates theorems stated but not yet proved (open proof obligations).

Citation

If you use this package in your research, please cite the associated article.