Anderson, A., Bakšys, M., Bayer, J., Collares, M., Degenne, R., Dillies, Y., Eltschig, B., Gouëzel, S., Kytölä, K., Lewis, R., Lez, P., Lorenzo, L., Macbeth, H., Massot, P., Mellendijk, A., Miller, K., Monticone, P., Morrison, K., Nash, O., Song, U., Tao, T., van Doorn, F., Wilshaw, S., & Wu, L. (2023). Formalization of the Polynomial Freiman-Ruzsa Conjecture of Marton (Version 0.1.0) [Computer software]. https://github.com/teorth/pfr