@online{huang2024interactive,
  author       = {Huang, Xuanqiang Angelo},
  title        = {Interactive Theorem Provers},
  date         = {2024-05-08},
  organization = {Xuanqiang Angelo Huang's Blog},
  url          = {https://flecart.github.io/notes/interactive-theorem-provers/},
  langid       = {english},
  abstract     = {Most of times the pattern of proving and verifying it is like this p r o v e → v er i f y , that is: there is an entity that generates the solution, andPo then another that tries to verify it. But more expressive algorithms could be possible if there is interaction between the tw}
}