forestIPM

{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 ($\lambda$) 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 $\lambda$ to climate and competition (📄), examine how stochastic $\lambda$ 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/.

Component	Module	Theorems	Proved	Sorry	Status
Demographic models	Growth	4	4	0	fully proved
	Survival	4	4	0	fully proved
	Ingrowth	9	8	1	1 open
Covariates	Competition	5	5	0	fully proved
	Climate	7	7	0	fully proved
Population model	MidpointRule	4	4	0	fully proved
	GaussLegendre	4	2	2	2 open
	Kernel	6	5	1	1 open
Engines	AsymptoticLambda	6	1	5	5 open
	CommunityDynamic	7	6	1	1 open
	Total	56	46	10

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.