Why do we have #ai chatbots that answer calls but no proof assistants that allow me to write in plain old #math without having to think about type theory when all I need at the moment is set theory and a little bit of integer arithmetic?
@semit0ne I thought there were proof assistants based on set theory. I though Mizar was supposed to be one of them.