Chemotaxis III in Lean Partial Lean 4 formalization · release v0.1.1
Menu

Acknowledgments and citation

Authors and AI disclosure

Paper authors: Le Chen, Ian Ruau and Wenxian Shen. Lean formalization and maintenance: Le Chen, with AI assistance in proofs, audit tooling and documentation. AI assistance is not an independent mathematical authority; the checked types, explicit inputs and stated review boundary determine the claims.

lean-pkg

Developed and verified with lean-pkg (doi:10.5281/zenodo.23272098). lean-pkg keeps the build, axiom and comparator receipts and generates the verification page and coverage table from them.

Auburn University Easley Cluster

This work was completed in part with resources provided by the Auburn University Easley Cluster.

Easley ran an accepted verification gate (full build, owned-declaration axiom audit, negative sorry control and the 108 + 12 comparator slots) during the private development of this companion, on an earlier state of the source. The receipts committed for this public history were produced on a local workstation; see trust and axioms.

Lean and Mathlib

Built on Lean 4 and Mathlib; exact versions are pinned in lean-toolchain and lake-manifest.json.

These standalone packages have their own APIs, receipts and releases. The companion currently retains its existing checked source rather than changing dependency identities during publication.

How to cite

Cite the software with CITATION.cff, and the paper:

@misc{chen_ruau_shen_2026_chemotaxis_iii,
  author = {Chen, Le and Ruau, Ian and Shen, Wenxian},
  title = {Chemotaxis models with signal-dependent sensitivity and a logistic-type source, III: Bifurcation and spike-like solutions},
  eprint = {2610.20976},
  archivePrefix = {arXiv},
  primaryClass = {math.AP},
  year = {2026}
}