Formalizing Hall's Marriage Theorem in Lean. - Alena Gusakov; Bhavik Mehta; Kyle A. Miller (CoRR, 2021)

L-space knots with tunnel number >1 by experiment. - Chris Anderson; Kenneth L. Baker; Xinghua Gao; Marc Kegel; Khanh Le; Kyle A. Miller; Sinem Onaran; Geoffrey Sangston; Samuel Tripp; Adam Wood; Ana Wright (Exp. Math., 2023)

Iterative Update Sample Consensus (IUSAC): A repeatable algorithm for optimal consensus set. - Jichul Kim; Byungjoon Lee 001; Michael R. Zanetti; Kyle A. Miller; Seongjai Kim (J. Comput. Appl. Math., 2024)

LeanLTL: A unifying framework for linear temporal logics in Lean. - Eric Vin; Kyle A. Miller; Daniel J. Fremont (CoRR, 2025)

Fast Collection Operations from Indexed Stream Fusion. - Scott Kovach; Praneeth Kolichala; Kyle A. Miller; David Broman; Fredrik Kjolstad (CoRR, 2025)