@article{DasguptaBhagwat1987,
  author  = {Dasgupta, Soura and Bhagwat, AS},
  title   = {Conditions for designing strictly positive real transfer functions for adaptive output error identification},
  journal = {IEEE Transactions on Circuits and Systems},
  volume  = {34},
  number  = {7},
  pages   = {731--736},
  year    = {1987}
}

@article{Kharitonov1978,
  author  = {Kharitonov, Vladimir L.},
  title   = {The asymptotic stability of the equilibrium state of a family of systems of linear differential equations},
  journal = {Differentsial'nye Uravneniya},
  volume  = {14},
  number  = {11},
  pages   = {2086--2088},
  year    = {1978}
}

@article{AndersonEtAl1990,
  author  = {Anderson, Brian D. O. and Dasgupta, Soura and Khargonekar, Pramod P. and Kraus, Frantisek J. and Mansour, Mohamed},
  title   = {Robust strict positive realness: characterization and construction},
  journal = {IEEE Transactions on Circuits and Systems},
  volume  = {37},
  number  = {7},
  pages   = {869--876},
  year    = {1990}
}

@article{BetserZeheb1993,
  author  = {Betser, A. and Zeheb, E.},
  title   = {Design of robust strictly positive real transfer functions},
  journal = {IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications},
  volume  = {40},
  number  = {9},
  pages   = {573--580},
  year    = {1993}
}

@article{YuWangFourth2001,
  author  = {Yu, Wensheng and Wang, Long},
  title   = {Anderson's claim on fourth-order {SPR} synthesis is true},
  journal = {IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications},
  volume  = {48},
  number  = {4},
  pages   = {506--509},
  year    = {2001}
}

@inproceedings{WangYu2001,
  author    = {Wang, Long and Yu, Wensheng},
  title     = {Robust {SPR} synthesis for low-order polynomial segments and interval polynomials},
  booktitle = {Proceedings of the 2001 American Control Conference},
  volume    = {5},
  pages     = {3612--3617},
  year      = {2001},
  publisher = {IEEE}
}

@article{YuWangAckermann2004,
  author  = {Yu, Wensheng and Wang, Long and Ackermann, J{\"u}rgen},
  title   = {Robust strictly positive real synthesis for polynomial families of arbitrary order},
  journal = {Science in China Series F: Information Sciences},
  volume  = {47},
  number  = {4},
  pages   = {475--489},
  year    = {2004}
}

@incollection{YuWang2008,
  author    = {Yu, Wensheng and Wang, Long},
  title     = {Design of robust strictly positive real transfer functions},
  booktitle = {Networked Control Systems: Theory and Applications},
  editor    = {Wang, Fei-Yue and Liu, Derong},
  pages     = {293--341},
  publisher = {Springer},
  address   = {London},
  year      = {2008}
}

@inproceedings{MouraUllrich2021,
  author    = {de Moura, Leonardo and Ullrich, Sebastian},
  title     = {The {Lean 4} theorem prover and programming language},
  booktitle = {Automated Deduction --- CADE 28},
  series    = {Lecture Notes in Computer Science},
  volume    = {12699},
  pages     = {625--635},
  publisher = {Springer},
  year      = {2021}
}

@inproceedings{Mathlib2020,
  author    = {{The mathlib Community}},
  title     = {The {Lean} mathematical library},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)},
  pages     = {367--381},
  publisher = {ACM},
  year      = {2020}
}

@inproceedings{DahmenHolzlLewis2019,
  author    = {Dahmen, Sander R. and H{\"o}lzl, Johannes and Lewis, Robert Y.},
  title     = {Formalizing the solution to the cap set problem},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {141},
  pages     = {15:1--15:19},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  year      = {2019}
}

@article{MahboubiSibutPinote2021,
  author  = {Mahboubi, Assia and Sibut-Pinote, Thomas},
  title   = {A formal proof of the irrationality of $\zeta(3)$},
  journal = {Logical Methods in Computer Science},
  volume  = {17},
  number  = {1},
  pages   = {16:1--16:28},
  year    = {2021}
}

@inproceedings{LiPaulson2019,
  author    = {Li, Wenda and Paulson, Lawrence C.},
  title     = {Counting polynomial roots in {Isabelle/HOL}: a formal proof of the {Budan--Fourier} theorem},
  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019)},
  pages     = {52--64},
  publisher = {ACM},
  year      = {2019}
}